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

Metamath Proof Explorer

Theorem cdleme30a

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 9-Feb-2013)

Ref Expression
Hypotheses cdleme30.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdleme30.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme30.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme30.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme30.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme30.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion cdleme30a ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 )

Proof

Step Hyp Ref Expression
1 cdleme30.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdleme30.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdleme30.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdleme30.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdleme30.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdleme30.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝐾 ∈ HL )
8 7 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝐾 ∈ Lat )
9 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑠 ∈ 𝐴 )
10 1 5 atbase ⊢ ( 𝑠 ∈ 𝐴 → 𝑠 ∈ 𝐵 )
11 9 10 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑠 ∈ 𝐵 )
12 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑌 ∈ 𝐵 )
13 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑊 ∈ 𝐻 )
14 1 6 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
15 13 14 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑊 ∈ 𝐵 )
16 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 )
17 8 12 15 16 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 )
18 simp22l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑋 ∈ 𝐵 )
19 1 3 latjass ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑠 ∈ 𝐵 ∧ ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ∨ 𝑋 ) = ( 𝑠 ∨ ( ( 𝑌 ∧ 𝑊 ) ∨ 𝑋 ) ) )
20 8 11 17 18 19 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ∨ 𝑋 ) = ( 𝑠 ∨ ( ( 𝑌 ∧ 𝑊 ) ∨ 𝑋 ) ) )
21 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 )
22 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑋 ≤ 𝑌 )
23 1 2 4 latmlem1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑌 → ( 𝑋 ∧ 𝑊 ) ≤ ( 𝑌 ∧ 𝑊 ) ) )
24 8 18 12 15 23 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑋 ≤ 𝑌 → ( 𝑋 ∧ 𝑊 ) ≤ ( 𝑌 ∧ 𝑊 ) ) )
25 22 24 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑋 ∧ 𝑊 ) ≤ ( 𝑌 ∧ 𝑊 ) )
26 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
27 8 18 15 26 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
28 1 2 3 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ∧ ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑊 ) ≤ ( 𝑌 ∧ 𝑊 ) → ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) ≤ ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ) )
29 8 27 17 11 28 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( ( 𝑋 ∧ 𝑊 ) ≤ ( 𝑌 ∧ 𝑊 ) → ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) ≤ ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ) )
30 25 29 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) ≤ ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) )
31 21 30 eqbrtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑋 ≤ ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) )
32 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑠 ∈ 𝐵 ∧ ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 ) → ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ∈ 𝐵 )
33 8 11 17 32 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ∈ 𝐵 )
34 1 2 3 latleeqj2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ∈ 𝐵 ) → ( 𝑋 ≤ ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ↔ ( ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ∨ 𝑋 ) = ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ) )
35 8 18 33 34 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑋 ≤ ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ↔ ( ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ∨ 𝑋 ) = ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ) )
36 31 35 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) ∨ 𝑋 ) = ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) )
37 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
38 1 2 3 4 6 lhpmod2i2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝑌 ∧ 𝑊 ) ∨ 𝑋 ) = ( 𝑌 ∧ ( 𝑊 ∨ 𝑋 ) ) )
39 37 12 18 22 38 syl121anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( ( 𝑌 ∧ 𝑊 ) ∨ 𝑋 ) = ( 𝑌 ∧ ( 𝑊 ∨ 𝑋 ) ) )
40 39 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑠 ∨ ( ( 𝑌 ∧ 𝑊 ) ∨ 𝑋 ) ) = ( 𝑠 ∨ ( 𝑌 ∧ ( 𝑊 ∨ 𝑋 ) ) ) )
41 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) )
42 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
43 1 2 3 42 6 lhpj1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑋 ) = ( 1. ‘ 𝐾 ) )
44 37 41 43 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑊 ∨ 𝑋 ) = ( 1. ‘ 𝐾 ) )
45 44 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑌 ∧ ( 𝑊 ∨ 𝑋 ) ) = ( 𝑌 ∧ ( 1. ‘ 𝐾 ) ) )
46 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
47 7 46 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝐾 ∈ OL )
48 1 4 42 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∧ ( 1. ‘ 𝐾 ) ) = 𝑌 )
49 47 12 48 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑌 ∧ ( 1. ‘ 𝐾 ) ) = 𝑌 )
50 45 49 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑌 ∧ ( 𝑊 ∨ 𝑋 ) ) = 𝑌 )
51 50 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑠 ∨ ( 𝑌 ∧ ( 𝑊 ∨ 𝑋 ) ) ) = ( 𝑠 ∨ 𝑌 ) )
52 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑠 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → 𝑠 ≤ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) )
53 8 11 27 52 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑠 ≤ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) )
54 53 21 breqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑠 ≤ 𝑋 )
55 1 2 8 11 18 12 54 22 lattrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑠 ≤ 𝑌 )
56 1 2 3 latleeqj1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑠 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑠 ≤ 𝑌 ↔ ( 𝑠 ∨ 𝑌 ) = 𝑌 ) )
57 8 11 12 56 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑠 ≤ 𝑌 ↔ ( 𝑠 ∨ 𝑌 ) = 𝑌 ) )
58 55 57 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑠 ∨ 𝑌 ) = 𝑌 )
59 40 51 58 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑠 ∨ ( ( 𝑌 ∧ 𝑊 ) ∨ 𝑋 ) ) = 𝑌 )
60 20 36 59 3eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 )