Metamath Proof Explorer

Theorem plngrotlem1

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

Ref Expression
Hypotheses plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
plngrot.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ ( 𝑍 𝐿 𝑌 ) ) )
plngrot.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
plngrot.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
plngrot.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
plngrotlem2.4 ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
plngrotlem2.1 ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
plngrotlem2.2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑍 𝐼 𝑊 ) )
plngrotlem2.3 ⊢ ( 𝜑 → 𝑌 ≠ 𝑊 )
plngrotlem1.1 ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
plngrotlem1.2 ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑍 ) )
Assertion plngrotlem1 ( 𝜑 → 𝑆 ∈ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )

Proof

Step Hyp Ref Expression
1 plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
5 plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 plngrot.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ ( 𝑍 𝐿 𝑌 ) ) )
7 plngrot.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
8 plngrot.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
9 plngrot.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
10 plngrotlem2.4 ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
11 plngrotlem2.1 ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
12 plngrotlem2.2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑍 𝐼 𝑊 ) )
13 plngrotlem2.3 ⊢ ( 𝜑 → 𝑌 ≠ 𝑊 )
14 plngrotlem1.1 ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) )
15 plngrotlem1.2 ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑍 ) )
16 8 eldifad ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
17 6 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
18 1 2 3 5 17 7 9 tglinerflx2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
19 elndif ⊢ ( 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) → ¬ 𝑌 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
20 18 19 syl ⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
21 nelne2 ⊢ ( ( 𝑍 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑌 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ) → 𝑍 ≠ 𝑌 )
22 8 20 21 syl2anc ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
23 1 2 3 5 16 7 22 tgelrnln ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑌 ) ∈ ran 𝐿 )
24 1 2 3 4 5 23 6 elplnglnid ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑌 ) ⊆ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )
25 24 sselda ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑆 ∈ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )
26 5 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
27 26 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝐺 ∈ TarskiG )
28 23 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ( 𝑍 𝐿 𝑌 ) ∈ ran 𝐿 )
29 1 2 3 5 17 7 9 tgelrnln ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
30 1 2 3 4 5 29 8 14 plngssp ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
31 30 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑆 ∈ 𝑃 )
32 11 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑊 ∈ 𝑃 )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑆 = 𝑊 ) → 𝑆 = 𝑊 )
34 1 2 3 5 16 7 11 22 12 btwnlng3 ⊢ ( 𝜑 → 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = 𝑊 ) → 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) )
36 33 35 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑆 = 𝑊 ) → 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) )
37 36 stoic1a ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → ¬ 𝑆 = 𝑊 )
38 37 neqned ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑆 ≠ 𝑊 )
39 1 2 3 26 31 32 38 tgelrnln ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → ( 𝑆 𝐿 𝑊 ) ∈ ran 𝐿 )
40 39 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ( 𝑆 𝐿 𝑊 ) ∈ ran 𝐿 )
41 31 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑆 ∈ 𝑃 )
42 32 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑊 ∈ 𝑃 )
43 29 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
44 43 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
45 simplr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) )
46 1 3 2 27 44 45 tglnpt ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑡 ∈ 𝑃 )
47 38 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑆 ≠ 𝑊 )
48 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
49 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) )
50 1 48 2 27 42 46 41 49 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑡 ∈ ( 𝑆 𝐼 𝑊 ) )
51 1 2 3 27 41 42 46 47 50 btwnlng1 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑡 ∈ ( 𝑆 𝐿 𝑊 ) )
52 13 neneqd ⊢ ( 𝜑 → ¬ 𝑌 = 𝑊 )
53 52 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → ¬ 𝑌 = 𝑊 )
54 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
55 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
56 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑍 𝐿 𝑌 ) ∈ ran 𝐿 )
57 16 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑍 ∈ 𝑃 )
58 7 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑌 ∈ 𝑃 )
59 22 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑍 ≠ 𝑌 )
60 1 2 3 26 57 58 59 tglinerflx1 ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑍 ∈ ( 𝑍 𝐿 𝑌 ) )
61 8 eldifbd ⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
62 61 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
63 nelne1 ⊢ ( ( 𝑍 ∈ ( 𝑍 𝐿 𝑌 ) ∧ ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑍 𝐿 𝑌 ) ≠ ( 𝑋 𝐿 𝑌 ) )
64 60 62 63 syl2an2r ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑍 𝐿 𝑌 ) ≠ ( 𝑋 𝐿 𝑌 ) )
65 64 necomd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑌 ) )
66 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
67 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑍 ∈ 𝑃 )
68 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ 𝑃 )
69 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑍 ≠ 𝑌 )
70 1 2 3 54 67 68 69 tglinerflx2 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ ( 𝑍 𝐿 𝑌 ) )
71 66 70 elind ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑌 ) ) )
72 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) )
73 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑊 ∈ 𝑃 )
74 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ ( 𝑍 𝐼 𝑊 ) )
75 1 2 3 54 67 68 73 69 74 btwnlng3 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) )
76 72 75 elind ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑊 ∈ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑌 ) ) )
77 1 2 3 54 55 56 65 71 76 tglineineq ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 = 𝑊 )
78 53 77 mtand ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → ¬ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) )
79 78 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ¬ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) )
80 nelne2 ⊢ ( ( 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ∧ ¬ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑡 ≠ 𝑊 )
81 45 79 80 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑡 ≠ 𝑊 )
82 1 2 3 27 41 42 47 tglinerflx1 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑆 ∈ ( 𝑆 𝐿 𝑊 ) )
83 simpllr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) )
84 nelne1 ⊢ ( ( 𝑆 ∈ ( 𝑆 𝐿 𝑊 ) ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → ( 𝑆 𝐿 𝑊 ) ≠ ( 𝑍 𝐿 𝑌 ) )
85 82 83 84 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ( 𝑆 𝐿 𝑊 ) ≠ ( 𝑍 𝐿 𝑌 ) )
86 85 necomd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ( 𝑍 𝐿 𝑌 ) ≠ ( 𝑆 𝐿 𝑊 ) )
87 34 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) )
88 1 2 3 27 41 42 47 tglinerflx2 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑊 ∈ ( 𝑆 𝐿 𝑊 ) )
89 87 88 elind ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑊 ∈ ( ( 𝑍 𝐿 𝑌 ) ∩ ( 𝑆 𝐿 𝑊 ) ) )
90 1 2 3 27 28 40 86 89 tglineinsn ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ( ( 𝑍 𝐿 𝑌 ) ∩ ( 𝑆 𝐿 𝑊 ) ) = { 𝑊 } )
91 1 2 3 4 27 28 40 51 42 81 90 lnincplng ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ( 𝑆 𝐿 𝑊 ) ⊆ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑡 ) )
92 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑋 ∈ ( 𝑃 ∖ ( 𝑍 𝐿 𝑌 ) ) )
93 17 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑋 ∈ 𝑃 )
94 58 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑌 ∈ 𝑃 )
95 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑋 ≠ 𝑌 )
96 1 2 3 27 93 94 95 tglinerflx1 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) )
97 60 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑍 ∈ ( 𝑍 𝐿 𝑌 ) )
98 61 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
99 98 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
100 97 99 63 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ( 𝑍 𝐿 𝑌 ) ≠ ( 𝑋 𝐿 𝑌 ) )
101 57 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑍 ∈ 𝑃 )
102 59 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑍 ≠ 𝑌 )
103 1 2 3 27 101 94 102 tglinerflx2 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑌 ∈ ( 𝑍 𝐿 𝑌 ) )
104 18 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
105 104 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
106 103 105 elind ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑌 ∈ ( ( 𝑍 𝐿 𝑌 ) ∩ ( 𝑋 𝐿 𝑌 ) ) )
107 1 2 3 27 28 44 100 106 tglineinsn ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ( ( 𝑍 𝐿 𝑌 ) ∩ ( 𝑋 𝐿 𝑌 ) ) = { 𝑌 } )
108 1 2 3 4 27 28 44 96 94 95 107 lnincplng ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ( 𝑋 𝐿 𝑌 ) ⊆ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )
109 108 45 sseldd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑡 ∈ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )
110 27 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
111 46 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑡 ∈ 𝑃 )
112 42 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑊 ∈ 𝑃 )
113 41 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑆 ∈ 𝑃 )
114 81 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑡 ≠ 𝑊 )
115 50 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑡 ∈ ( 𝑆 𝐼 𝑊 ) )
116 1 2 3 110 111 112 113 114 115 btwnlng2 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑆 ∈ ( 𝑡 𝐿 𝑊 ) )
117 57 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑍 ∈ 𝑃 )
118 99 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
119 nelne2 ⊢ ( ( 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ∧ ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑡 ≠ 𝑍 )
120 45 118 119 syl2an2r ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑡 ≠ 𝑍 )
121 120 necomd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑍 ≠ 𝑡 )
122 1 2 3 110 117 111 121 tglinecom ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → ( 𝑍 𝐿 𝑡 ) = ( 𝑡 𝐿 𝑍 ) )
123 22 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
124 1 48 2 5 16 7 11 12 123 tgbtwnne ⊢ ( 𝜑 → 𝑍 ≠ 𝑊 )
125 124 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑍 ≠ 𝑊 )
126 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) )
127 1 2 3 5 16 11 7 124 12 btwnlng1 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑍 𝐿 𝑊 ) )
128 1 2 3 5 16 11 124 7 123 127 tglineelsb2 ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑌 ) )
129 128 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → ( 𝑍 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑌 ) )
130 126 129 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑡 ∈ ( 𝑍 𝐿 𝑊 ) )
131 1 2 3 110 117 112 125 111 120 130 tglineelsb2 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → ( 𝑍 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑡 ) )
132 131 129 eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → ( 𝑍 𝐿 𝑡 ) = ( 𝑍 𝐿 𝑌 ) )
133 81 necomd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑊 ≠ 𝑡 )
134 133 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑊 ≠ 𝑡 )
135 1 2 3 110 111 117 112 120 130 125 lnrot2 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑊 ∈ ( 𝑡 𝐿 𝑍 ) )
136 1 2 3 110 111 117 120 112 134 135 tglineelsb2 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → ( 𝑡 𝐿 𝑍 ) = ( 𝑡 𝐿 𝑊 ) )
137 122 132 136 3eqtr3rd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → ( 𝑡 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑌 ) )
138 116 137 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ∧ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) )
139 83 138 mtand ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ¬ 𝑡 ∈ ( 𝑍 𝐿 𝑌 ) )
140 109 139 eldifd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑡 ∈ ( ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) ∖ ( 𝑍 𝐿 𝑌 ) ) )
141 1 2 3 4 27 28 92 140 plngcp ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) = ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑡 ) )
142 91 141 sseqtrrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → ( 𝑆 𝐿 𝑊 ) ⊆ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )
143 142 82 sseldd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) → 𝑆 ∈ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )
144 eleq1 ⊢ ( 𝑡 = 𝑆 → ( 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ↔ 𝑆 ∈ ( 𝑊 𝐼 𝑆 ) ) )
145 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) )
146 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
147 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑊 ∈ 𝑃 )
148 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑆 ∈ 𝑃 )
149 1 48 2 146 147 148 tgbtwntriv2 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑆 ∈ ( 𝑊 𝐼 𝑆 ) )
150 144 145 149 rspcedvdw ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) )
151 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
152 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
153 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑆 ∈ 𝑃 )
154 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑊 ∈ 𝑃 )
155 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑍 ∈ 𝑃 )
156 15 ord ⊢ ( 𝜑 → ( ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) → 𝑆 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑍 ) )
157 156 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → ( ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) → 𝑆 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑍 ) )
158 157 imp ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑆 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑍 )
159 1 2 3 152 151 153 10 155 158 hpgcom ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑆 )
160 12 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑌 ∈ ( 𝑍 𝐼 𝑊 ) )
161 1 48 2 10 57 32 104 98 78 160 islnoppd ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑍 𝑂 𝑊 )
162 1 2 3 10 26 43 57 31 32 161 lnopp2hpgb ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → ( 𝑆 𝑂 𝑊 ↔ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑆 ) )
163 162 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑆 𝑂 𝑊 ↔ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑆 ) )
164 159 163 mpbird ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑆 𝑂 𝑊 )
165 1 48 2 10 3 151 152 153 154 164 oppcom ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑊 𝑂 𝑆 )
166 1 48 2 10 154 153 islnopp ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑊 𝑂 𝑆 ↔ ( ( ¬ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) ) )
167 165 166 mpbid ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( ( ¬ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) ) )
168 167 simprd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) ∧ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) → ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) )
169 exmidd ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → ( 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ∨ ¬ 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ) )
170 150 168 169 mpjaodan ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) 𝑡 ∈ ( 𝑊 𝐼 𝑆 ) )
171 143 170 r19.29a ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) → 𝑆 ∈ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )
172 exmidd ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ∨ ¬ 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) ) )
173 25 171 172 mpjaodan ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )