Metamath Proof Explorer

Theorem nhpmirhp

Description: If a point Z is on the plane defined by a line A and a point Y , but not on the same half-plane as Y , then its mirror point ( MZ ) by a point X on A is on the same half-plane as Y . (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses nhpmirhp.p 
|- P = ( Base ` G )
nhpmirhp.l 
|- L = ( LineG ` G )
nhpmirhp.s 
|- S = ( pInvG ` G )
nhpmirhp.e 
|- E = ( PlnG ` G )
nhpmirhp.m 
|- M = ( S ` X )
nhpmirhp.g 
|- ( ph -> G e. TarskiG )
nhpmirhp.a 
|- ( ph -> A e. ran L )
nhpmirhp.x 
|- ( ph -> X e. A )
nhpmirhp.y 
|- ( ph -> Y e. ( P \ A ) )
nhpmirhp.z 
|- ( ph -> Z e. ( ( A E Y ) \ A ) )
nhpmirhp.1 
|- ( ph -> -. Y ( ( hpG ` G ) ` A ) Z )
Assertion nhpmirhp 
|- ( ph -> Y ( ( hpG ` G ) ` A ) ( M ` Z ) )

Proof

Step Hyp Ref Expression
1 nhpmirhp.p 
 |-  P = ( Base ` G )
2 nhpmirhp.l 
 |-  L = ( LineG ` G )
3 nhpmirhp.s 
 |-  S = ( pInvG ` G )
4 nhpmirhp.e 
 |-  E = ( PlnG ` G )
5 nhpmirhp.m 
 |-  M = ( S ` X )
6 nhpmirhp.g 
 |-  ( ph -> G e. TarskiG )
7 nhpmirhp.a 
 |-  ( ph -> A e. ran L )
8 nhpmirhp.x 
 |-  ( ph -> X e. A )
9 nhpmirhp.y 
 |-  ( ph -> Y e. ( P \ A ) )
10 nhpmirhp.z 
 |-  ( ph -> Z e. ( ( A E Y ) \ A ) )
11 nhpmirhp.1 
 |-  ( ph -> -. Y ( ( hpG ` G ) ` A ) Z )
12 eqid 
 |-  ( dist ` G ) = ( dist ` G )
13 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
14 eleq1w 
 |-  ( x = z -> ( x e. ( P \ A ) <-> z e. ( P \ A ) ) )
15 eleq1w 
 |-  ( y = w -> ( y e. ( P \ A ) <-> w e. ( P \ A ) ) )
16 14 15 bi2anan9 
 |-  ( ( x = z /\ y = w ) -> ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) <-> ( z e. ( P \ A ) /\ w e. ( P \ A ) ) ) )
17 oveq12 
 |-  ( ( x = z /\ y = w ) -> ( x ( Itv ` G ) y ) = ( z ( Itv ` G ) w ) )
18 17 eleq2d 
 |-  ( ( x = z /\ y = w ) -> ( s e. ( x ( Itv ` G ) y ) <-> s e. ( z ( Itv ` G ) w ) ) )
19 18 rexbidv 
 |-  ( ( x = z /\ y = w ) -> ( E. s e. A s e. ( x ( Itv ` G ) y ) <-> E. s e. A s e. ( z ( Itv ` G ) w ) ) )
20 eleq1w 
 |-  ( s = t -> ( s e. ( z ( Itv ` G ) w ) <-> t e. ( z ( Itv ` G ) w ) ) )
21 20 cbvrexvw 
 |-  ( E. s e. A s e. ( z ( Itv ` G ) w ) <-> E. t e. A t e. ( z ( Itv ` G ) w ) )
22 19 21 bitrdi 
 |-  ( ( x = z /\ y = w ) -> ( E. s e. A s e. ( x ( Itv ` G ) y ) <-> E. t e. A t e. ( z ( Itv ` G ) w ) ) )
23 16 22 anbi12d 
 |-  ( ( x = z /\ y = w ) -> ( ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) <-> ( ( z e. ( P \ A ) /\ w e. ( P \ A ) ) /\ E. t e. A t e. ( z ( Itv ` G ) w ) ) ) )
24 23 cbvopabv 
 |-  { <. x , y >. | ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) } = { <. z , w >. | ( ( z e. ( P \ A ) /\ w e. ( P \ A ) ) /\ E. t e. A t e. ( z ( Itv ` G ) w ) ) }
25 10 eldifad 
 |-  ( ph -> Z e. ( A E Y ) )
26 1 13 2 4 6 7 9 25 plngssp 
 |-  ( ph -> Z e. P )
27 1 2 13 6 7 8 tglnpt 
 |-  ( ph -> X e. P )
28 1 12 13 2 3 6 27 5 26 mircl 
 |-  ( ph -> ( M ` Z ) e. P )
29 10 eldifbd 
 |-  ( ph -> -. Z e. A )
30 26 29 eldifd 
 |-  ( ph -> Z e. ( P \ A ) )
31 1 13 3 5 24 6 7 8 30 2 oppmir 
 |-  ( ph -> Z { <. x , y >. | ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) } ( M ` Z ) )
32 1 12 13 24 2 7 6 26 28 31 oppcom 
 |-  ( ph -> ( M ` Z ) { <. x , y >. | ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) } Z )
33 9 eldifad 
 |-  ( ph -> Y e. P )
34 6 adantr 
 |-  ( ( ph /\ Z ( ( hpG ` G ) ` A ) Y ) -> G e. TarskiG )
35 7 adantr 
 |-  ( ( ph /\ Z ( ( hpG ` G ) ` A ) Y ) -> A e. ran L )
36 26 adantr 
 |-  ( ( ph /\ Z ( ( hpG ` G ) ` A ) Y ) -> Z e. P )
37 33 adantr 
 |-  ( ( ph /\ Z ( ( hpG ` G ) ` A ) Y ) -> Y e. P )
38 simpr 
 |-  ( ( ph /\ Z ( ( hpG ` G ) ` A ) Y ) -> Z ( ( hpG ` G ) ` A ) Y )
39 1 13 2 34 35 36 24 37 38 hpgcom 
 |-  ( ( ph /\ Z ( ( hpG ` G ) ` A ) Y ) -> Y ( ( hpG ` G ) ` A ) Z )
40 11 39 mtand 
 |-  ( ph -> -. Z ( ( hpG ` G ) ` A ) Y )
41 1 13 2 4 6 7 9 24 26 elplng 
 |-  ( ph -> ( Z e. ( A E Y ) <-> ( Z e. A \/ Z ( ( hpG ` G ) ` A ) Y \/ Z { <. x , y >. | ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) } Y ) ) )
42 25 41 mpbid 
 |-  ( ph -> ( Z e. A \/ Z ( ( hpG ` G ) ` A ) Y \/ Z { <. x , y >. | ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) } Y ) )
43 29 40 42 ecase33d 
 |-  ( ph -> Z { <. x , y >. | ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) } Y )
44 1 12 13 24 2 7 6 26 33 43 oppcom 
 |-  ( ph -> Y { <. x , y >. | ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) } Z )
45 1 13 2 24 6 7 33 28 26 44 lnopp2hpgb 
 |-  ( ph -> ( ( M ` Z ) { <. x , y >. | ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) } Z <-> Y ( ( hpG ` G ) ` A ) ( M ` Z ) ) )
46 32 45 mpbid 
 |-  ( ph -> Y ( ( hpG ` G ) ` A ) ( M ` Z ) )