Metamath Proof Explorer

Theorem cdleme42a

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 3-Mar-2013)

Ref Expression
Hypotheses cdleme42.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdleme42.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme42.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme42.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme42.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme42.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme42.v ⊢ 𝑉 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
Assertion cdleme42a ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑅 ∨ 𝑆 ) = ( 𝑅 ∨ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 cdleme42.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdleme42.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdleme42.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdleme42.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdleme42.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdleme42.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 cdleme42.v ⊢ 𝑉 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
8 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
9 2 3 8 5 6 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑅 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
10 9 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑅 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
11 10 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑅 ∨ 𝑊 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) )
12 7 oveq2i ⊢ ( 𝑅 ∨ 𝑉 ) = ( 𝑅 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) )
13 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
14 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑅 ∈ 𝐴 )
15 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑆 ∈ 𝐴 )
16 1 3 5 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑆 ) ∈ 𝐵 )
17 13 14 15 16 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑅 ∨ 𝑆 ) ∈ 𝐵 )
18 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
19 1 6 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
20 18 19 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐵 )
21 2 3 5 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → 𝑅 ≤ ( 𝑅 ∨ 𝑆 ) )
22 13 14 15 21 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑅 ≤ ( 𝑅 ∨ 𝑆 ) )
23 1 2 3 4 5 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑅 ∨ 𝑆 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝑅 ≤ ( 𝑅 ∨ 𝑆 ) ) → ( 𝑅 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑅 ∨ 𝑊 ) ) )
24 13 14 17 20 22 23 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑅 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑅 ∨ 𝑊 ) ) )
25 12 24 eqtr2id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑅 ∨ 𝑊 ) ) = ( 𝑅 ∨ 𝑉 ) )
26 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
27 13 26 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝐾 ∈ OL )
28 1 4 8 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑅 ∨ 𝑆 ) ∈ 𝐵 ) → ( ( 𝑅 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑅 ∨ 𝑆 ) )
29 27 17 28 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑅 ∨ 𝑆 ) )
30 11 25 29 3eqtr3rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑅 ∨ 𝑆 ) = ( 𝑅 ∨ 𝑉 ) )