Metamath Proof Explorer

Theorem cdlemc1

Description: Part of proof of Lemma C in Crawley p. 112. TODO: shorten with atmod3i1 ? (Contributed by NM, 29-May-2012)

Ref Expression
Hypotheses cdlemc1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemc1.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemc1.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemc1.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdlemc1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemc1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion cdlemc1 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) ) = ( 𝑃 ∨ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 cdlemc1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemc1.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdlemc1.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdlemc1.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdlemc1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemc1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
8 7 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
9 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
10 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
11 9 10 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐵 )
12 simp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐵 )
13 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑋 ) ∈ 𝐵 )
14 8 11 12 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑋 ) ∈ 𝐵 )
15 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
16 1 6 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
17 15 16 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐵 )
18 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑋 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) ∈ 𝐵 )
19 8 14 17 18 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) ∈ 𝐵 )
20 1 3 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) ∈ 𝐵 ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) ) = ( ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) ∨ 𝑃 ) )
21 8 11 19 20 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) ) = ( ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) ∨ 𝑃 ) )
22 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑋 ) )
23 8 11 12 22 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑋 ) )
24 1 2 3 4 5 atmod2i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑋 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝑃 ≤ ( 𝑃 ∨ 𝑋 ) ) → ( ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) ∨ 𝑃 ) = ( ( 𝑃 ∨ 𝑋 ) ∧ ( 𝑊 ∨ 𝑃 ) ) )
25 7 9 14 17 23 24 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) ∨ 𝑃 ) = ( ( 𝑃 ∨ 𝑋 ) ∧ ( 𝑊 ∨ 𝑃 ) ) )
26 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
27 2 3 26 5 6 lhpjat1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑃 ) = ( 1. ‘ 𝐾 ) )
28 27 3adant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑃 ) = ( 1. ‘ 𝐾 ) )
29 28 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑋 ) ∧ ( 𝑊 ∨ 𝑃 ) ) = ( ( 𝑃 ∨ 𝑋 ) ∧ ( 1. ‘ 𝐾 ) ) )
30 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
31 7 30 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ OL )
32 1 4 26 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ 𝑋 ) ∈ 𝐵 ) → ( ( 𝑃 ∨ 𝑋 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑋 ) )
33 31 14 32 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑋 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑋 ) )
34 29 33 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑋 ) ∧ ( 𝑊 ∨ 𝑃 ) ) = ( 𝑃 ∨ 𝑋 ) )
35 21 25 34 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) ) = ( 𝑃 ∨ 𝑋 ) )