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

Metamath Proof Explorer

Theorem cdleme20zN

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme20z.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme20z.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme20z.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme20z.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cdleme20zN ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑆 ∨ 𝑅 ) ∧ 𝑇 ) = ( 0. ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 cdleme20z.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme20z.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme20z.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme20z.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
6 5 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ Lat )
7 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ HL )
8 simp22 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑆 ∈ 𝐴 )
9 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑅 ∈ 𝐴 )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
12 7 8 9 11 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑆 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
13 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑇 ∈ 𝐴 )
14 10 4 atbase ⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
16 10 3 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑆 ∨ 𝑅 ) ∧ 𝑇 ) = ( 𝑇 ∧ ( 𝑆 ∨ 𝑅 ) ) )
17 6 12 15 16 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑆 ∨ 𝑅 ) ∧ 𝑇 ) = ( 𝑇 ∧ ( 𝑆 ∨ 𝑅 ) ) )
18 simp3r ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) )
19 hlcvl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CvLat )
20 19 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ CvLat )
21 simp3l ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑆 ≠ 𝑇 )
22 21 necomd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑇 ≠ 𝑆 )
23 1 2 4 cvlatexch1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑇 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑇 ≠ 𝑆 ) → ( 𝑇 ≤ ( 𝑆 ∨ 𝑅 ) → 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) )
24 20 13 9 8 22 23 syl131anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑇 ≤ ( 𝑆 ∨ 𝑅 ) → 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) )
25 18 24 mtod ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ¬ 𝑇 ≤ ( 𝑆 ∨ 𝑅 ) )
26 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
27 26 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ AtLat )
28 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
29 10 1 3 28 4 atnle ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑇 ∈ 𝐴 ∧ ( 𝑆 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( ¬ 𝑇 ≤ ( 𝑆 ∨ 𝑅 ) ↔ ( 𝑇 ∧ ( 𝑆 ∨ 𝑅 ) ) = ( 0. ‘ 𝐾 ) ) )
30 27 13 12 29 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ¬ 𝑇 ≤ ( 𝑆 ∨ 𝑅 ) ↔ ( 𝑇 ∧ ( 𝑆 ∨ 𝑅 ) ) = ( 0. ‘ 𝐾 ) ) )
31 25 30 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑇 ∧ ( 𝑆 ∨ 𝑅 ) ) = ( 0. ‘ 𝐾 ) )
32 17 31 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ¬ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑆 ∨ 𝑅 ) ∧ 𝑇 ) = ( 0. ‘ 𝐾 ) )