Metamath Proof Explorer


Theorem cgr3tr

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

Ref Expression
Hypotheses tgcgrxfr.p 𝑃 = ( Base ‘ 𝐺 )
tgcgrxfr.m = ( dist ‘ 𝐺 )
tgcgrxfr.i 𝐼 = ( Itv ‘ 𝐺 )
tgcgrxfr.r = ( cgrG ‘ 𝐺 )
tgcgrxfr.g ( 𝜑𝐺 ∈ TarskiG )
tgbtwnxfr.a ( 𝜑𝐴𝑃 )
tgbtwnxfr.b ( 𝜑𝐵𝑃 )
tgbtwnxfr.c ( 𝜑𝐶𝑃 )
tgbtwnxfr.d ( 𝜑𝐷𝑃 )
tgbtwnxfr.e ( 𝜑𝐸𝑃 )
tgbtwnxfr.f ( 𝜑𝐹𝑃 )
tgbtwnxfr.2 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
cgr3tr.j ( 𝜑𝐽𝑃 )
cgr3tr.k ( 𝜑𝐾𝑃 )
cgr3tr.l ( 𝜑𝐿𝑃 )
cgr3tr.1 ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ⟨“ 𝐽 𝐾 𝐿 ”⟩ )
Assertion cgr3tr ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ⟨“ 𝐽 𝐾 𝐿 ”⟩ )

Proof

Step Hyp Ref Expression
1 tgcgrxfr.p 𝑃 = ( Base ‘ 𝐺 )
2 tgcgrxfr.m = ( dist ‘ 𝐺 )
3 tgcgrxfr.i 𝐼 = ( Itv ‘ 𝐺 )
4 tgcgrxfr.r = ( cgrG ‘ 𝐺 )
5 tgcgrxfr.g ( 𝜑𝐺 ∈ TarskiG )
6 tgbtwnxfr.a ( 𝜑𝐴𝑃 )
7 tgbtwnxfr.b ( 𝜑𝐵𝑃 )
8 tgbtwnxfr.c ( 𝜑𝐶𝑃 )
9 tgbtwnxfr.d ( 𝜑𝐷𝑃 )
10 tgbtwnxfr.e ( 𝜑𝐸𝑃 )
11 tgbtwnxfr.f ( 𝜑𝐹𝑃 )
12 tgbtwnxfr.2 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
13 cgr3tr.j ( 𝜑𝐽𝑃 )
14 cgr3tr.k ( 𝜑𝐾𝑃 )
15 cgr3tr.l ( 𝜑𝐿𝑃 )
16 cgr3tr.1 ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ⟨“ 𝐽 𝐾 𝐿 ”⟩ )
17 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp1 ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) )
18 1 2 3 4 5 9 10 11 13 14 15 16 cgr3simp1 ( 𝜑 → ( 𝐷 𝐸 ) = ( 𝐽 𝐾 ) )
19 17 18 eqtrd ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐽 𝐾 ) )
20 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp2 ( 𝜑 → ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) )
21 1 2 3 4 5 9 10 11 13 14 15 16 cgr3simp2 ( 𝜑 → ( 𝐸 𝐹 ) = ( 𝐾 𝐿 ) )
22 20 21 eqtrd ( 𝜑 → ( 𝐵 𝐶 ) = ( 𝐾 𝐿 ) )
23 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp3 ( 𝜑 → ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) )
24 1 2 3 4 5 9 10 11 13 14 15 16 cgr3simp3 ( 𝜑 → ( 𝐹 𝐷 ) = ( 𝐿 𝐽 ) )
25 23 24 eqtrd ( 𝜑 → ( 𝐶 𝐴 ) = ( 𝐿 𝐽 ) )
26 1 2 4 5 6 7 8 13 14 15 19 22 25 trgcgr ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ⟨“ 𝐽 𝐾 𝐿 ”⟩ )