Metamath Proof Explorer

Theorem lhple

Description: Property of a lattice element under a co-atom. (Contributed by NM, 28-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 lhple.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lhple.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lhple.j ⊢ ∨ = ( join ‘ 𝐾 )
4 lhple.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 lhple.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 lhple.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
8 7 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
9 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
10 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
11 9 10 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐵 )
12 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐵 )
13 1 3 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑋 ) = ( 𝑋 ∨ 𝑃 ) )
14 8 11 12 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑋 ) = ( 𝑋 ∨ 𝑃 ) )
15 14 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) = ( ( 𝑋 ∨ 𝑃 ) ∧ 𝑊 ) )
16 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑋 ≤ 𝑊 )
18 1 2 3 4 6 lhpmod6i1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → ( 𝑋 ∨ ( 𝑃 ∧ 𝑊 ) ) = ( ( 𝑋 ∨ 𝑃 ) ∧ 𝑊 ) )
19 16 12 11 17 18 syl121anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝑋 ∨ ( 𝑃 ∧ 𝑊 ) ) = ( ( 𝑋 ∨ 𝑃 ) ∧ 𝑊 ) )
20 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
21 2 4 20 5 6 lhpmat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
22 21 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝑃 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
23 22 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝑋 ∨ ( 𝑃 ∧ 𝑊 ) ) = ( 𝑋 ∨ ( 0. ‘ 𝐾 ) ) )
24 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
25 7 24 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → 𝐾 ∈ OL )
26 1 3 20 olj01 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∨ ( 0. ‘ 𝐾 ) ) = 𝑋 )
27 25 12 26 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝑋 ∨ ( 0. ‘ 𝐾 ) ) = 𝑋 )
28 23 27 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝑋 ∨ ( 𝑃 ∧ 𝑊 ) ) = 𝑋 )
29 15 19 28 3eqtr2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑋 ) ∧ 𝑊 ) = 𝑋 )