Metamath Proof Explorer

Theorem plngrotlem2

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 )
Assertion plngrotlem2 
|- ( 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 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 5 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) ) -> G e. TarskiG )
15 6 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) ) -> X e. ( P \ ( Z L Y ) ) )
16 7 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) ) -> Y e. P )
17 8 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) ) -> Z e. ( P \ ( X L Y ) ) )
18 9 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) ) -> X =/= Y )
19 11 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) ) -> W e. P )
20 12 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) ) -> Y e. ( Z I W ) )
21 13 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) ) -> Y =/= W )
22 simpr 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> s e. ( ( X L Y ) E Z ) )
23 22 adantr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) ) -> s e. ( ( X L Y ) E Z ) )
24 simpr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) ) -> ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) )
25 1 2 3 4 14 15 16 17 18 10 19 20 21 23 24 plngrotlem1 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) ) -> s e. ( ( Z L Y ) E X ) )
26 5 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> G e. TarskiG )
27 6 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> X e. ( P \ ( Z L Y ) ) )
28 8 eldifad 
 |-  ( ph -> Z e. P )
29 28 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> Z e. P )
30 7 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> Y e. P )
31 6 eldifad 
 |-  ( ph -> X e. P )
32 1 2 3 5 31 7 9 tglinerflx2 
 |-  ( ph -> Y e. ( X L Y ) )
33 elndif 
 |-  ( Y e. ( X L Y ) -> -. Y e. ( P \ ( X L Y ) ) )
34 32 33 syl 
 |-  ( ph -> -. Y e. ( P \ ( X L Y ) ) )
35 nelne2 
 |-  ( ( Z e. ( P \ ( X L Y ) ) /\ -. Y e. ( P \ ( X L Y ) ) ) -> Z =/= Y )
36 8 34 35 syl2anc 
 |-  ( ph -> Z =/= Y )
37 36 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> Z =/= Y )
38 1 2 3 26 29 30 37 tglinecom 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( Z L Y ) = ( Y L Z ) )
39 11 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> W e. P )
40 13 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> Y =/= W )
41 1 2 3 5 7 11 28 13 12 btwnlng2 
 |-  ( ph -> Z e. ( Y L W ) )
42 41 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> Z e. ( Y L W ) )
43 1 2 3 26 30 39 40 29 37 42 tglineelsb2 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( Y L W ) = ( Y L Z ) )
44 1 2 3 26 30 39 40 tglinecom 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( Y L W ) = ( W L Y ) )
45 38 43 44 3eqtr2d 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( Z L Y ) = ( W L Y ) )
46 45 difeq2d 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( P \ ( Z L Y ) ) = ( P \ ( W L Y ) ) )
47 27 46 eleqtrd 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> X e. ( P \ ( W L Y ) ) )
48 13 neneqd 
 |-  ( ph -> -. Y = W )
49 5 adantr 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> G e. TarskiG )
50 31 adantr 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> X e. P )
51 7 adantr 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> Y e. P )
52 9 adantr 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> X =/= Y )
53 1 2 3 49 50 51 52 tgelrnln 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> ( X L Y ) e. ran L )
54 28 adantr 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> Z e. P )
55 36 adantr 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> Z =/= Y )
56 1 2 3 49 54 51 55 tgelrnln 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> ( Z L Y ) e. ran L )
57 1 2 3 5 28 7 36 tglinerflx1 
 |-  ( ph -> Z e. ( Z L Y ) )
58 57 adantr 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> Z e. ( Z L Y ) )
59 8 eldifbd 
 |-  ( ph -> -. Z e. ( X L Y ) )
60 59 adantr 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> -. Z e. ( X L Y ) )
61 nelne1 
 |-  ( ( Z e. ( Z L Y ) /\ -. Z e. ( X L Y ) ) -> ( Z L Y ) =/= ( X L Y ) )
62 58 60 61 syl2anc 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> ( Z L Y ) =/= ( X L Y ) )
63 62 necomd 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> ( X L Y ) =/= ( Z L Y ) )
64 32 adantr 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> Y e. ( X L Y ) )
65 1 2 3 49 54 51 55 tglinerflx2 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> Y e. ( Z L Y ) )
66 64 65 elind 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> Y e. ( ( X L Y ) i^i ( Z L Y ) ) )
67 simpr 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> W e. ( X L Y ) )
68 11 adantr 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> W e. P )
69 12 adantr 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> Y e. ( Z I W ) )
70 1 2 3 49 54 51 68 55 69 btwnlng3 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> W e. ( Z L Y ) )
71 67 70 elind 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> W e. ( ( X L Y ) i^i ( Z L Y ) ) )
72 1 2 3 49 53 56 63 66 71 tglineineq 
 |-  ( ( ph /\ W e. ( X L Y ) ) -> Y = W )
73 48 72 mtand 
 |-  ( ph -> -. W e. ( X L Y ) )
74 73 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> -. W e. ( X L Y ) )
75 39 74 eldifd 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> W e. ( P \ ( X L Y ) ) )
76 9 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> X =/= Y )
77 eqid 
 |-  ( dist ` G ) = ( dist ` G )
78 1 77 2 5 28 7 11 12 tgbtwncom 
 |-  ( ph -> Y e. ( W I Z ) )
79 78 ad2antrr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> Y e. ( W I Z ) )
80 37 necomd 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> Y =/= Z )
81 1 77 2 10 11 28 32 73 59 78 islnoppd 
 |-  ( ph -> W O Z )
82 81 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> W O Z )
83 5 adantr 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> G e. TarskiG )
84 83 ad2antrr 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> G e. TarskiG )
85 31 adantr 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> X e. P )
86 7 adantr 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> Y e. P )
87 9 adantr 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> X =/= Y )
88 1 2 3 83 85 86 87 tgelrnln 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> ( X L Y ) e. ran L )
89 88 ad2antrr 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> ( X L Y ) e. ran L )
90 8 adantr 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> Z e. ( P \ ( X L Y ) ) )
91 1 2 3 4 83 88 90 22 plngssp 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> s e. P )
92 91 ad2antrr 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> s e. P )
93 11 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> W e. P )
94 28 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> Z e. P )
95 simpr 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> s O Z )
96 1 2 3 10 84 89 92 93 94 95 lnopp2hpgb 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> ( W O Z <-> s ( ( hpG ` G ) ` ( X L Y ) ) W ) )
97 82 96 mpbid 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> s ( ( hpG ` G ) ` ( X L Y ) ) W )
98 97 orcd 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> ( s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) )
99 98 ex 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) -> ( s O Z -> ( s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) ) )
100 99 ex 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> ( -. s e. ( X L Y ) -> ( s O Z -> ( s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) ) ) )
101 100 a2d 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> ( ( -. s e. ( X L Y ) -> s O Z ) -> ( -. s e. ( X L Y ) -> ( s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) ) ) )
102 df-or 
 |-  ( ( s e. ( X L Y ) \/ s O Z ) <-> ( -. s e. ( X L Y ) -> s O Z ) )
103 df-or 
 |-  ( ( s e. ( X L Y ) \/ ( s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) ) <-> ( -. s e. ( X L Y ) -> ( s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) ) )
104 101 102 103 3imtr4g 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> ( ( s e. ( X L Y ) \/ s O Z ) -> ( s e. ( X L Y ) \/ ( s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) ) ) )
105 104 imp 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( s e. ( X L Y ) \/ ( s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) ) )
106 3orass 
 |-  ( ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) <-> ( s e. ( X L Y ) \/ ( s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) ) )
107 105 106 sylibr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) )
108 88 adantr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( X L Y ) e. ran L )
109 91 adantr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> s e. P )
110 1 2 3 4 26 108 75 10 109 elplng 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( s e. ( ( X L Y ) E W ) <-> ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) ) )
111 107 110 mpbird 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> s e. ( ( X L Y ) E W ) )
112 32 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> Y e. ( X L Y ) )
113 59 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> -. Z e. ( X L Y ) )
114 73 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> -. W e. ( X L Y ) )
115 12 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> Y e. ( Z I W ) )
116 1 77 2 10 94 93 112 113 114 115 islnoppd 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> Z O W )
117 1 2 3 10 84 89 94 93 116 lnoppnhpg 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> -. Z ( ( hpG ` G ) ` ( X L Y ) ) W )
118 89 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) /\ W O s ) -> ( X L Y ) e. ran L )
119 84 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) /\ W O s ) -> G e. TarskiG )
120 93 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) /\ W O s ) -> W e. P )
121 92 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) /\ W O s ) -> s e. P )
122 simpr 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) /\ W O s ) -> W O s )
123 1 77 2 10 3 118 119 120 121 122 oppcom 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) /\ W O s ) -> s O W )
124 89 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) /\ s O W ) -> ( X L Y ) e. ran L )
125 84 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) /\ s O W ) -> G e. TarskiG )
126 92 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) /\ s O W ) -> s e. P )
127 93 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) /\ s O W ) -> W e. P )
128 simpr 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) /\ s O W ) -> s O W )
129 1 77 2 10 3 124 125 126 127 128 oppcom 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) /\ s O W ) -> W O s )
130 123 129 impbida 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> ( W O s <-> s O W ) )
131 1 77 2 10 3 89 84 92 94 95 oppcom 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> Z O s )
132 1 2 3 10 84 89 94 93 92 131 lnopp2hpgb 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> ( W O s <-> Z ( ( hpG ` G ) ` ( X L Y ) ) W ) )
133 130 132 bitr3d 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> ( s O W <-> Z ( ( hpG ` G ) ` ( X L Y ) ) W ) )
134 117 133 mtbird 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) /\ s O Z ) -> -. s O W )
135 134 ex 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ -. s e. ( X L Y ) ) -> ( s O Z -> -. s O W ) )
136 135 ex 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> ( -. s e. ( X L Y ) -> ( s O Z -> -. s O W ) ) )
137 136 a2d 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> ( ( -. s e. ( X L Y ) -> s O Z ) -> ( -. s e. ( X L Y ) -> -. s O W ) ) )
138 137 imp 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( -. s e. ( X L Y ) -> s O Z ) ) -> ( -. s e. ( X L Y ) -> -. s O W ) )
139 102 138 sylan2b 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( -. s e. ( X L Y ) -> -. s O W ) )
140 139 imp 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) /\ -. s e. ( X L Y ) ) -> -. s O W )
141 df-3or 
 |-  ( ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) <-> ( ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W ) \/ s O W ) )
142 orcom 
 |-  ( ( ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W ) \/ s O W ) <-> ( s O W \/ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W ) ) )
143 df-or 
 |-  ( ( s O W \/ ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W ) ) <-> ( -. s O W -> ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W ) ) )
144 141 142 143 3bitri 
 |-  ( ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W \/ s O W ) <-> ( -. s O W -> ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W ) ) )
145 107 144 sylib 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( -. s O W -> ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W ) ) )
146 145 imp 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) /\ -. s O W ) -> ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W ) )
147 df-or 
 |-  ( ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W ) <-> ( -. s e. ( X L Y ) -> s ( ( hpG ` G ) ` ( X L Y ) ) W ) )
148 146 147 sylib 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) /\ -. s O W ) -> ( -. s e. ( X L Y ) -> s ( ( hpG ` G ) ` ( X L Y ) ) W ) )
149 148 imp 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) /\ -. s O W ) /\ -. s e. ( X L Y ) ) -> s ( ( hpG ` G ) ` ( X L Y ) ) W )
150 149 an32s 
 |-  ( ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) /\ -. s e. ( X L Y ) ) /\ -. s O W ) -> s ( ( hpG ` G ) ` ( X L Y ) ) W )
151 140 150 mpdan 
 |-  ( ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) /\ -. s e. ( X L Y ) ) -> s ( ( hpG ` G ) ` ( X L Y ) ) W )
152 151 ex 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( -. s e. ( X L Y ) -> s ( ( hpG ` G ) ` ( X L Y ) ) W ) )
153 152 147 sylibr 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) W ) )
154 1 2 3 4 26 47 30 75 76 10 29 79 80 111 153 plngrotlem1 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> s e. ( ( W L Y ) E X ) )
155 45 eqcomd 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( W L Y ) = ( Z L Y ) )
156 155 oveq1d 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> ( ( W L Y ) E X ) = ( ( Z L Y ) E X ) )
157 154 156 eleqtrd 
 |-  ( ( ( ph /\ s e. ( ( X L Y ) E Z ) ) /\ ( s e. ( X L Y ) \/ s O Z ) ) -> s e. ( ( Z L Y ) E X ) )
158 1 2 3 4 83 88 90 10 91 elplng 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> ( s e. ( ( X L Y ) E Z ) <-> ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z \/ s O Z ) ) )
159 22 158 mpbid 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z \/ s O Z ) )
160 3orass 
 |-  ( ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z \/ s O Z ) <-> ( s e. ( X L Y ) \/ ( s ( ( hpG ` G ) ` ( X L Y ) ) Z \/ s O Z ) ) )
161 orordi 
 |-  ( ( s e. ( X L Y ) \/ ( s ( ( hpG ` G ) ` ( X L Y ) ) Z \/ s O Z ) ) <-> ( ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) \/ ( s e. ( X L Y ) \/ s O Z ) ) )
162 160 161 bitri 
 |-  ( ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z \/ s O Z ) <-> ( ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) \/ ( s e. ( X L Y ) \/ s O Z ) ) )
163 159 162 sylib 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> ( ( s e. ( X L Y ) \/ s ( ( hpG ` G ) ` ( X L Y ) ) Z ) \/ ( s e. ( X L Y ) \/ s O Z ) ) )
164 25 157 163 mpjaodan 
 |-  ( ( ph /\ s e. ( ( X L Y ) E Z ) ) -> s e. ( ( Z L Y ) E X ) )
165 164 ex 
 |-  ( ph -> ( s e. ( ( X L Y ) E Z ) -> s e. ( ( Z L Y ) E X ) ) )
166 165 ssrdv 
 |-  ( ph -> ( ( X L Y ) E Z ) C_ ( ( Z L Y ) E X ) )