Metamath Proof Explorer


Theorem trgcgrcom

Description: Commutative law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019)

Ref Expression
Hypotheses tgcgrxfr.p P = Base G
tgcgrxfr.m - ˙ = dist G
tgcgrxfr.i I = Itv G
tgcgrxfr.r ˙ = 𝒢 G
tgcgrxfr.g φ G 𝒢 Tarski
tgbtwnxfr.a φ A P
tgbtwnxfr.b φ B P
tgbtwnxfr.c φ C P
tgbtwnxfr.d φ D P
tgbtwnxfr.e φ E P
tgbtwnxfr.f φ F P
tgbtwnxfr.2 φ ⟨“ ABC ”⟩ ˙ ⟨“ DEF ”⟩
Assertion trgcgrcom φ ⟨“ DEF ”⟩ ˙ ⟨“ ABC ”⟩

Proof

Step Hyp Ref Expression
1 tgcgrxfr.p P = Base G
2 tgcgrxfr.m - ˙ = dist G
3 tgcgrxfr.i I = Itv G
4 tgcgrxfr.r ˙ = 𝒢 G
5 tgcgrxfr.g φ G 𝒢 Tarski
6 tgbtwnxfr.a φ A P
7 tgbtwnxfr.b φ B P
8 tgbtwnxfr.c φ C P
9 tgbtwnxfr.d φ D P
10 tgbtwnxfr.e φ E P
11 tgbtwnxfr.f φ F P
12 tgbtwnxfr.2 φ ⟨“ ABC ”⟩ ˙ ⟨“ DEF ”⟩
13 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp1 φ A - ˙ B = D - ˙ E
14 13 eqcomd φ D - ˙ E = A - ˙ B
15 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp2 φ B - ˙ C = E - ˙ F
16 15 eqcomd φ E - ˙ F = B - ˙ C
17 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp3 φ C - ˙ A = F - ˙ D
18 17 eqcomd φ F - ˙ D = C - ˙ A
19 1 2 4 5 9 10 11 6 7 8 14 16 18 trgcgr φ ⟨“ DEF ”⟩ ˙ ⟨“ ABC ”⟩