Theorem cdleme22d

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

	Ref	Expression
Hypotheses	cdleme22.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme22.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme22.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme22.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme22.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	cdleme22d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑉 = ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		cdleme22.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme22.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme22.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme22.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme22.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		simp3r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) )
7		simp1l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝐾 ∈ HL )
8		simp22l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑇 ∈ 𝐴 )
9		simp23l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑉 ∈ 𝐴 )
10	1 2 4	hlatlej1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → 𝑇 ≤ ( 𝑇 ∨ 𝑉 ) )
11	7 8 9 10	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑇 ≤ ( 𝑇 ∨ 𝑉 ) )
12	7	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝐾 ∈ Lat )
13		simp21l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑆 ∈ 𝐴 )
14		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
15	14 4	atbase	⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
16	13 15	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
17	14 4	atbase	⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
18	8 17	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
19	14 2 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( 𝑇 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
20	7 8 9 19	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( 𝑇 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
21	14 1 2	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑇 ≤ ( 𝑇 ∨ 𝑉 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑇 ∨ 𝑉 ) ) )
22	12 16 18 20 21	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑇 ≤ ( 𝑇 ∨ 𝑉 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑇 ∨ 𝑉 ) ) )
23	6 11 22	mpbi2and	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑇 ∨ 𝑉 ) )
24	14 2 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
25	7 13 8 24	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
26		simp1r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑊 ∈ 𝐻 )
27	14 5	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
28	26 27	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
29	14 1 3	latmlem1	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑇 ∨ 𝑉 ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ 𝑊 ) ) )
30	12 25 20 28 29	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑇 ∨ 𝑉 ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ 𝑊 ) ) )
31	23 30	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ 𝑊 ) )
32		simp1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
33		simp22	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) )
34		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
35	1 3 34 4 5	lhpmat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) → ( 𝑇 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
36	32 33 35	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( 𝑇 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
37	36	oveq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( ( 𝑇 ∧ 𝑊 ) ∨ 𝑉 ) = ( ( 0. ‘ 𝐾 ) ∨ 𝑉 ) )
38		simp23r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑉 ≤ 𝑊 )
39	14 1 2 3 4	atmod4i1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑉 ≤ 𝑊 ) → ( ( 𝑇 ∧ 𝑊 ) ∨ 𝑉 ) = ( ( 𝑇 ∨ 𝑉 ) ∧ 𝑊 ) )
40	7 9 18 28 38 39	syl131anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( ( 𝑇 ∧ 𝑊 ) ∨ 𝑉 ) = ( ( 𝑇 ∨ 𝑉 ) ∧ 𝑊 ) )
41		hlol	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
42	7 41	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝐾 ∈ OL )
43	14 4	atbase	⊢ ( 𝑉 ∈ 𝐴 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
44	9 43	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑉 ∈ ( Base ‘ 𝐾 ) )
45	14 2 34	olj02	⊢ ( ( 𝐾 ∈ OL ∧ 𝑉 ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ∨ 𝑉 ) = 𝑉 )
46	42 44 45	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( ( 0. ‘ 𝐾 ) ∨ 𝑉 ) = 𝑉 )
47	37 40 46	3eqtr3d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( ( 𝑇 ∨ 𝑉 ) ∧ 𝑊 ) = 𝑉 )
48	31 47	breqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ≤ 𝑉 )
49		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
50	7 49	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝐾 ∈ AtLat )
51		simp21r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ¬ 𝑆 ≤ 𝑊 )
52		simp3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑆 ≠ 𝑇 )
53	1 2 3 4 5	lhpat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ∈ 𝐴 )
54	7 26 13 51 8 52 53	syl222anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ∈ 𝐴 )
55	1 4	atcmp	⊢ ( ( 𝐾 ∈ AtLat ∧ ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ≤ 𝑉 ↔ ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) = 𝑉 ) )
56	50 54 9 55	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) ≤ 𝑉 ↔ ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) = 𝑉 ) )
57	48 56	mpbid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) = 𝑉 )
58	57	eqcomd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑆 ≠ 𝑇 ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ) ) → 𝑉 = ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) )