Theorem cgrcgra

Description: Triangle congruence implies angle congruence. This is a portion of CPCTC, focusing on a specific angle. (Contributed by Arnoux, 2-Aug-2020)

	Ref	Expression
Hypotheses	cgraid.p	|- P = ( Base ` G )
	cgraid.i	|- I = ( Itv ` G )
	cgraid.g	|- ( ph -> G e. TarskiG )
	cgraid.k	|- K = ( hlG ` G )
	cgraid.a	|- ( ph -> A e. P )
	cgraid.b	|- ( ph -> B e. P )
	cgraid.c	|- ( ph -> C e. P )
	cgracom.d	|- ( ph -> D e. P )
	cgracom.e	|- ( ph -> E e. P )
	cgracom.f	|- ( ph -> F e. P )
	cgrcgra.1	|- ( ph -> A =/= B )
	cgrcgra.2	|- ( ph -> B =/= C )
	cgrcgra.3	|- ( ph -> <" A B C "> ( cgrG ` G ) <" D E F "> )
Assertion	cgrcgra	|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )

Proof

Step	Hyp	Ref	Expression
1		cgraid.p	|- P = ( Base ` G )
2		cgraid.i	|- I = ( Itv ` G )
3		cgraid.g	|- ( ph -> G e. TarskiG )
4		cgraid.k	|- K = ( hlG ` G )
5		cgraid.a	|- ( ph -> A e. P )
6		cgraid.b	|- ( ph -> B e. P )
7		cgraid.c	|- ( ph -> C e. P )
8		cgracom.d	|- ( ph -> D e. P )
9		cgracom.e	|- ( ph -> E e. P )
10		cgracom.f	|- ( ph -> F e. P )
11		cgrcgra.1	|- ( ph -> A =/= B )
12		cgrcgra.2	|- ( ph -> B =/= C )
13		cgrcgra.3	|- ( ph -> <" A B C "> ( cgrG ` G ) <" D E F "> )
14		eqid	|- ( dist ` G ) = ( dist ` G )
15		eqid	|- ( cgrG ` G ) = ( cgrG ` G )
16	1 14 2 15 3 5 6 7 8 9 10 13	cgr3simp1	|- ( ph -> ( A ( dist ` G ) B ) = ( D ( dist ` G ) E ) )
17	1 14 2 3 5 6 8 9 16 11	tgcgrneq	|- ( ph -> D =/= E )
18	1 2 4 8 5 9 3 17	hlid	|- ( ph -> D ( K ` E ) D )
19	1 14 2 15 3 5 6 7 8 9 10 13	cgr3simp2	|- ( ph -> ( B ( dist ` G ) C ) = ( E ( dist ` G ) F ) )
20	1 14 2 3 6 7 9 10 19	tgcgrcomlr	|- ( ph -> ( C ( dist ` G ) B ) = ( F ( dist ` G ) E ) )
21	12	necomd	|- ( ph -> C =/= B )
22	1 14 2 3 7 6 10 9 20 21	tgcgrneq	|- ( ph -> F =/= E )
23	1 2 4 10 5 9 3 22	hlid	|- ( ph -> F ( K ` E ) F )
24	1 2 4 3 5 6 7 8 9 10 8 10 13 18 23	iscgrad	|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )