This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemednpq

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. D represents s_2. (Contributed by NM, 18-Nov-2012)

Ref Expression
Hypotheses cdlemeda.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemeda.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemeda.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdlemeda.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemeda.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemeda.d ⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
Assertion cdlemednpq ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 cdlemeda.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdlemeda.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdlemeda.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdlemeda.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdlemeda.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdlemeda.d ⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
7 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ HL )
8 7 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ Lat )
9 simp23l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑅 ∈ 𝐴 )
10 simp31l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ∈ 𝐴 )
11 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 11 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
13 7 9 10 12 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
14 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑊 ∈ 𝐻 )
15 11 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
16 14 15 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
17 11 1 3 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ≤ 𝑊 )
18 8 13 16 17 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ≤ 𝑊 )
19 6 18 eqbrtrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐷 ≤ 𝑊 )
20 simp23r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑅 ≤ 𝑊 )
21 nbrne2 ⊢ ( ( 𝐷 ≤ 𝑊 ∧ ¬ 𝑅 ≤ 𝑊 ) → 𝐷 ≠ 𝑅 )
22 19 20 21 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐷 ≠ 𝑅 )
23 8 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐾 ∈ Lat )
24 13 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
25 16 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
26 11 1 3 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ≤ ( 𝑅 ∨ 𝑆 ) )
27 23 24 25 26 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ≤ ( 𝑅 ∨ 𝑆 ) )
28 6 27 eqbrtrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐷 ≤ ( 𝑅 ∨ 𝑆 ) )
29 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) )
30 simp31r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑆 ≤ 𝑊 )
31 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
32 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
33 1 2 3 4 5 6 cdlemeda ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐷 ∈ 𝐴 )
34 7 14 10 30 9 31 32 33 syl223anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐷 ∈ 𝐴 )
35 11 4 atbase ⊢ ( 𝐷 ∈ 𝐴 → 𝐷 ∈ ( Base ‘ 𝐾 ) )
36 34 35 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐷 ∈ ( Base ‘ 𝐾 ) )
37 36 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐷 ∈ ( Base ‘ 𝐾 ) )
38 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ∈ 𝐴 )
39 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑄 ∈ 𝐴 )
40 11 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
41 7 38 39 40 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
42 41 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
43 11 1 3 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐷 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝐷 ≤ ( 𝑅 ∨ 𝑆 ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ 𝐷 ≤ ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) )
44 23 37 24 42 43 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝐷 ≤ ( 𝑅 ∨ 𝑆 ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ 𝐷 ≤ ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) )
45 28 29 44 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐷 ≤ ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) )
46 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
47 7 46 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ AtLat )
48 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
49 11 1 3 48 4 atnle ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑆 ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) ) )
50 47 10 41 49 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑆 ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) ) )
51 32 50 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑆 ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) )
52 51 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ∨ ( 𝑆 ∧ ( 𝑃 ∨ 𝑄 ) ) ) = ( 𝑅 ∨ ( 0. ‘ 𝐾 ) ) )
53 11 4 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
54 10 53 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
55 11 1 2 3 4 atmod1i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑅 ∨ ( 𝑆 ∧ ( 𝑃 ∨ 𝑄 ) ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) )
56 7 9 54 41 31 55 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ∨ ( 𝑆 ∧ ( 𝑃 ∨ 𝑄 ) ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) )
57 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
58 7 57 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ OL )
59 11 4 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
60 9 59 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
61 11 2 48 olj01 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ∨ ( 0. ‘ 𝐾 ) ) = 𝑅 )
62 58 60 61 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ∨ ( 0. ‘ 𝐾 ) ) = 𝑅 )
63 52 56 62 3eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = 𝑅 )
64 63 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = 𝑅 )
65 45 64 breqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐷 ≤ 𝑅 )
66 65 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) → 𝐷 ≤ 𝑅 ) )
67 1 4 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝐷 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝐷 ≤ 𝑅 ↔ 𝐷 = 𝑅 ) )
68 47 34 9 67 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐷 ≤ 𝑅 ↔ 𝐷 = 𝑅 ) )
69 66 68 sylibd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) → 𝐷 = 𝑅 ) )
70 69 necon3ad ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐷 ≠ 𝑅 → ¬ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) ) )
71 22 70 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝐷 ≤ ( 𝑃 ∨ 𝑄 ) )