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

Metamath Proof Explorer

Theorem lhpmat

Description: An element covered by the lattice unity, when conjoined with an atom not under it, equals the lattice zero. (Contributed by NM, 6-Jun-2012)

Ref Expression
Hypotheses lhpmat.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpmat.m ⊢ ∧ = ( meet ‘ 𝐾 )
lhpmat.z ⊢ 0 = ( 0. ‘ 𝐾 )
lhpmat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhpmat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpmat ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∧ 𝑊 ) = 0 )

Proof

Step Hyp Ref Expression
1 lhpmat.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhpmat.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 lhpmat.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 lhpmat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 lhpmat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ¬ 𝑃 ≤ 𝑊 )
7 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
8 7 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ AtLat )
9 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
12 11 ad2antlr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
13 10 1 2 3 4 atnle ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ¬ 𝑃 ≤ 𝑊 ↔ ( 𝑃 ∧ 𝑊 ) = 0 ) )
14 8 9 12 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ¬ 𝑃 ≤ 𝑊 ↔ ( 𝑃 ∧ 𝑊 ) = 0 ) )
15 6 14 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∧ 𝑊 ) = 0 )