Metamath Proof Explorer


Theorem pmapfval

Description: The projective map of a Hilbert lattice. (Contributed by NM, 2-Oct-2011)

Ref Expression
Hypotheses pmapfval.b 𝐵 = ( Base ‘ 𝐾 )
pmapfval.l = ( le ‘ 𝐾 )
pmapfval.a 𝐴 = ( Atoms ‘ 𝐾 )
pmapfval.m 𝑀 = ( pmap ‘ 𝐾 )
Assertion pmapfval ( 𝐾𝐶𝑀 = ( 𝑥𝐵 ↦ { 𝑎𝐴𝑎 𝑥 } ) )

Proof

Step Hyp Ref Expression
1 pmapfval.b 𝐵 = ( Base ‘ 𝐾 )
2 pmapfval.l = ( le ‘ 𝐾 )
3 pmapfval.a 𝐴 = ( Atoms ‘ 𝐾 )
4 pmapfval.m 𝑀 = ( pmap ‘ 𝐾 )
5 elex ( 𝐾𝐶𝐾 ∈ V )
6 fveq2 ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
7 6 1 eqtr4di ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
8 fveq2 ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
9 8 3 eqtr4di ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
10 fveq2 ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
11 10 2 eqtr4di ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = )
12 11 breqd ( 𝑘 = 𝐾 → ( 𝑎 ( le ‘ 𝑘 ) 𝑥𝑎 𝑥 ) )
13 9 12 rabeqbidv ( 𝑘 = 𝐾 → { 𝑎 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑎 ( le ‘ 𝑘 ) 𝑥 } = { 𝑎𝐴𝑎 𝑥 } )
14 7 13 mpteq12dv ( 𝑘 = 𝐾 → ( 𝑥 ∈ ( Base ‘ 𝑘 ) ↦ { 𝑎 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑎 ( le ‘ 𝑘 ) 𝑥 } ) = ( 𝑥𝐵 ↦ { 𝑎𝐴𝑎 𝑥 } ) )
15 df-pmap pmap = ( 𝑘 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑘 ) ↦ { 𝑎 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑎 ( le ‘ 𝑘 ) 𝑥 } ) )
16 14 15 1 mptfvmpt ( 𝐾 ∈ V → ( pmap ‘ 𝐾 ) = ( 𝑥𝐵 ↦ { 𝑎𝐴𝑎 𝑥 } ) )
17 4 16 syl5eq ( 𝐾 ∈ V → 𝑀 = ( 𝑥𝐵 ↦ { 𝑎𝐴𝑎 𝑥 } ) )
18 5 17 syl ( 𝐾𝐶𝑀 = ( 𝑥𝐵 ↦ { 𝑎𝐴𝑎 𝑥 } ) )