Metamath Proof Explorer

Theorem tgextahp

Description: The reflected point and D lie on the same OPEN half-plane of line A C -- the fact acopyeu requires and inA does not give. tgextalem1inag puts the reflected point inside the exterior angle, which is non-strict: isinag 's witness clause is ( x = C \/ x ( KC ) P ) , so a point inside an angle may sit on a boundary ray. The x = C branch collapses to ( A e. ( C L D ) \/ C = D ) and is killed by tgextancd ; the main branch is tgextahpl , whose off-line input is tgextamirn . The $d s are the mandatory ones isinag carries for the witness variable. (Contributed by JAG , 12-Aug-2026)

Ref Expression
Hypotheses tgextalem1inag.p 
|- P = ( Base ` G )
tgextalem1inag.m 
|- .- = ( dist ` G )
tgextalem1inag.i 
|- I = ( Itv ` G )
tgextalem1inag.l 
|- L = ( LineG ` G )
tgextalem1inag.k 
|- K = ( hlG ` G )
tgextalem1inag.g 
|- ( ph -> G e. TarskiG )
tgextalem1inag.a 
|- ( ph -> A e. P )
tgextalem1inag.b 
|- ( ph -> B e. P )
tgextalem1inag.c 
|- ( ph -> C e. P )
tgextalem1inag.d 
|- ( ph -> D e. P )
tgextalem1inag.ext 
|- ( ph -> C e. ( B I D ) )
tgextalem1inag.ncol 
|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
tgextalem1inag.ne 
|- ( ph -> C =/= D )
Assertion tgextahp 
|- ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( ( hpG ` G ) ` ( A L C ) ) D )

Proof

Step Hyp Ref Expression
1 tgextalem1inag.p 
 |-  P = ( Base ` G )
2 tgextalem1inag.m 
 |-  .- = ( dist ` G )
3 tgextalem1inag.i 
 |-  I = ( Itv ` G )
4 tgextalem1inag.l 
 |-  L = ( LineG ` G )
5 tgextalem1inag.k 
 |-  K = ( hlG ` G )
6 tgextalem1inag.g 
 |-  ( ph -> G e. TarskiG )
7 tgextalem1inag.a 
 |-  ( ph -> A e. P )
8 tgextalem1inag.b 
 |-  ( ph -> B e. P )
9 tgextalem1inag.c 
 |-  ( ph -> C e. P )
10 tgextalem1inag.d 
 |-  ( ph -> D e. P )
11 tgextalem1inag.ext 
 |-  ( ph -> C e. ( B I D ) )
12 tgextalem1inag.ncol 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
13 tgextalem1inag.ne 
 |-  ( ph -> C =/= D )
14 1 2 3 4 5 6 7 8 9 10 11 12 13 tgextalem1inag 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( inA ` G ) <" A C D "> )
15 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
16 1 4 3 6 8 9 7 12 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
17 1 2 3 6 16 7 9 midcl 
 |-  ( ph -> ( A ( midG ` G ) C ) e. P )
18 eqid 
 |-  ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) = ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) )
19 1 2 3 4 15 6 17 18 8 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
20 1 3 5 19 7 9 10 6 isinag 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( inA ` G ) <" A C D "> <-> ( ( A =/= C /\ D =/= C /\ ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) =/= C ) /\ E. x e. P ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) )
21 14 20 mpbid 
 |-  ( ph -> ( ( A =/= C /\ D =/= C /\ ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) =/= C ) /\ E. x e. P ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) )
22 21 simprd 
 |-  ( ph -> E. x e. P ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) )
23 6 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) -> G e. TarskiG )
24 23 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x = C ) -> G e. TarskiG )
25 9 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) -> C e. P )
26 25 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x = C ) -> C e. P )
27 10 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) -> D e. P )
28 27 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x = C ) -> D e. P )
29 7 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) -> A e. P )
30 29 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x = C ) -> A e. P )
31 simpr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x = C ) -> x = C )
32 simprrl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) -> x e. ( A I D ) )
33 32 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x = C ) -> x e. ( A I D ) )
34 31 33 eqeltrrd 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x = C ) -> C e. ( A I D ) )
35 1 4 3 24 26 28 30 34 btwncolg2 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x = C ) -> ( A e. ( C L D ) \/ C = D ) )
36 1 2 3 4 6 7 8 9 10 11 12 13 tgextancd 
 |-  ( ph -> -. ( A e. ( C L D ) \/ C = D ) )
37 36 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) -> -. ( A e. ( C L D ) \/ C = D ) )
38 37 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x = C ) -> -. ( A e. ( C L D ) \/ C = D ) )
39 35 38 pm2.21dd 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x = C ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( ( hpG ` G ) ` ( A L C ) ) D )
40 23 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> G e. TarskiG )
41 29 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> A e. P )
42 25 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> C e. P )
43 27 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> D e. P )
44 19 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
45 44 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
46 simprl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) -> x e. P )
47 46 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> x e. P )
48 37 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> -. ( A e. ( C L D ) \/ C = D ) )
49 1 2 3 4 6 7 8 9 12 tgextamirn 
 |-  ( ph -> -. ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) )
50 49 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) -> -. ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) )
51 50 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> -. ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. ( A L C ) )
52 32 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> x e. ( A I D ) )
53 simpr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) )
54 1 2 3 4 5 40 41 42 43 45 47 48 51 52 53 tgextahpl 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) /\ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( ( hpG ` G ) ` ( A L C ) ) D )
55 simprrr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) -> ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) )
56 39 54 55 mpjaodan 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( A I D ) /\ ( x = C \/ x ( K ` C ) ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ) ) ) ) -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( ( hpG ` G ) ` ( A L C ) ) D )
57 22 56 rexlimddv 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( ( hpG ` G ) ` ( A L C ) ) D )