Metamath Proof Explorer

Theorem lnssplnglem

Description: Lemma for lnssplng . (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 )
lnssplnglem.x 
|- ( ph -> X e. ( A E R ) )
lnssplnglem.y 
|- ( ph -> Y e. ( A E R ) )
lnssplnglem.1 
|- ( ph -> X =/= Y )
lnssplnglem.2 
|- ( ph -> A e. ran L )
lnssplnglem.3 
|- ( ph -> R e. ( P \ A ) )
lnssplnglem.4 
|- ( ph -> A =/= ( X L Y ) )
lnssplnglem.5 
|- ( ph -> -. Y e. A )
Assertion lnssplnglem 
|- ( ph -> ( ( X L Y ) C_ ( A E R ) /\ E. s e. ( P \ ( X L Y ) ) ( A E R ) = ( ( X L Y ) E s ) ) )

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 lnssplnglem.x 
 |-  ( ph -> X e. ( A E R ) )
7 lnssplnglem.y 
 |-  ( ph -> Y e. ( A E R ) )
8 lnssplnglem.1 
 |-  ( ph -> X =/= Y )
9 lnssplnglem.2 
 |-  ( ph -> A e. ran L )
10 lnssplnglem.3 
 |-  ( ph -> R e. ( P \ A ) )
11 lnssplnglem.4 
 |-  ( ph -> A =/= ( X L Y ) )
12 lnssplnglem.5 
 |-  ( ph -> -. Y e. A )
13 5 adantr 
 |-  ( ( ph /\ z e. A ) -> G e. TarskiG )
14 13 adantr 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> G e. TarskiG )
15 1 2 3 4 5 9 10 6 plngssp 
 |-  ( ph -> X e. P )
16 15 adantr 
 |-  ( ( ph /\ z e. A ) -> X e. P )
17 1 2 3 4 5 9 10 7 plngssp 
 |-  ( ph -> Y e. P )
18 17 adantr 
 |-  ( ( ph /\ z e. A ) -> Y e. P )
19 8 adantr 
 |-  ( ( ph /\ z e. A ) -> X =/= Y )
20 1 2 3 13 16 18 19 tgelrnln 
 |-  ( ( ph /\ z e. A ) -> ( X L Y ) e. ran L )
21 20 adantr 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> ( X L Y ) e. ran L )
22 9 ad2antrr 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> A e. ran L )
23 simplr 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> z e. A )
24 1 3 2 14 22 23 tglnpt 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> z e. P )
25 simpr 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> -. z e. ( X L Y ) )
26 24 25 eldifd 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> z e. ( P \ ( X L Y ) ) )
27 1 2 3 4 14 21 26 elplnglnid 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> ( X L Y ) C_ ( ( X L Y ) E z ) )
28 16 adantr 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> X e. P )
29 14 adantr 
 |-  ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ X e. ( z L Y ) ) -> G e. TarskiG )
30 28 adantr 
 |-  ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ X e. ( z L Y ) ) -> X e. P )
31 18 ad2antrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ X e. ( z L Y ) ) -> Y e. P )
32 24 adantr 
 |-  ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ X e. ( z L Y ) ) -> z e. P )
33 19 ad2antrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ X e. ( z L Y ) ) -> X =/= Y )
34 1 2 3 5 15 17 8 tglinerflx2 
 |-  ( ph -> Y e. ( X L Y ) )
35 34 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ X e. ( z L Y ) ) -> Y e. ( X L Y ) )
36 simplr 
 |-  ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ X e. ( z L Y ) ) -> -. z e. ( X L Y ) )
37 nelne2 
 |-  ( ( Y e. ( X L Y ) /\ -. z e. ( X L Y ) ) -> Y =/= z )
38 35 36 37 syl2anc 
 |-  ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ X e. ( z L Y ) ) -> Y =/= z )
39 simpr 
 |-  ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ X e. ( z L Y ) ) -> X e. ( z L Y ) )
40 1 2 3 29 31 32 30 38 39 lncom 
 |-  ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ X e. ( z L Y ) ) -> X e. ( Y L z ) )
41 1 2 3 29 30 31 32 33 40 38 lnrot2 
 |-  ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ X e. ( z L Y ) ) -> z e. ( X L Y ) )
42 25 41 mtand 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> -. X e. ( z L Y ) )
43 28 42 eldifd 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> X e. ( P \ ( z L Y ) ) )
44 18 adantr 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> Y e. P )
45 19 adantr 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> X =/= Y )
46 1 2 3 4 14 43 44 26 45 plngrot 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> ( ( X L Y ) E z ) = ( ( z L Y ) E X ) )
47 46 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> ( ( X L Y ) E z ) = ( ( z L Y ) E X ) )
48 5 ad4antr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> G e. TarskiG )
49 24 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> z e. P )
50 17 ad4antr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> Y e. P )
51 23 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> z e. A )
52 12 ad4antr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> -. Y e. A )
53 nelne2 
 |-  ( ( z e. A /\ -. Y e. A ) -> z =/= Y )
54 51 52 53 syl2anc 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> z =/= Y )
55 1 2 3 48 49 50 54 tgelrnln 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> ( z L Y ) e. ran L )
56 9 ad4antr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> A e. ran L )
57 simplr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> w e. ( A \ ( Y L z ) ) )
58 57 eldifad 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> w e. A )
59 1 3 2 48 56 58 tglnpt 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> w e. P )
60 57 eldifbd 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> -. w e. ( Y L z ) )
61 1 2 3 48 49 50 54 tglinecom 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> ( z L Y ) = ( Y L z ) )
62 60 61 neleqtrrd 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> -. w e. ( z L Y ) )
63 59 62 eldifd 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> w e. ( P \ ( z L Y ) ) )
64 6 ad4antr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> X e. ( A E R ) )
65 simpr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> w =/= z )
66 1 2 3 48 59 49 65 65 56 58 51 tglinethru 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> A = ( w L z ) )
67 52 66 neleqtrd 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> -. Y e. ( w L z ) )
68 50 67 eldifd 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> Y e. ( P \ ( w L z ) ) )
69 59 60 eldifd 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> w e. ( P \ ( Y L z ) ) )
70 54 necomd 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> Y =/= z )
71 1 2 3 4 48 68 49 69 70 plngrot 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> ( ( Y L z ) E w ) = ( ( w L z ) E Y ) )
72 61 oveq1d 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> ( ( z L Y ) E w ) = ( ( Y L z ) E w ) )
73 66 oveq1d 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> ( A E Y ) = ( ( w L z ) E Y ) )
74 71 72 73 3eqtr4d 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> ( ( z L Y ) E w ) = ( A E Y ) )
75 7 12 eldifd 
 |-  ( ph -> Y e. ( ( A E R ) \ A ) )
76 1 2 3 4 5 9 10 75 plngcp 
 |-  ( ph -> ( A E R ) = ( A E Y ) )
77 76 ad4antr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> ( A E R ) = ( A E Y ) )
78 74 77 eqtr4d 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> ( ( z L Y ) E w ) = ( A E R ) )
79 64 78 eleqtrrd 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> X e. ( ( z L Y ) E w ) )
80 42 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> -. X e. ( z L Y ) )
81 79 80 eldifd 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> X e. ( ( ( z L Y ) E w ) \ ( z L Y ) ) )
82 1 2 3 4 48 55 63 81 plngcp 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> ( ( z L Y ) E w ) = ( ( z L Y ) E X ) )
83 47 82 78 3eqtr2rd 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) /\ w e. ( A \ ( Y L z ) ) ) /\ w =/= z ) -> ( A E R ) = ( ( X L Y ) E z ) )
84 34 ad2antrr 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> Y e. ( X L Y ) )
85 84 25 37 syl2anc 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> Y =/= z )
86 1 2 3 14 44 24 85 tgelrnln 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> ( Y L z ) e. ran L )
87 1 2 3 14 44 24 85 tglinerflx1 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> Y e. ( Y L z ) )
88 12 ad2antrr 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> -. Y e. A )
89 nelne1 
 |-  ( ( Y e. ( Y L z ) /\ -. Y e. A ) -> ( Y L z ) =/= A )
90 87 88 89 syl2anc 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> ( Y L z ) =/= A )
91 90 necomd 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> A =/= ( Y L z ) )
92 1 2 3 14 22 86 23 91 tglnpt4 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> E. w e. ( A \ ( Y L z ) ) w =/= z )
93 83 92 r19.29a 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> ( A E R ) = ( ( X L Y ) E z ) )
94 27 93 sseqtrrd 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> ( X L Y ) C_ ( A E R ) )
95 oveq2 
 |-  ( s = z -> ( ( X L Y ) E s ) = ( ( X L Y ) E z ) )
96 95 eqeq2d 
 |-  ( s = z -> ( ( A E R ) = ( ( X L Y ) E s ) <-> ( A E R ) = ( ( X L Y ) E z ) ) )
97 96 26 93 rspcedvdw 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> E. s e. ( P \ ( X L Y ) ) ( A E R ) = ( ( X L Y ) E s ) )
98 94 97 jca 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. ( X L Y ) ) -> ( ( X L Y ) C_ ( A E R ) /\ E. s e. ( P \ ( X L Y ) ) ( A E R ) = ( ( X L Y ) E s ) ) )
99 11 neneqd 
 |-  ( ph -> -. A = ( X L Y ) )
100 5 adantr 
 |-  ( ( ph /\ A C_ ( X L Y ) ) -> G e. TarskiG )
101 9 adantr 
 |-  ( ( ph /\ A C_ ( X L Y ) ) -> A e. ran L )
102 15 adantr 
 |-  ( ( ph /\ A C_ ( X L Y ) ) -> X e. P )
103 17 adantr 
 |-  ( ( ph /\ A C_ ( X L Y ) ) -> Y e. P )
104 8 adantr 
 |-  ( ( ph /\ A C_ ( X L Y ) ) -> X =/= Y )
105 1 2 3 100 102 103 104 tgelrnln 
 |-  ( ( ph /\ A C_ ( X L Y ) ) -> ( X L Y ) e. ran L )
106 simpr 
 |-  ( ( ph /\ A C_ ( X L Y ) ) -> A C_ ( X L Y ) )
107 3 100 101 105 106 tglinesseq 
 |-  ( ( ph /\ A C_ ( X L Y ) ) -> A = ( X L Y ) )
108 99 107 mtand 
 |-  ( ph -> -. A C_ ( X L Y ) )
109 nssrex 
 |-  ( -. A C_ ( X L Y ) <-> E. z e. A -. z e. ( X L Y ) )
110 108 109 sylib 
 |-  ( ph -> E. z e. A -. z e. ( X L Y ) )
111 98 110 r19.29a 
 |-  ( ph -> ( ( X L Y ) C_ ( A E R ) /\ E. s e. ( P \ ( X L Y ) ) ( A E R ) = ( ( X L Y ) E s ) ) )