Metamath Proof Explorer


Theorem midcom

Description: Commutativity rule for the midpoint. (Contributed by Thierry Arnoux, 2-Dec-2019)

Ref Expression
Hypotheses ismid.p P = Base G
ismid.d - ˙ = dist G
ismid.i I = Itv G
ismid.g φ G 𝒢 Tarski
ismid.1 φ G Dim 𝒢 2
midcl.1 φ A P
midcl.2 φ B P
Assertion midcom φ A mid 𝒢 G B = B mid 𝒢 G A

Proof

Step Hyp Ref Expression
1 ismid.p P = Base G
2 ismid.d - ˙ = dist G
3 ismid.i I = Itv G
4 ismid.g φ G 𝒢 Tarski
5 ismid.1 φ G Dim 𝒢 2
6 midcl.1 φ A P
7 midcl.2 φ B P
8 eqid Line 𝒢 G = Line 𝒢 G
9 eqid pInv 𝒢 G = pInv 𝒢 G
10 1 2 3 4 5 7 6 midcl φ B mid 𝒢 G A P
11 eqid pInv 𝒢 G B mid 𝒢 G A = pInv 𝒢 G B mid 𝒢 G A
12 eqidd φ B mid 𝒢 G A = B mid 𝒢 G A
13 1 2 3 4 5 7 6 12 midcgr φ B mid 𝒢 G A - ˙ B = B mid 𝒢 G A - ˙ A
14 1 2 3 4 5 7 6 midbtwn φ B mid 𝒢 G A B I A
15 1 2 3 8 9 4 10 11 6 7 13 14 ismir φ B = pInv 𝒢 G B mid 𝒢 G A A
16 1 2 3 4 5 6 7 9 10 ismidb φ B = pInv 𝒢 G B mid 𝒢 G A A A mid 𝒢 G B = B mid 𝒢 G A
17 15 16 mpbid φ A mid 𝒢 G B = B mid 𝒢 G A