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

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 eqtrid ⊢ ( 𝐾 ∈ V → 𝑀 = ( 𝑥 ∈ 𝐵 ↦ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } ) )
18 5 17 syl ⊢ ( 𝐾 ∈ 𝐶 → 𝑀 = ( 𝑥 ∈ 𝐵 ↦ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } ) )