Metamath Proof Explorer

Theorem plngmiropp

Description: Given a line A and a point X not on A , then a point Y on the plane defined by A and X is either opposite to X , or opposite to the mirror point of X by any point Z of A . (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses plngmiropp.p 
|- P = ( Base ` G )
plngmiropp.i 
|- I = ( Itv ` G )
plngmiropp.l 
|- L = ( LineG ` G )
plngmiropp.e 
|- E = ( PlnG ` G )
plngmiropp.s 
|- S = ( pInvG ` G )
plngmiropp.m 
|- M = ( S ` Z )
plngmiropp.o 
|- O = { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) }
plngmiropp.g 
|- ( ph -> G e. TarskiG )
plngmiropp.a 
|- ( ph -> A e. ran L )
plngmiropp.x 
|- ( ph -> X e. ( P \ A ) )
plngmiropp.y 
|- ( ph -> Y e. ( ( A E X ) \ A ) )
plngmiropp.z 
|- ( ph -> Z e. A )
Assertion plngmiropp 
|- ( ph -> ( X O Y \/ ( M ` X ) O Y ) )

Proof

Step Hyp Ref Expression
1 plngmiropp.p 
 |-  P = ( Base ` G )
2 plngmiropp.i 
 |-  I = ( Itv ` G )
3 plngmiropp.l 
 |-  L = ( LineG ` G )
4 plngmiropp.e 
 |-  E = ( PlnG ` G )
5 plngmiropp.s 
 |-  S = ( pInvG ` G )
6 plngmiropp.m 
 |-  M = ( S ` Z )
7 plngmiropp.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) }
8 plngmiropp.g 
 |-  ( ph -> G e. TarskiG )
9 plngmiropp.a 
 |-  ( ph -> A e. ran L )
10 plngmiropp.x 
 |-  ( ph -> X e. ( P \ A ) )
11 plngmiropp.y 
 |-  ( ph -> Y e. ( ( A E X ) \ A ) )
12 plngmiropp.z 
 |-  ( ph -> Z e. A )
13 eqid 
 |-  ( dist ` G ) = ( dist ` G )
14 9 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) X ) -> A e. ran L )
15 8 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) X ) -> G e. TarskiG )
16 11 eldifad 
 |-  ( ph -> Y e. ( A E X ) )
17 1 2 3 4 8 9 10 16 plngssp 
 |-  ( ph -> Y e. P )
18 17 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) X ) -> Y e. P )
19 1 3 2 8 9 12 tglnpt 
 |-  ( ph -> Z e. P )
20 10 eldifad 
 |-  ( ph -> X e. P )
21 1 13 2 3 5 8 19 6 20 mircl 
 |-  ( ph -> ( M ` X ) e. P )
22 21 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) X ) -> ( M ` X ) e. P )
23 20 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) X ) -> X e. P )
24 simpr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) X ) -> Y ( ( hpG ` G ) ` A ) X )
25 1 2 3 15 14 18 7 23 24 hpgcom 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) X ) -> X ( ( hpG ` G ) ` A ) Y )
26 1 2 5 6 7 8 9 12 10 3 oppmir 
 |-  ( ph -> X O ( M ` X ) )
27 1 2 3 7 8 9 20 17 21 26 lnopp2hpgb 
 |-  ( ph -> ( Y O ( M ` X ) <-> X ( ( hpG ` G ) ` A ) Y ) )
28 27 biimpar 
 |-  ( ( ph /\ X ( ( hpG ` G ) ` A ) Y ) -> Y O ( M ` X ) )
29 25 28 syldan 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) X ) -> Y O ( M ` X ) )
30 1 13 2 7 3 14 15 18 22 29 oppcom 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) X ) -> ( M ` X ) O Y )
31 9 adantr 
 |-  ( ( ph /\ Y O X ) -> A e. ran L )
32 8 adantr 
 |-  ( ( ph /\ Y O X ) -> G e. TarskiG )
33 17 adantr 
 |-  ( ( ph /\ Y O X ) -> Y e. P )
34 20 adantr 
 |-  ( ( ph /\ Y O X ) -> X e. P )
35 simpr 
 |-  ( ( ph /\ Y O X ) -> Y O X )
36 1 13 2 7 3 31 32 33 34 35 oppcom 
 |-  ( ( ph /\ Y O X ) -> X O Y )
37 1 2 3 4 8 9 10 7 17 elplng 
 |-  ( ph -> ( Y e. ( A E X ) <-> ( Y e. A \/ Y ( ( hpG ` G ) ` A ) X \/ Y O X ) ) )
38 16 37 mpbid 
 |-  ( ph -> ( Y e. A \/ Y ( ( hpG ` G ) ` A ) X \/ Y O X ) )
39 3orass 
 |-  ( ( Y e. A \/ Y ( ( hpG ` G ) ` A ) X \/ Y O X ) <-> ( Y e. A \/ ( Y ( ( hpG ` G ) ` A ) X \/ Y O X ) ) )
40 38 39 sylib 
 |-  ( ph -> ( Y e. A \/ ( Y ( ( hpG ` G ) ` A ) X \/ Y O X ) ) )
41 11 eldifbd 
 |-  ( ph -> -. Y e. A )
42 40 41 orcnd 
 |-  ( ph -> ( Y ( ( hpG ` G ) ` A ) X \/ Y O X ) )
43 30 36 42 orim12da 
 |-  ( ph -> ( ( M ` X ) O Y \/ X O Y ) )
44 43 orcomd 
 |-  ( ph -> ( X O Y \/ ( M ` X ) O Y ) )