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

Metamath Proof Explorer

Theorem cdleme10

Description: Part of proof of Lemma E in Crawley p. 113, 2nd paragraph on p. 114. D represents s_2. In their notation, we prove s \/ s_2 = s \/ r. (Contributed by NM, 9-Jun-2012)

Ref Expression
Hypotheses cdleme10.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme10.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme10.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme10.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme10.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme10.d ⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
Assertion cdleme10 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ 𝐷 ) = ( 𝑆 ∨ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 cdleme10.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme10.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme10.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme10.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme10.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme10.d ⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
7 6 oveq2i ⊢ ( 𝑆 ∨ 𝐷 ) = ( 𝑆 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) )
8 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
9 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑆 ∈ 𝐴 )
10 simp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑅 ∈ 𝐴 )
11 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 11 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
13 8 10 9 12 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
14 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
15 11 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
16 14 15 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
17 8 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
18 11 4 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
19 18 3ad2ant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
20 11 4 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
21 9 20 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
22 11 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → 𝑆 ≤ ( 𝑅 ∨ 𝑆 ) )
23 17 19 21 22 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑆 ≤ ( 𝑅 ∨ 𝑆 ) )
24 11 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑆 ) ) → ( 𝑆 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑊 ) ) )
25 8 9 13 16 23 24 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑊 ) ) )
26 11 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ∨ 𝑆 ) = ( 𝑆 ∨ 𝑅 ) )
27 17 19 21 26 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑅 ∨ 𝑆 ) = ( 𝑆 ∨ 𝑅 ) )
28 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
29 1 2 28 4 5 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
30 29 3adant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
31 27 30 oveq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑊 ) ) = ( ( 𝑆 ∨ 𝑅 ) ∧ ( 1. ‘ 𝐾 ) ) )
32 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
33 8 32 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝐾 ∈ OL )
34 11 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑆 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
35 17 21 19 34 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
36 11 3 28 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑆 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑆 ∨ 𝑅 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑆 ∨ 𝑅 ) )
37 33 35 36 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( ( 𝑆 ∨ 𝑅 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑆 ∨ 𝑅 ) )
38 25 31 37 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( 𝑆 ∨ 𝑅 ) )
39 7 38 eqtrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ 𝐷 ) = ( 𝑆 ∨ 𝑅 ) )