Metamath Proof Explorer

Theorem plngrotlem3

Description: Lemma for plngrot . (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses plngval.p 
|- P = ( Base ` G )
plngval.i 
|- I = ( Itv ` G )
plngval.1 
|- L = ( LineG ` G )
plngval.e 
|- E = ( PlnG ` G )
plngval.g 
|- ( ph -> G e. TarskiG )
plngrot.x 
|- ( ph -> X e. ( P \ ( Z L Y ) ) )
plngrot.y 
|- ( ph -> Y e. P )
plngrot.z 
|- ( ph -> Z e. ( P \ ( X L Y ) ) )
plngrot.1 
|- ( ph -> X =/= Y )
plngrotlem3.1 
|- O = { <. a , b >. | ( ( a e. ( P \ ( X L Y ) ) /\ b e. ( P \ ( X L Y ) ) ) /\ E. t e. ( X L Y ) t e. ( a I b ) ) }
Assertion plngrotlem3 
|- ( ph -> ( ( X L Y ) E Z ) C_ ( ( Z L Y ) E X ) )

Proof

Step Hyp Ref Expression
1 plngval.p 
 |-  P = ( Base ` G )
2 plngval.i 
 |-  I = ( Itv ` G )
3 plngval.1 
 |-  L = ( LineG ` G )
4 plngval.e 
 |-  E = ( PlnG ` G )
5 plngval.g 
 |-  ( ph -> G e. TarskiG )
6 plngrot.x 
 |-  ( ph -> X e. ( P \ ( Z L Y ) ) )
7 plngrot.y 
 |-  ( ph -> Y e. P )
8 plngrot.z 
 |-  ( ph -> Z e. ( P \ ( X L Y ) ) )
9 plngrot.1 
 |-  ( ph -> X =/= Y )
10 plngrotlem3.1 
 |-  O = { <. a , b >. | ( ( a e. ( P \ ( X L Y ) ) /\ b e. ( P \ ( X L Y ) ) ) /\ E. t e. ( X L Y ) t e. ( a I b ) ) }
11 5 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ Y e. ( Z I w ) ) /\ Y =/= w ) -> G e. TarskiG )
12 6 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ Y e. ( Z I w ) ) /\ Y =/= w ) -> X e. ( P \ ( Z L Y ) ) )
13 7 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ Y e. ( Z I w ) ) /\ Y =/= w ) -> Y e. P )
14 8 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ Y e. ( Z I w ) ) /\ Y =/= w ) -> Z e. ( P \ ( X L Y ) ) )
15 9 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ Y e. ( Z I w ) ) /\ Y =/= w ) -> X =/= Y )
16 simpllr 
 |-  ( ( ( ( ph /\ w e. P ) /\ Y e. ( Z I w ) ) /\ Y =/= w ) -> w e. P )
17 simplr 
 |-  ( ( ( ( ph /\ w e. P ) /\ Y e. ( Z I w ) ) /\ Y =/= w ) -> Y e. ( Z I w ) )
18 simpr 
 |-  ( ( ( ( ph /\ w e. P ) /\ Y e. ( Z I w ) ) /\ Y =/= w ) -> Y =/= w )
19 1 2 3 4 11 12 13 14 15 10 16 17 18 plngrotlem2 
 |-  ( ( ( ( ph /\ w e. P ) /\ Y e. ( Z I w ) ) /\ Y =/= w ) -> ( ( X L Y ) E Z ) C_ ( ( Z L Y ) E X ) )
20 19 anasss 
 |-  ( ( ( ph /\ w e. P ) /\ ( Y e. ( Z I w ) /\ Y =/= w ) ) -> ( ( X L Y ) E Z ) C_ ( ( Z L Y ) E X ) )
21 eqid 
 |-  ( dist ` G ) = ( dist ` G )
22 8 eldifad 
 |-  ( ph -> Z e. P )
23 1 fvexi 
 |-  P e. _V
24 23 a1i 
 |-  ( ph -> P e. _V )
25 6 eldifad 
 |-  ( ph -> X e. P )
26 24 25 7 9 nehash2 
 |-  ( ph -> 2 <_ ( # ` P ) )
27 1 21 2 5 22 7 26 tgbtwndiff 
 |-  ( ph -> E. w e. P ( Y e. ( Z I w ) /\ Y =/= w ) )
28 20 27 r19.29a 
 |-  ( ph -> ( ( X L Y ) E Z ) C_ ( ( Z L Y ) E X ) )