Metamath Proof Explorer


Theorem isoas

Description: Congruence theorem for isocele triangles: if two angles of a triangle are congruent, then the corresponding sides also are. (Contributed by Thierry Arnoux, 5-Oct-2020)

Ref Expression
Hypotheses isoas.p
|- P = ( Base ` G )
isoas.m
|- .- = ( dist ` G )
isoas.i
|- I = ( Itv ` G )
isoas.l
|- L = ( LineG ` G )
isoas.g
|- ( ph -> G e. TarskiG )
isoas.a
|- ( ph -> A e. P )
isoas.b
|- ( ph -> B e. P )
isoas.c
|- ( ph -> C e. P )
isoas.1
|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
isoas.2
|- ( ph -> <" A B C "> ( cgrA ` G ) <" A C B "> )
Assertion isoas
|- ( ph -> ( A .- B ) = ( A .- C ) )

Proof

Step Hyp Ref Expression
1 isoas.p
 |-  P = ( Base ` G )
2 isoas.m
 |-  .- = ( dist ` G )
3 isoas.i
 |-  I = ( Itv ` G )
4 isoas.l
 |-  L = ( LineG ` G )
5 isoas.g
 |-  ( ph -> G e. TarskiG )
6 isoas.a
 |-  ( ph -> A e. P )
7 isoas.b
 |-  ( ph -> B e. P )
8 isoas.c
 |-  ( ph -> C e. P )
9 isoas.1
 |-  ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
10 isoas.2
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" A C B "> )
11 eqid
 |-  ( cgrG ` G ) = ( cgrG ` G )
12 1 4 3 5 6 7 8 9 ncolrot1
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
13 1 2 3 5 7 8 axtgcgrrflx
 |-  ( ph -> ( B .- C ) = ( C .- B ) )
14 eqid
 |-  ( hlG ` G ) = ( hlG ` G )
15 1 3 5 14 6 7 8 6 8 7 10 cgracom
 |-  ( ph -> <" A C B "> ( cgrA ` G ) <" A B C "> )
16 1 3 2 5 6 8 7 6 7 8 15 cgraswaplr
 |-  ( ph -> <" B C A "> ( cgrA ` G ) <" C B A "> )
17 1 2 3 5 7 8 6 8 7 6 4 12 13 16 10 tgasa
 |-  ( ph -> <" B C A "> ( cgrG ` G ) <" C B A "> )
18 1 2 3 11 5 7 8 6 8 7 6 17 cgr3simp3
 |-  ( ph -> ( A .- B ) = ( A .- C ) )