[Metamath] Proposal: Allow primed class variables in set.mm body (e.g., A')

[David A. Wheeler]

I propose that we allow A' , B' , etc., as class variables, at least to support 
geometry.
This would make it much easier to indicate corresponding values (such as points)
and make it easier for proofs to more obviously match their original source 
material.
Having primed variables is already common mathematical practice, so we'd be
supporting common practices.

Background:
I'm hoping to contribute to the Elementary Geometry section, so I've been 
walking through
the current set.mm work due mostly to Thierry Arnoux, Mario Carneiro, and Scott 
Fenton.
This involves reading [Schwabauser], something of a trick since it's in German 
and
I can't read German. (Hello Google translate!)

An unnecessary challenge in doing this is that the geometry proofs
often involve many points that correspond to each other, which is typically 
indicated by
a prime. However, the set.mm main body doesn't support that. This inability to 
easily indicate
point correspondences makes it unnecessarily hard to read the proof statements, 
AND
it creates an unnecessary difference between set.mm and the original source 
material.

For example, here are the key hypotheses and conclusion of
http://us.metamath.org/mpeuni/tgifscgr.html

𝐵 ∈ (𝐴𝐼𝐶)        ; "B is between A and C"
𝐹 ∈ (𝐸𝐼𝐾))
(𝐴 − 𝐶) = (𝐸 − 𝐾)
(𝐵 − 𝐶) = (𝐹 − 𝐾)
(𝐴 − 𝐷) = (𝐸 − 𝐻)
(𝐶 − 𝐷) = (𝐾 − 𝐻)
Proves
(𝐵 − 𝐷) = (𝐹 − 𝐻)

If we allowed A' etc., this could expressed as the following, which
is MUCH clearer because the "primed" class variables make
correspondences MUCH more obvious:

𝐵 ∈ (𝐴𝐼𝐶)        ; "B is between A and C"
𝐵' ∈ (𝐴' 𝐼 𝐶' )
(𝐴 − 𝐶) = (𝐴' − 𝐶' )
(𝐵 − 𝐶) = (𝐵' − 𝐶' )
(𝐴 − 𝐷) = (𝐴' − 𝐷' )
(𝐶 − 𝐷) = (𝐶' − 𝐷' )
Proves
(𝐵 − 𝐷) = (𝐵' − 𝐷')

Having "primed" variables is very common in mathematics, and
there's no technical reason set.mm can't support them.
These are *already* defined in the Mathbox for Jonathan Ben-Naim, so they
just have to be moved up. We could also move up double-primed (A") if desired.

Let's do it!

--- David A. Wheeler

-- 
You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/E1juiC6-0004X6-W9%40rmmprod06.runbox.