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	$$⊢B={\mathrm{Base}}_K$$
	pmapfval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	pmapfval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	pmapfval.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
Assertion	pmapval	$$⊢\left(K\in C\wedge X\in B\right)\to M\left(X\right)=\left\{a\in A|a\underset{\dot{}}{\le }X\right\}$$

Proof

Step	Hyp	Ref	Expression
1		pmapfval.b	$$⊢B={\mathrm{Base}}_K$$
2		pmapfval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		pmapfval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		pmapfval.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
5	1 2 3 4	pmapfval	$$⊢K\in C\to M=\left(x\in B⟼\left\{a\in A|a\underset{\dot{}}{\le }x\right\}\right)$$
6	5	fveq1d	$$⊢K\in C\to M\left(X\right)=\left(x\in B⟼\left\{a\in A|a\underset{\dot{}}{\le }x\right\}\right)\left(X\right)$$
7		breq2	$$⊢x=X\to \left(a\underset{\dot{}}{\le }x\leftrightarrow a\underset{\dot{}}{\le }X\right)$$
8	7	rabbidv	$$⊢x=X\to \left\{a\in A|a\underset{\dot{}}{\le }x\right\}=\left\{a\in A|a\underset{\dot{}}{\le }X\right\}$$
9		eqid	$$⊢\left(x\in B⟼\left\{a\in A|a\underset{\dot{}}{\le }x\right\}\right)=\left(x\in B⟼\left\{a\in A|a\underset{\dot{}}{\le }x\right\}\right)$$
10	3	fvexi	$$⊢A\in \mathrm{V}$$
11	10	rabex	$$⊢\left\{a\in A|a\underset{\dot{}}{\le }X\right\}\in \mathrm{V}$$
12	8 9 11	fvmpt	$$⊢X\in B\to \left(x\in B⟼\left\{a\in A|a\underset{\dot{}}{\le }x\right\}\right)\left(X\right)=\left\{a\in A|a\underset{\dot{}}{\le }X\right\}$$
13	6 12	sylan9eq	$$⊢\left(K\in C\wedge X\in B\right)\to M\left(X\right)=\left\{a\in A|a\underset{\dot{}}{\le }X\right\}$$