Metamath Proof Explorer

Theorem tgmircgrg

Description: Reflecting B through the midpoint of A and C carries triangle C A B onto A C P , where P is the reflected point. The dimension condition the mid* family carries is discharged from the non-collinearity through ncoltgdim2 , not taken as a hypothesis. (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 tgmircgrg 
|- ( ph -> <" C A B "> ( cgrG ` 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 
 |-  ( cgrG ` G ) = ( cgrG ` 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 eqidd 
 |-  ( ph -> ( A .- C ) = ( A .- C ) )
17 1 2 3 5 6 8 6 8 16 tgcgrcoml 
 |-  ( ph -> ( C .- A ) = ( A .- C ) )
18 eqidd 
 |-  ( ph -> ( A ( midG ` G ) C ) = ( A ( midG ` G ) C ) )
19 1 2 3 5 12 6 8 11 13 ismidb 
 |-  ( ph -> ( C = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` A ) <-> ( A ( midG ` G ) C ) = ( A ( midG ` G ) C ) ) )
20 18 19 mpbird 
 |-  ( ph -> C = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` A ) )
21 20 oveq1d 
 |-  ( ph -> ( C .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) = ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` A ) .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) )
22 1 2 3 4 11 5 13 14 6 7 miriso 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` A ) .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) = ( A .- B ) )
23 21 22 eqtrd 
 |-  ( ph -> ( C .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) = ( A .- B ) )
24 23 eqcomd 
 |-  ( ph -> ( A .- B ) = ( C .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) )
25 1 2 3 4 11 5 13 14 7 8 miriso 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` C ) ) = ( B .- C ) )
26 20 fveq2d 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` C ) = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` A ) ) )
27 1 2 3 4 11 5 13 14 6 mirmir 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` A ) ) = A )
28 26 27 eqtrd 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` C ) = A )
29 28 oveq2d 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` C ) ) = ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) .- A ) )
30 25 29 eqtr3d 
 |-  ( ph -> ( B .- C ) = ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) .- A ) )
31 1 2 10 5 8 6 7 6 8 15 17 24 30 trgcgr 
 |-  ( ph -> <" C A B "> ( cgrG ` G ) <" A C ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) "> )