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

Metamath Proof Explorer

Theorem pmapval

Description: Value of the projective map of a Hilbert lattice. Definition in Theorem 15.5 of MaedaMaeda p. 62. (Contributed by NM, 2-Oct-2011)

Ref Expression
Hypotheses pmapfval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmapfval.l ⊢ ≤ = ( le ‘ 𝐾 )
pmapfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pmapfval.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion pmapval ( ( 𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) = { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑋 } )

Proof

Step Hyp Ref Expression
1 pmapfval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pmapfval.l ⊢ ≤ = ( le ‘ 𝐾 )
3 pmapfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 pmapfval.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
5 1 2 3 4 pmapfval ⊢ ( 𝐾 ∈ 𝐶 → 𝑀 = ( 𝑥 ∈ 𝐵 ↦ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } ) )
6 5 fveq1d ⊢ ( 𝐾 ∈ 𝐶 → ( 𝑀 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝐵 ↦ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } ) ‘ 𝑋 ) )
7 breq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑎 ≤ 𝑥 ↔ 𝑎 ≤ 𝑋 ) )
8 7 rabbidv ⊢ ( 𝑥 = 𝑋 → { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } = { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑋 } )
9 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } )
10 3 fvexi ⊢ 𝐴 ∈ V
11 10 rabex ⊢ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑋 } ∈ V
12 8 9 11 fvmpt ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } ) ‘ 𝑋 ) = { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑋 } )
13 6 12 sylan9eq ⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) = { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑋 } )