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 ( ( 𝐾𝐶𝑋𝐵 ) → ( 𝑀𝑋 ) = { 𝑎𝐴𝑎 𝑋 } )