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

Metamath Proof Explorer

Theorem pmapeq0

Description: A projective map value is zero iff its argument is lattice zero. (Contributed by NM, 27-Jan-2012)

Ref Expression
Hypotheses pmapeq0.b ⊢ B = Base K
pmapeq0.z ⊢ 0 ˙ = 0. ⁡ K
pmapeq0.m ⊢ M = pmap ⁡ K
Assertion pmapeq0 ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X = ∅ ↔ X = 0 ˙

Proof

Step Hyp Ref Expression
1 pmapeq0.b ⊢ B = Base K
2 pmapeq0.z ⊢ 0 ˙ = 0. ⁡ K
3 pmapeq0.m ⊢ M = pmap ⁡ K
4 hlatl ⊢ K ∈ HL → K ∈ AtLat
5 4 adantr ⊢ K ∈ HL ∧ X ∈ B → K ∈ AtLat
6 2 3 pmap0 ⊢ K ∈ AtLat → M ⁡ 0 ˙ = ∅
7 5 6 syl ⊢ K ∈ HL ∧ X ∈ B → M ⁡ 0 ˙ = ∅
8 7 eqeq2d ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X = M ⁡ 0 ˙ ↔ M ⁡ X = ∅
9 hlop ⊢ K ∈ HL → K ∈ OP
10 9 adantr ⊢ K ∈ HL ∧ X ∈ B → K ∈ OP
11 1 2 op0cl ⊢ K ∈ OP → 0 ˙ ∈ B
12 10 11 syl ⊢ K ∈ HL ∧ X ∈ B → 0 ˙ ∈ B
13 1 3 pmap11 ⊢ K ∈ HL ∧ X ∈ B ∧ 0 ˙ ∈ B → M ⁡ X = M ⁡ 0 ˙ ↔ X = 0 ˙
14 12 13 mpd3an3 ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X = M ⁡ 0 ˙ ↔ X = 0 ˙
15 8 14 bitr3d ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X = ∅ ↔ X = 0 ˙