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 ) )