Metamath Proof Explorer

Theorem plngrotlem2

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 ⊢ ( 𝜑 → 𝑌 ≠ 𝑊 )
Assertion plngrotlem2 ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) ⊆ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )

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