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

Metamath Proof Explorer

Theorem lhpmatb

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

Ref Expression
Hypotheses lhpmat.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpmat.m ⊢ ∧ = ( meet ‘ 𝐾 )
lhpmat.z ⊢ 0 = ( 0. ‘ 𝐾 )
lhpmat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhpmat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpmatb ( ( ( 𝐾 ∈ 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 1 2 3 4 5 lhpmat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∧ 𝑊 ) = 0 )
7 6 anassrs ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ 𝑊 ) → ( 𝑃 ∧ 𝑊 ) = 0 )
8 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
9 8 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑃 ∧ 𝑊 ) = 0 ) → 𝐾 ∈ AtLat )
10 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑃 ∧ 𝑊 ) = 0 ) → 𝑃 ∈ 𝐴 )
11 3 4 atn0 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ≠ 0 )
12 11 necomd ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 0 ≠ 𝑃 )
13 9 10 12 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑃 ∧ 𝑊 ) = 0 ) → 0 ≠ 𝑃 )
14 neeq1 ⊢ ( ( 𝑃 ∧ 𝑊 ) = 0 → ( ( 𝑃 ∧ 𝑊 ) ≠ 𝑃 ↔ 0 ≠ 𝑃 ) )
15 14 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑃 ∧ 𝑊 ) = 0 ) → ( ( 𝑃 ∧ 𝑊 ) ≠ 𝑃 ↔ 0 ≠ 𝑃 ) )
16 13 15 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑃 ∧ 𝑊 ) = 0 ) → ( 𝑃 ∧ 𝑊 ) ≠ 𝑃 )
17 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
18 17 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑃 ∧ 𝑊 ) = 0 ) → 𝐾 ∈ Lat )
19 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
20 19 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
21 10 20 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑃 ∧ 𝑊 ) = 0 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
22 19 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
23 22 ad3antlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑃 ∧ 𝑊 ) = 0 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
24 19 1 2 latleeqm1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ≤ 𝑊 ↔ ( 𝑃 ∧ 𝑊 ) = 𝑃 ) )
25 18 21 23 24 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑃 ∧ 𝑊 ) = 0 ) → ( 𝑃 ≤ 𝑊 ↔ ( 𝑃 ∧ 𝑊 ) = 𝑃 ) )
26 25 necon3bbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑃 ∧ 𝑊 ) = 0 ) → ( ¬ 𝑃 ≤ 𝑊 ↔ ( 𝑃 ∧ 𝑊 ) ≠ 𝑃 ) )
27 16 26 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑃 ∧ 𝑊 ) = 0 ) → ¬ 𝑃 ≤ 𝑊 )
28 7 27 impbida ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑃 ≤ 𝑊 ↔ ( 𝑃 ∧ 𝑊 ) = 0 ) )