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 ) = ∅ )