Metamath Proof Explorer

Theorem pmap0

Description: Value of the projective map of a Hilbert lattice at lattice zero. Part of Theorem 15.5.1 of MaedaMaeda p. 62. (Contributed by NM, 17-Oct-2011)

Ref Expression
Hypotheses pmap0.z ⊢ 0 ˙ = 0. ⁡ K
pmap0.m ⊢ M = pmap ⁡ K
Assertion pmap0 ⊢ K ∈ AtLat → M ⁡ 0 ˙ = ∅

Proof

Step Hyp Ref Expression
1 pmap0.z ⊢ 0 ˙ = 0. ⁡ K
2 pmap0.m ⊢ M = pmap ⁡ K
3 eqid ⊢ Base K = Base K
4 3 1 atl0cl ⊢ K ∈ AtLat → 0 ˙ ∈ Base K
5 eqid ⊢ ≤ K = ≤ K
6 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
7 3 5 6 2 pmapval ⊢ K ∈ AtLat ∧ 0 ˙ ∈ Base K → M ⁡ 0 ˙ = a ∈ Atoms ⁡ K | a ≤ K 0 ˙
8 4 7 mpdan ⊢ K ∈ AtLat → M ⁡ 0 ˙ = a ∈ Atoms ⁡ K | a ≤ K 0 ˙
9 5 1 6 atnle0 ⊢ K ∈ AtLat ∧ a ∈ Atoms ⁡ K → ¬ a ≤ K 0 ˙
10 9 nrexdv ⊢ K ∈ AtLat → ¬ ∃ a ∈ Atoms ⁡ K a ≤ K 0 ˙
11 rabn0 ⊢ a ∈ Atoms ⁡ K | a ≤ K 0 ˙ ≠ ∅ ↔ ∃ a ∈ Atoms ⁡ K a ≤ K 0 ˙
12 10 11 sylnibr ⊢ K ∈ AtLat → ¬ a ∈ Atoms ⁡ K | a ≤ K 0 ˙ ≠ ∅
13 nne ⊢ ¬ a ∈ Atoms ⁡ K | a ≤ K 0 ˙ ≠ ∅ ↔ a ∈ Atoms ⁡ K | a ≤ K 0 ˙ = ∅
14 12 13 sylib ⊢ K ∈ AtLat → a ∈ Atoms ⁡ K | a ≤ K 0 ˙ = ∅
15 8 14 eqtrd ⊢ K ∈ AtLat → M ⁡ 0 ˙ = ∅