Theorem tgmircgra

Description: The angle congruence the exterior-angle theorem opens with: the interior angle at A in triangle C A B is congruent to the angle at C in the midpoint-reflected triangle. This is cgrcgra over tgmircgrg ; the vertex distinctnesses come from the non-collinearity via tgbcne and tgacne . (Contributed by JAG, 12-Aug-2026)

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

Proof

Step	Hyp	Ref	Expression
1		tgmircgrg.p	|- P = ( Base ` G )
2		tgmircgrg.m	|- .- = ( dist ` G )
3		tgmircgrg.i	|- I = ( Itv ` G )
4		tgmircgrg.l	|- L = ( LineG ` G )
5		tgmircgrg.g	|- ( ph -> G e. TarskiG )
6		tgmircgrg.a	|- ( ph -> A e. P )
7		tgmircgrg.b	|- ( ph -> B e. P )
8		tgmircgrg.c	|- ( ph -> C e. P )
9		tgmircgrg.ncol	|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
10		eqid	|- ( hlG ` G ) = ( hlG ` G )
11		eqid	|- ( pInvG ` G ) = ( pInvG ` G )
12	1 4 3 5 7 8 6 9	ncoltgdim2	|- ( ph -> G TarskiGDim>= 2 )
13	1 2 3 5 12 6 8	midcl	|- ( ph -> ( A ( midG ` G ) C ) e. P )
14		eqid	|- ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) = ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) )
15	1 2 3 4 11 5 13 14 7	mircl	|- ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
16	1 3 4 5 7 8 6 9	tgbcne	|- ( ph -> C =/= A )
17	1 3 4 5 7 8 6 9	tgacne	|- ( ph -> B =/= A )
18	17	necomd	|- ( ph -> A =/= B )
19	1 2 3 4 5 6 7 8 9	tgmircgrg	|- ( ph -> <" C A B "> ( cgrG ` G ) <" A C ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) "> )
20	1 3 5 10 8 6 7 6 8 15 16 18 19	cgrcgra	|- ( ph -> <" C A B "> ( cgrA ` G ) <" A C ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) "> )