Metamath Proof Explorer


Theorem trgcgr

Description: Triangle congruence. (Contributed by Thierry Arnoux, 27-Apr-2019)

Ref Expression
Hypotheses trgcgrg.p 𝑃 = ( Base ‘ 𝐺 )
trgcgrg.m = ( dist ‘ 𝐺 )
trgcgrg.r = ( cgrG ‘ 𝐺 )
trgcgrg.g ( 𝜑𝐺 ∈ TarskiG )
trgcgrg.a ( 𝜑𝐴𝑃 )
trgcgrg.b ( 𝜑𝐵𝑃 )
trgcgrg.c ( 𝜑𝐶𝑃 )
trgcgrg.d ( 𝜑𝐷𝑃 )
trgcgrg.e ( 𝜑𝐸𝑃 )
trgcgrg.f ( 𝜑𝐹𝑃 )
trgcgr.1 ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) )
trgcgr.2 ( 𝜑 → ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) )
trgcgr.3 ( 𝜑 → ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) )
Assertion trgcgr ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )

Proof

Step Hyp Ref Expression
1 trgcgrg.p 𝑃 = ( Base ‘ 𝐺 )
2 trgcgrg.m = ( dist ‘ 𝐺 )
3 trgcgrg.r = ( cgrG ‘ 𝐺 )
4 trgcgrg.g ( 𝜑𝐺 ∈ TarskiG )
5 trgcgrg.a ( 𝜑𝐴𝑃 )
6 trgcgrg.b ( 𝜑𝐵𝑃 )
7 trgcgrg.c ( 𝜑𝐶𝑃 )
8 trgcgrg.d ( 𝜑𝐷𝑃 )
9 trgcgrg.e ( 𝜑𝐸𝑃 )
10 trgcgrg.f ( 𝜑𝐹𝑃 )
11 trgcgr.1 ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) )
12 trgcgr.2 ( 𝜑 → ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) )
13 trgcgr.3 ( 𝜑 → ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) )
14 1 2 3 4 5 6 7 8 9 10 trgcgrg ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) ∧ ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) ∧ ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) ) ) )
15 11 12 13 14 mpbir3and ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )