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	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) = { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑋 } )