Theorem pmapfval

Description: The projective map of a Hilbert lattice. (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	pmapfval	$$⊢K\in C\to M=\left(x\in B⟼\left\{a\in A|a\underset{\dot{}}{\le }x\right\}\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		elex	$$⊢K\in C\to K\in \mathrm{V}$$
6		fveq2	$$⊢k=K\to {\mathrm{Base}}_k={\mathrm{Base}}_K$$
7	6 1	eqtr4di	$$⊢k=K\to {\mathrm{Base}}_k=B$$
8		fveq2	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=\mathrm{Atoms}\left(K\right)$$
9	8 3	eqtr4di	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=A$$
10		fveq2	$$⊢k=K\to {\le }_k={\le }_K$$
11	10 2	eqtr4di	$$⊢k=K\to {\le }_k=\underset{\dot{}}{\le }$$
12	11	breqd	$$⊢k=K\to \left(a{\le }_{k}x\leftrightarrow a\underset{\dot{}}{\le }x\right)$$
13	9 12	rabeqbidv	$$⊢k=K\to \left\{a\in \mathrm{Atoms}\left(k\right)|a{\le }_{k}x\right\}=\left\{a\in A|a\underset{\dot{}}{\le }x\right\}$$
14	7 13	mpteq12dv	$$⊢k=K\to \left(x\in {\mathrm{Base}}_k⟼\left\{a\in \mathrm{Atoms}\left(k\right)|a{\le }_{k}x\right\}\right)=\left(x\in B⟼\left\{a\in A|a\underset{\dot{}}{\le }x\right\}\right)$$
15		df-pmap	$$⊢\mathrm{pmap}=\left(k\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_k⟼\left\{a\in \mathrm{Atoms}\left(k\right)|a{\le }_{k}x\right\}\right)\right)$$
16	14 15 1	mptfvmpt	$$⊢K\in \mathrm{V}\to \mathrm{pmap}\left(K\right)=\left(x\in B⟼\left\{a\in A|a\underset{\dot{}}{\le }x\right\}\right)$$
17	4 16	syl5eq	$$⊢K\in \mathrm{V}\to M=\left(x\in B⟼\left\{a\in A|a\underset{\dot{}}{\le }x\right\}\right)$$
18	5 17	syl	$$⊢K\in C\to M=\left(x\in B⟼\left\{a\in A|a\underset{\dot{}}{\le }x\right\}\right)$$