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

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. ‘ 𝐾 )
pmap0.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion pmap0 ( 𝐾 ∈ AtLat → ( 𝑀 ‘ 0 ) = ∅ )

Proof

Step Hyp Ref Expression
1 pmap0.z ⊢ 0 = ( 0. ‘ 𝐾 )
2 pmap0.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
3 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
4 3 1 atl0cl ⊢ ( 𝐾 ∈ AtLat → 0 ∈ ( Base ‘ 𝐾 ) )
5 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
6 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7 3 5 6 2 pmapval ⊢ ( ( 𝐾 ∈ AtLat ∧ 0 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑀 ‘ 0 ) = { 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑎 ( le ‘ 𝐾 ) 0 } )
8 4 7 mpdan ⊢ ( 𝐾 ∈ AtLat → ( 𝑀 ‘ 0 ) = { 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑎 ( le ‘ 𝐾 ) 0 } )
9 5 1 6 atnle0 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑎 ∈ ( Atoms ‘ 𝐾 ) ) → ¬ 𝑎 ( le ‘ 𝐾 ) 0 )
10 9 nrexdv ⊢ ( 𝐾 ∈ AtLat → ¬ ∃ 𝑎 ∈ ( Atoms ‘ 𝐾 ) 𝑎 ( le ‘ 𝐾 ) 0 )
11 rabn0 ⊢ ( { 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑎 ( le ‘ 𝐾 ) 0 } ≠ ∅ ↔ ∃ 𝑎 ∈ ( Atoms ‘ 𝐾 ) 𝑎 ( le ‘ 𝐾 ) 0 )
12 10 11 sylnibr ⊢ ( 𝐾 ∈ AtLat → ¬ { 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑎 ( le ‘ 𝐾 ) 0 } ≠ ∅ )
13 nne ⊢ ( ¬ { 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑎 ( le ‘ 𝐾 ) 0 } ≠ ∅ ↔ { 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑎 ( le ‘ 𝐾 ) 0 } = ∅ )
14 12 13 sylib ⊢ ( 𝐾 ∈ AtLat → { 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑎 ( le ‘ 𝐾 ) 0 } = ∅ )
15 8 14 eqtrd ⊢ ( 𝐾 ∈ AtLat → ( 𝑀 ‘ 0 ) = ∅ )