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

Metamath Proof Explorer

Theorem cdleme23b

Description: Part of proof of Lemma E in Crawley p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012)

Ref Expression
Hypotheses cdleme23.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdleme23.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme23.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme23.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme23.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme23.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme23.v ⊢ 𝑉 = ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) )
Assertion cdleme23b ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑉 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 cdleme23.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdleme23.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdleme23.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdleme23.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdleme23.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdleme23.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 cdleme23.v ⊢ 𝑉 = ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) )
8 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ HL )
9 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
10 8 9 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ OL )
11 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑆 ∈ 𝐴 )
12 simp13l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑇 ∈ 𝐴 )
13 1 3 5 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 )
14 8 11 12 13 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 )
15 8 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ Lat )
16 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑋 ∈ 𝐵 )
17 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐻 )
18 1 6 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
19 17 18 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐵 )
20 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
21 15 16 19 20 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
22 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 )
23 15 14 21 22 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 )
24 1 4 latmassOLD ⊢ ( ( 𝐾 ∈ OL ∧ ( ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ) ∧ 𝑊 ) = ( ( 𝑆 ∨ 𝑇 ) ∧ ( ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑊 ) ) )
25 10 14 23 19 24 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ) ∧ 𝑊 ) = ( ( 𝑆 ∨ 𝑇 ) ∧ ( ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑊 ) ) )
26 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) )
27 15 14 21 26 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) )
28 1 2 4 latleeqm1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ↔ ( ( 𝑆 ∨ 𝑇 ) ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ) = ( 𝑆 ∨ 𝑇 ) ) )
29 15 14 23 28 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ↔ ( ( 𝑆 ∨ 𝑇 ) ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ) = ( 𝑆 ∨ 𝑇 ) ) )
30 27 29 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ) = ( 𝑆 ∨ 𝑇 ) )
31 30 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ∧ ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ) ∧ 𝑊 ) = ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) )
32 1 5 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ 𝐵 )
33 11 32 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑆 ∈ 𝐵 )
34 1 5 atbase ⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ 𝐵 )
35 12 34 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑇 ∈ 𝐵 )
36 1 3 latjjdir ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) = ( ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) ∨ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
37 15 33 35 21 36 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) = ( ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) ∨ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
38 simp32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 )
39 simp33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 )
40 38 39 oveq12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) ∨ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ) = ( 𝑋 ∨ 𝑋 ) )
41 1 3 latjidm ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑋 ) = 𝑋 )
42 15 16 41 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∨ 𝑋 ) = 𝑋 )
43 37 40 42 3eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 )
44 43 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑊 ) = ( 𝑋 ∧ 𝑊 ) )
45 44 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ ( ( ( 𝑆 ∨ 𝑇 ) ∨ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑊 ) ) = ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) ) )
46 25 31 45 3eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) = ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) ) )
47 simp12r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ¬ 𝑆 ≤ 𝑊 )
48 simp31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑆 ≠ 𝑇 )
49 2 3 4 5 6 lhpat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ∈ 𝐴 )
50 8 17 11 47 12 48 49 syl222anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ∈ 𝐴 )
51 46 50 eqeltrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐴 )
52 7 51 eqeltrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑉 ∈ 𝐴 )