Metamath Proof Explorer

Theorem plngrotlem1

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 )
plngrotlem2.4 
|- 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 ) ) }
plngrotlem2.1 
|- ( ph -> W e. P )
plngrotlem2.2 
|- ( ph -> Y e. ( Z I W ) )
plngrotlem2.3 
|- ( ph -> Y =/= W )
plngrotlem1.1 
|- ( ph -> S e. ( ( X L Y ) E Z ) )
plngrotlem1.2 
|- ( ph -> ( S e. ( X L Y ) \/ S ( ( hpG ` G ) ` ( X L Y ) ) Z ) )
Assertion plngrotlem1 
|- ( ph -> S e. ( ( 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 plngrotlem2.4 
 |-  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 plngrotlem2.1 
 |-  ( ph -> W e. P )
12 plngrotlem2.2 
 |-  ( ph -> Y e. ( Z I W ) )
13 plngrotlem2.3 
 |-  ( ph -> Y =/= W )
14 plngrotlem1.1 
 |-  ( ph -> S e. ( ( X L Y ) E Z ) )
15 plngrotlem1.2 
 |-  ( ph -> ( S e. ( X L Y ) \/ S ( ( hpG ` G ) ` ( X L Y ) ) Z ) )
16 8 eldifad 
 |-  ( ph -> Z e. P )
17 6 eldifad 
 |-  ( ph -> X e. P )
18 1 2 3 5 17 7 9 tglinerflx2 
 |-  ( ph -> Y e. ( X L Y ) )
19 elndif 
 |-  ( Y e. ( X L Y ) -> -. Y e. ( P \ ( X L Y ) ) )
20 18 19 syl 
 |-  ( ph -> -. Y e. ( P \ ( X L Y ) ) )
21 nelne2 
 |-  ( ( Z e. ( P \ ( X L Y ) ) /\ -. Y e. ( P \ ( X L Y ) ) ) -> Z =/= Y )
22 8 20 21 syl2anc 
 |-  ( ph -> Z =/= Y )
23 1 2 3 5 16 7 22 tgelrnln 
 |-  ( ph -> ( Z L Y ) e. ran L )
24 1 2 3 4 5 23 6 elplnglnid 
 |-  ( ph -> ( Z L Y ) C_ ( ( Z L Y ) E X ) )
25 24 sselda 
 |-  ( ( ph /\ S e. ( Z L Y ) ) -> S e. ( ( Z L Y ) E X ) )
26 5 adantr 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> G e. TarskiG )
27 26 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> G e. TarskiG )
28 23 ad3antrrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> ( Z L Y ) e. ran L )
29 1 2 3 5 17 7 9 tgelrnln 
 |-  ( ph -> ( X L Y ) e. ran L )
30 1 2 3 4 5 29 8 14 plngssp 
 |-  ( ph -> S e. P )
31 30 adantr 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> S e. P )
32 11 adantr 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> W e. P )
33 simpr 
 |-  ( ( ph /\ S = W ) -> S = W )
34 1 2 3 5 16 7 11 22 12 btwnlng3 
 |-  ( ph -> W e. ( Z L Y ) )
35 34 adantr 
 |-  ( ( ph /\ S = W ) -> W e. ( Z L Y ) )
36 33 35 eqeltrd 
 |-  ( ( ph /\ S = W ) -> S e. ( Z L Y ) )
37 36 stoic1a 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> -. S = W )
38 37 neqned 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> S =/= W )
39 1 2 3 26 31 32 38 tgelrnln 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> ( S L W ) e. ran L )
40 39 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> ( S L W ) e. ran L )
41 31 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> S e. P )
42 32 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> W e. P )
43 29 adantr 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> ( X L Y ) e. ran L )
44 43 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> ( X L Y ) e. ran L )
45 simplr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> t e. ( X L Y ) )
46 1 3 2 27 44 45 tglnpt 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> t e. P )
47 38 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> S =/= W )
48 eqid 
 |-  ( dist ` G ) = ( dist ` G )
49 simpr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> t e. ( W I S ) )
50 1 48 2 27 42 46 41 49 tgbtwncom 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> t e. ( S I W ) )
51 1 2 3 27 41 42 46 47 50 btwnlng1 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> t e. ( S L W ) )
52 13 neneqd 
 |-  ( ph -> -. Y = W )
53 52 adantr 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> -. Y = W )
54 5 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> G e. TarskiG )
55 29 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> ( X L Y ) e. ran L )
56 23 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> ( Z L Y ) e. ran L )
57 16 adantr 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> Z e. P )
58 7 adantr 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> Y e. P )
59 22 adantr 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> Z =/= Y )
60 1 2 3 26 57 58 59 tglinerflx1 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> Z e. ( Z L Y ) )
61 8 eldifbd 
 |-  ( ph -> -. Z e. ( X L Y ) )
62 61 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> -. Z e. ( X L Y ) )
63 nelne1 
 |-  ( ( Z e. ( Z L Y ) /\ -. Z e. ( X L Y ) ) -> ( Z L Y ) =/= ( X L Y ) )
64 60 62 63 syl2an2r 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> ( Z L Y ) =/= ( X L Y ) )
65 64 necomd 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> ( X L Y ) =/= ( Z L Y ) )
66 18 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> Y e. ( X L Y ) )
67 16 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> Z e. P )
68 7 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> Y e. P )
69 22 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> Z =/= Y )
70 1 2 3 54 67 68 69 tglinerflx2 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> Y e. ( Z L Y ) )
71 66 70 elind 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> Y e. ( ( X L Y ) i^i ( Z L Y ) ) )
72 simpr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> W e. ( X L Y ) )
73 11 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> W e. P )
74 12 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> Y e. ( Z I W ) )
75 1 2 3 54 67 68 73 69 74 btwnlng3 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> W e. ( Z L Y ) )
76 72 75 elind 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> W e. ( ( X L Y ) i^i ( Z L Y ) ) )
77 1 2 3 54 55 56 65 71 76 tglineineq 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ W e. ( X L Y ) ) -> Y = W )
78 53 77 mtand 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> -. W e. ( X L Y ) )
79 78 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> -. W e. ( X L Y ) )
80 nelne2 
 |-  ( ( t e. ( X L Y ) /\ -. W e. ( X L Y ) ) -> t =/= W )
81 45 79 80 syl2anc 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> t =/= W )
82 1 2 3 27 41 42 47 tglinerflx1 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> S e. ( S L W ) )
83 simpllr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> -. S e. ( Z L Y ) )
84 nelne1 
 |-  ( ( S e. ( S L W ) /\ -. S e. ( Z L Y ) ) -> ( S L W ) =/= ( Z L Y ) )
85 82 83 84 syl2anc 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> ( S L W ) =/= ( Z L Y ) )
86 85 necomd 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> ( Z L Y ) =/= ( S L W ) )
87 34 ad3antrrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> W e. ( Z L Y ) )
88 1 2 3 27 41 42 47 tglinerflx2 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> W e. ( S L W ) )
89 87 88 elind 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> W e. ( ( Z L Y ) i^i ( S L W ) ) )
90 1 2 3 27 28 40 86 89 tglineinsn 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> ( ( Z L Y ) i^i ( S L W ) ) = { W } )
91 1 2 3 4 27 28 40 51 42 81 90 lnincplng 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> ( S L W ) C_ ( ( Z L Y ) E t ) )
92 6 ad3antrrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> X e. ( P \ ( Z L Y ) ) )
93 17 ad3antrrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> X e. P )
94 58 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> Y e. P )
95 9 ad3antrrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> X =/= Y )
96 1 2 3 27 93 94 95 tglinerflx1 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> X e. ( X L Y ) )
97 60 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> Z e. ( Z L Y ) )
98 61 adantr 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> -. Z e. ( X L Y ) )
99 98 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> -. Z e. ( X L Y ) )
100 97 99 63 syl2anc 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> ( Z L Y ) =/= ( X L Y ) )
101 57 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> Z e. P )
102 59 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> Z =/= Y )
103 1 2 3 27 101 94 102 tglinerflx2 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> Y e. ( Z L Y ) )
104 18 adantr 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> Y e. ( X L Y ) )
105 104 ad2antrr 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> Y e. ( X L Y ) )
106 103 105 elind 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> Y e. ( ( Z L Y ) i^i ( X L Y ) ) )
107 1 2 3 27 28 44 100 106 tglineinsn 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> ( ( Z L Y ) i^i ( X L Y ) ) = { Y } )
108 1 2 3 4 27 28 44 96 94 95 107 lnincplng 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> ( X L Y ) C_ ( ( Z L Y ) E X ) )
109 108 45 sseldd 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> t e. ( ( Z L Y ) E X ) )
110 27 adantr 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> G e. TarskiG )
111 46 adantr 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> t e. P )
112 42 adantr 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> W e. P )
113 41 adantr 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> S e. P )
114 81 adantr 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> t =/= W )
115 50 adantr 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> t e. ( S I W ) )
116 1 2 3 110 111 112 113 114 115 btwnlng2 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> S e. ( t L W ) )
117 57 ad3antrrr 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> Z e. P )
118 99 adantr 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> -. Z e. ( X L Y ) )
119 nelne2 
 |-  ( ( t e. ( X L Y ) /\ -. Z e. ( X L Y ) ) -> t =/= Z )
120 45 118 119 syl2an2r 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> t =/= Z )
121 120 necomd 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> Z =/= t )
122 1 2 3 110 117 111 121 tglinecom 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> ( Z L t ) = ( t L Z ) )
123 22 necomd 
 |-  ( ph -> Y =/= Z )
124 1 48 2 5 16 7 11 12 123 tgbtwnne 
 |-  ( ph -> Z =/= W )
125 124 ad4antr 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> Z =/= W )
126 simpr 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> t e. ( Z L Y ) )
127 1 2 3 5 16 11 7 124 12 btwnlng1 
 |-  ( ph -> Y e. ( Z L W ) )
128 1 2 3 5 16 11 124 7 123 127 tglineelsb2 
 |-  ( ph -> ( Z L W ) = ( Z L Y ) )
129 128 ad4antr 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> ( Z L W ) = ( Z L Y ) )
130 126 129 eleqtrrd 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> t e. ( Z L W ) )
131 1 2 3 110 117 112 125 111 120 130 tglineelsb2 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> ( Z L W ) = ( Z L t ) )
132 131 129 eqtr3d 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> ( Z L t ) = ( Z L Y ) )
133 81 necomd 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> W =/= t )
134 133 adantr 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> W =/= t )
135 1 2 3 110 111 117 112 120 130 125 lnrot2 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> W e. ( t L Z ) )
136 1 2 3 110 111 117 120 112 134 135 tglineelsb2 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> ( t L Z ) = ( t L W ) )
137 122 132 136 3eqtr3rd 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> ( t L W ) = ( Z L Y ) )
138 116 137 eleqtrd 
 |-  ( ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) /\ t e. ( Z L Y ) ) -> S e. ( Z L Y ) )
139 83 138 mtand 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> -. t e. ( Z L Y ) )
140 109 139 eldifd 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> t e. ( ( ( Z L Y ) E X ) \ ( Z L Y ) ) )
141 1 2 3 4 27 28 92 140 plngcp 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> ( ( Z L Y ) E X ) = ( ( Z L Y ) E t ) )
142 91 141 sseqtrrd 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> ( S L W ) C_ ( ( Z L Y ) E X ) )
143 142 82 sseldd 
 |-  ( ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ t e. ( X L Y ) ) /\ t e. ( W I S ) ) -> S e. ( ( Z L Y ) E X ) )
144 eleq1 
 |-  ( t = S -> ( t e. ( W I S ) <-> S e. ( W I S ) ) )
145 simpr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ S e. ( X L Y ) ) -> S e. ( X L Y ) )
146 5 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ S e. ( X L Y ) ) -> G e. TarskiG )
147 11 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ S e. ( X L Y ) ) -> W e. P )
148 30 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ S e. ( X L Y ) ) -> S e. P )
149 1 48 2 146 147 148 tgbtwntriv2 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ S e. ( X L Y ) ) -> S e. ( W I S ) )
150 144 145 149 rspcedvdw 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ S e. ( X L Y ) ) -> E. t e. ( X L Y ) t e. ( W I S ) )
151 29 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> ( X L Y ) e. ran L )
152 5 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> G e. TarskiG )
153 30 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> S e. P )
154 11 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> W e. P )
155 16 ad2antrr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> Z e. P )
156 15 ord 
 |-  ( ph -> ( -. S e. ( X L Y ) -> S ( ( hpG ` G ) ` ( X L Y ) ) Z ) )
157 156 adantr 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> ( -. S e. ( X L Y ) -> S ( ( hpG ` G ) ` ( X L Y ) ) Z ) )
158 157 imp 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> S ( ( hpG ` G ) ` ( X L Y ) ) Z )
159 1 2 3 152 151 153 10 155 158 hpgcom 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> Z ( ( hpG ` G ) ` ( X L Y ) ) S )
160 12 adantr 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> Y e. ( Z I W ) )
161 1 48 2 10 57 32 104 98 78 160 islnoppd 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> Z O W )
162 1 2 3 10 26 43 57 31 32 161 lnopp2hpgb 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> ( S O W <-> Z ( ( hpG ` G ) ` ( X L Y ) ) S ) )
163 162 adantr 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> ( S O W <-> Z ( ( hpG ` G ) ` ( X L Y ) ) S ) )
164 159 163 mpbird 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> S O W )
165 1 48 2 10 3 151 152 153 154 164 oppcom 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> W O S )
166 1 48 2 10 154 153 islnopp 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> ( W O S <-> ( ( -. W e. ( X L Y ) /\ -. S e. ( X L Y ) ) /\ E. t e. ( X L Y ) t e. ( W I S ) ) ) )
167 165 166 mpbid 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> ( ( -. W e. ( X L Y ) /\ -. S e. ( X L Y ) ) /\ E. t e. ( X L Y ) t e. ( W I S ) ) )
168 167 simprd 
 |-  ( ( ( ph /\ -. S e. ( Z L Y ) ) /\ -. S e. ( X L Y ) ) -> E. t e. ( X L Y ) t e. ( W I S ) )
169 exmidd 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> ( S e. ( X L Y ) \/ -. S e. ( X L Y ) ) )
170 150 168 169 mpjaodan 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> E. t e. ( X L Y ) t e. ( W I S ) )
171 143 170 r19.29a 
 |-  ( ( ph /\ -. S e. ( Z L Y ) ) -> S e. ( ( Z L Y ) E X ) )
172 exmidd 
 |-  ( ph -> ( S e. ( Z L Y ) \/ -. S e. ( Z L Y ) ) )
173 25 171 172 mpjaodan 
 |-  ( ph -> S e. ( ( Z L Y ) E X ) )