Metamath Proof Explorer

Theorem tgextamirn

Description: The midpoint-reflected point is off line A C . If it were on that line, mirln -- whose centre-on-the-line hypothesis is the midpoint, itself on A C -- would put its reflection there too, and mirmir says that reflection is B , contradicting the triangle's non-collinearity. This is the strengthening inA cannot give: it is what turns "inside the angle" into an open half-plane fact. (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 tgextamirn 
|- ( ph -> -. ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) )

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 1 4 3 5 7 8 6 9 ncolrot1 
 |-  ( ph -> -. ( B e. ( C L A ) \/ C = A ) )
11 1 4 3 5 8 6 7 10 ncolcom 
 |-  ( ph -> -. ( B e. ( A L C ) \/ A = C ) )
12 ioran 
 |-  ( -. ( B e. ( A L C ) \/ A = C ) <-> ( -. B e. ( A L C ) /\ -. A = C ) )
13 11 12 sylib 
 |-  ( ph -> ( -. B e. ( A L C ) /\ -. A = C ) )
14 13 simpld 
 |-  ( ph -> -. B e. ( A L C ) )
15 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
16 5 adantr 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) ) -> G e. TarskiG )
17 1 4 3 5 7 8 6 9 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
18 1 2 3 5 17 6 8 midcl 
 |-  ( ph -> ( A ( midG ` G ) C ) e. P )
19 18 adantr 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) ) -> ( A ( midG ` G ) C ) e. P )
20 eqid 
 |-  ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) = ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) )
21 7 adantr 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) ) -> B e. P )
22 1 2 3 4 15 16 19 20 21 mirmir 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) = B )
23 1 3 4 5 6 7 8 9 ncolne2 
 |-  ( ph -> A =/= C )
24 1 3 4 5 6 8 23 tgelrnln 
 |-  ( ph -> ( A L C ) e. ran L )
25 24 adantr 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) ) -> ( A L C ) e. ran L )
26 1 2 3 5 17 6 8 midbtwn 
 |-  ( ph -> ( A ( midG ` G ) C ) e. ( A I C ) )
27 1 4 3 5 6 8 18 26 btwncolg1 
 |-  ( ph -> ( ( A ( midG ` G ) C ) e. ( A L C ) \/ A = C ) )
28 23 neneqd 
 |-  ( ph -> -. A = C )
29 27 28 olcnd 
 |-  ( ph -> ( A ( midG ` G ) C ) e. ( A L C ) )
30 29 adantr 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) ) -> ( A ( midG ` G ) C ) e. ( A L C ) )
31 simpr 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) )
32 1 2 3 4 15 16 20 25 30 31 mirln 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) e. ( A L C ) )
33 22 32 eqeltrrd 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) ) -> B e. ( A L C ) )
34 14 33 mtand 
 |-  ( ph -> -. ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) )