Theorem pmap1N

Description: Value of the projective map of a Hilbert lattice at lattice unit. Part of Theorem 15.5.1 of MaedaMaeda p. 62. (Contributed by NM, 22-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmap1.u	⊢ 1 = ( 1. ‘ 𝐾 )
	pmap1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pmap1.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion	pmap1N	⊢ ( 𝐾 ∈ OP → ( 𝑀 ‘ 1 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pmap1.u	⊢ 1 = ( 1. ‘ 𝐾 )
2		pmap1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		pmap1.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
4		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5	4 1	op1cl	⊢ ( 𝐾 ∈ OP → 1 ∈ ( Base ‘ 𝐾 ) )
6		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7	4 6 2 3	pmapval	⊢ ( ( 𝐾 ∈ OP ∧ 1 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑀 ‘ 1 ) = { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) 1 } )
8	5 7	mpdan	⊢ ( 𝐾 ∈ OP → ( 𝑀 ‘ 1 ) = { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) 1 } )
9	4 2	atbase	⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( Base ‘ 𝐾 ) )
10	4 6 1	ople1	⊢ ( ( 𝐾 ∈ OP ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) → 𝑝 ( le ‘ 𝐾 ) 1 )
11	9 10	sylan2	⊢ ( ( 𝐾 ∈ OP ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ( le ‘ 𝐾 ) 1 )
12	11	ralrimiva	⊢ ( 𝐾 ∈ OP → ∀ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) 1 )
13		rabid2	⊢ ( 𝐴 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) 1 } ↔ ∀ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) 1 )
14	12 13	sylibr	⊢ ( 𝐾 ∈ OP → 𝐴 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) 1 } )
15	8 14	eqtr4d	⊢ ( 𝐾 ∈ OP → ( 𝑀 ‘ 1 ) = 𝐴 )