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

Metamath Proof Explorer

Theorem pmap1N

Description: Value of the projective map of a Hilbert lattice at lattice unity. 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 ) = 𝐴 )