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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑠 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 )