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

Metamath Proof Explorer

Theorem cdleme8

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

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

Proof

Step Hyp Ref Expression
1 cdleme8.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme8.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme8.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme8.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme8.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme8.4 ⊢ 𝐶 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
7 6 oveq2i ⊢ ( 𝑃 ∨ 𝐶 ) = ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) )
8 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝐾 ∈ HL )
9 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
10 8 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝐾 ∈ Lat )
11 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 11 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
13 9 12 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
14 11 4 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
15 14 3ad2ant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
16 11 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
17 10 13 15 16 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
18 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝑊 ∈ 𝐻 )
19 11 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
20 18 19 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
21 11 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) )
22 10 13 15 21 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) )
23 11 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
24 8 9 17 20 22 23 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
25 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
26 1 2 25 4 5 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
27 26 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
28 27 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) )
29 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
30 8 29 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝐾 ∈ OL )
31 11 3 25 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑆 ) )
32 30 17 31 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑆 ) )
33 24 28 32 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( 𝑃 ∨ 𝑆 ) )
34 7 33 eqtrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝐶 ) = ( 𝑃 ∨ 𝑆 ) )