Metamath Proof Explorer

Theorem cdleme23a

Description: Part of proof of Lemma E in Crawley p. 113. (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 cdleme23a ( ( ( ( 𝐾 ∈ 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 8 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ Lat )
10 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑆 ∈ 𝐴 )
11 simp13l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑇 ∈ 𝐴 )
12 1 3 5 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 )
13 8 10 11 12 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 )
14 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑋 ∈ 𝐵 )
15 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐻 )
16 1 6 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
17 15 16 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐵 )
18 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
19 9 14 17 18 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
20 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 )
21 9 13 19 20 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 )
22 1 2 4 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) ) ≤ ( 𝑋 ∧ 𝑊 ) )
23 9 13 19 22 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) ) ≤ ( 𝑋 ∧ 𝑊 ) )
24 1 2 4 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 )
25 9 14 17 24 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 )
26 1 2 9 21 19 17 23 25 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) ) ≤ 𝑊 )
27 7 26 eqbrtrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑉 ≤ 𝑊 )