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

Metamath Proof Explorer

Theorem cdleme15b

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, showing, in their notation, (p \/ s_1) /\ (q \/ s_1)=s_1. We represent s_1 with C . (Contributed by NM, 10-Oct-2012)

Ref Expression
Hypotheses cdleme12.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme12.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme12.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme12.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme12.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme12.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
cdleme12.f ⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
cdleme12.g ⊢ 𝐺 = ( ( 𝑇 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 ) ) )
cdleme15.c ⊢ 𝐶 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
cdleme15.x ⊢ 𝑋 = ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 )
Assertion cdleme15b ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑃 ∨ 𝐶 ) ∧ ( 𝑄 ∨ 𝐶 ) ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 cdleme12.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme12.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme12.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme12.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme12.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme12.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7 cdleme12.f ⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
8 cdleme12.g ⊢ 𝐺 = ( ( 𝑇 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 ) ) )
9 cdleme15.c ⊢ 𝐶 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
10 cdleme15.x ⊢ 𝑋 = ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 )
11 9 oveq2i ⊢ ( 𝑃 ∨ 𝐶 ) = ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) )
12 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ HL )
13 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑃 ∈ 𝐴 )
14 simp21l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑆 ∈ 𝐴 )
15 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
16 15 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
17 12 13 14 16 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
18 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑊 ∈ 𝐻 )
19 15 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
20 18 19 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
21 1 2 4 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) )
22 12 13 14 21 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) )
23 15 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
24 12 13 17 20 22 23 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
25 11 24 eqtrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑃 ∨ 𝐶 ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
26 25 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑃 ∨ 𝐶 ) ∧ 𝑄 ) = ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) ∧ 𝑄 ) )
27 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
28 12 27 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ OL )
29 12 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ Lat )
30 15 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
31 13 30 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
32 15 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
33 29 31 20 32 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑃 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
34 simp13l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑄 ∈ 𝐴 )
35 15 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
36 34 35 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
37 15 3 latmrot ⊢ ( ( 𝐾 ∈ OL ∧ ( ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) ∧ 𝑄 ) = ( ( 𝑄 ∧ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
38 28 17 33 36 37 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) ∧ 𝑄 ) = ( ( 𝑄 ∧ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
39 simp31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
40 simp23l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑃 ≠ 𝑄 )
41 40 necomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑄 ≠ 𝑃 )
42 1 2 4 hlatexch1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑄 ≠ 𝑃 ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) → 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) )
43 12 34 14 13 41 42 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) → 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) )
44 39 43 mtod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) )
45 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
46 12 45 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ AtLat )
47 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
48 15 1 3 47 4 atnle ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ↔ ( 𝑄 ∧ ( 𝑃 ∨ 𝑆 ) ) = ( 0. ‘ 𝐾 ) ) )
49 46 34 17 48 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ↔ ( 𝑄 ∧ ( 𝑃 ∨ 𝑆 ) ) = ( 0. ‘ 𝐾 ) ) )
50 44 49 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑄 ∧ ( 𝑃 ∨ 𝑆 ) ) = ( 0. ‘ 𝐾 ) )
51 50 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑄 ∧ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑃 ∨ 𝑊 ) ) = ( ( 0. ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
52 15 3 47 olm02 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑊 ) ) = ( 0. ‘ 𝐾 ) )
53 28 33 52 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 0. ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑊 ) ) = ( 0. ‘ 𝐾 ) )
54 38 51 53 3eqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 0. ‘ 𝐾 ) = ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) ∧ 𝑄 ) )
55 26 54 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑃 ∨ 𝐶 ) ∧ 𝑄 ) = ( 0. ‘ 𝐾 ) )
56 55 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( ( 𝑃 ∨ 𝐶 ) ∧ 𝑄 ) ∨ 𝐶 ) = ( ( 0. ‘ 𝐾 ) ∨ 𝐶 ) )
57 15 2 3 4 5 9 cdleme9b ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) ) → 𝐶 ∈ ( Base ‘ 𝐾 ) )
58 12 13 14 18 57 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐶 ∈ ( Base ‘ 𝐾 ) )
59 15 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) )
60 29 31 58 59 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑃 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) )
61 15 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) → 𝐶 ≤ ( 𝑃 ∨ 𝐶 ) )
62 29 31 58 61 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐶 ≤ ( 𝑃 ∨ 𝐶 ) )
63 15 1 2 3 4 atmod2i2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝐶 ≤ ( 𝑃 ∨ 𝐶 ) ) → ( ( ( 𝑃 ∨ 𝐶 ) ∧ 𝑄 ) ∨ 𝐶 ) = ( ( 𝑃 ∨ 𝐶 ) ∧ ( 𝑄 ∨ 𝐶 ) ) )
64 12 34 60 58 62 63 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( ( 𝑃 ∨ 𝐶 ) ∧ 𝑄 ) ∨ 𝐶 ) = ( ( 𝑃 ∨ 𝐶 ) ∧ ( 𝑄 ∨ 𝐶 ) ) )
65 15 2 47 olj02 ⊢ ( ( 𝐾 ∈ OL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ∨ 𝐶 ) = 𝐶 )
66 28 58 65 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 0. ‘ 𝐾 ) ∨ 𝐶 ) = 𝐶 )
67 56 64 66 3eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑃 ∨ 𝐶 ) ∧ ( 𝑄 ∨ 𝐶 ) ) = 𝐶 )