Theorem cgraid

Description: Angle congruence is reflexive. Theorem 11.6 of Schwabhauser p. 96. (Contributed by Thierry Arnoux, 31-Jul-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 )
	cgraid.1	|- ( ph -> A =/= B )
	cgraid.2	|- ( ph -> B =/= C )
Assertion	cgraid	|- ( ph -> <" A B C "> ( cgrA ` G ) <" A B C "> )

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		cgraid.1	|- ( ph -> A =/= B )
9		cgraid.2	|- ( ph -> B =/= C )
10		eqid	|- ( dist ` G ) = ( dist ` G )
11		eqid	|- ( cgrG ` G ) = ( cgrG ` G )
12	1 10 2 11 3 5 6 7	cgr3id	|- ( ph -> <" A B C "> ( cgrG ` G ) <" A B C "> )
13	1 2 4 5 5 6 3 8	hlid	|- ( ph -> A ( K ` B ) A )
14	9	necomd	|- ( ph -> C =/= B )
15	1 2 4 7 5 6 3 14	hlid	|- ( ph -> C ( K ` B ) C )
16	1 2 4 3 5 6 7 5 6 7 5 7 12 13 15	iscgrad	|- ( ph -> <" A B C "> ( cgrA ` G ) <" A B C "> )