Metamath Proof Explorer

Theorem ps-2b

Description: Variation of projective geometry axiom ps-2 . (Contributed by NM, 3-Jul-2012)

Ref Expression
Hypotheses ps-2b.l ⊢ ≤ = ( le ‘ 𝐾 )
ps-2b.j ⊢ ∨ = ( join ‘ 𝐾 )
ps-2b.m ⊢ ∧ = ( meet ‘ 𝐾 )
ps-2b.z ⊢ 0 = ( 0. ‘ 𝐾 )
ps-2b.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion ps-2b ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 ps-2b.l ⊢ ≤ = ( le ‘ 𝐾 )
2 ps-2b.j ⊢ ∨ = ( join ‘ 𝐾 )
3 ps-2b.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 ps-2b.z ⊢ 0 = ( 0. ‘ 𝐾 )
5 ps-2b.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → 𝐾 ∈ HL )
7 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → 𝑃 ∈ 𝐴 )
8 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → 𝑄 ∈ 𝐴 )
9 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → 𝑅 ∈ 𝐴 )
10 7 8 9 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) )
11 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → 𝑆 ∈ 𝐴 )
12 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → 𝑇 ∈ 𝐴 )
13 11 12 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) )
14 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
15 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → 𝑆 ≠ 𝑇 )
16 14 15 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ) )
17 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) )
18 1 2 5 ps-2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) )
19 6 10 13 16 17 18 syl32anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) )
20 simp111 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ HL )
21 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
22 20 21 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ AtLat )
23 20 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ Lat )
24 simp112 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑃 ∈ 𝐴 )
25 simp121 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑅 ∈ 𝐴 )
26 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
27 26 2 5 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
28 20 24 25 27 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
29 simp122 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑆 ∈ 𝐴 )
30 simp123 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑇 ∈ 𝐴 )
31 26 2 5 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
32 20 29 30 31 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
33 26 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
34 23 28 32 33 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
35 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑢 ∈ 𝐴 )
36 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) )
37 26 5 atbase ⊢ ( 𝑢 ∈ 𝐴 → 𝑢 ∈ ( Base ‘ 𝐾 ) )
38 35 37 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑢 ∈ ( Base ‘ 𝐾 ) )
39 26 1 3 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑢 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ↔ 𝑢 ≤ ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ) )
40 23 38 28 32 39 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ↔ 𝑢 ≤ ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ) )
41 36 40 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑢 ≤ ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) )
42 26 1 4 5 atlen0 ⊢ ( ( ( 𝐾 ∈ AtLat ∧ ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≠ 0 )
43 22 34 35 41 42 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ∧ 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≠ 0 )
44 43 rexlimdv3a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≠ 0 ) )
45 19 44 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≠ 0 )