Theorem lvolset

Description: The set of 3-dim lattice volumes in a Hilbert lattice. (Contributed by NM, 1-Jul-2012)

	Ref	Expression
Hypotheses	lvolset.b	$$⊢B={\mathrm{Base}}_K$$
	lvolset.c	$$⊢C={⋖}_K$$
	lvolset.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
	lvolset.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
Assertion	lvolset	$$⊢K\in A\to V=\left\{x\in B|\exists y\in PyCx\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lvolset.b	$$⊢B={\mathrm{Base}}_K$$
2		lvolset.c	$$⊢C={⋖}_K$$
3		lvolset.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
4		lvolset.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
5		elex	$$⊢K\in A\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{LPlanes}\left(k\right)=\mathrm{LPlanes}\left(K\right)$$
9	8 3	eqtr4di	$$⊢k=K\to \mathrm{LPlanes}\left(k\right)=P$$
10		fveq2	$$⊢k=K\to {⋖}_k={⋖}_K$$
11	10 2	eqtr4di	$$⊢k=K\to {⋖}_k=C$$
12	11	breqd	$$⊢k=K\to \left(y{⋖}_{k}x\leftrightarrow yCx\right)$$
13	9 12	rexeqbidv	$$⊢k=K\to \left(\exists y\in \mathrm{LPlanes}\left(k\right)y{⋖}_{k}x\leftrightarrow \exists y\in PyCx\right)$$
14	7 13	rabeqbidv	$$⊢k=K\to \left\{x\in {\mathrm{Base}}_k|\exists y\in \mathrm{LPlanes}\left(k\right)y{⋖}_{k}x\right\}=\left\{x\in B|\exists y\in PyCx\right\}$$
15		df-lvols	$$⊢\mathrm{LVols}=\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|\exists y\in \mathrm{LPlanes}\left(k\right)y{⋖}_{k}x\right\}\right)$$
16	1	fvexi	$$⊢B\in \mathrm{V}$$
17	16	rabex	$$⊢\left\{x\in B|\exists y\in PyCx\right\}\in \mathrm{V}$$
18	14 15 17	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{LVols}\left(K\right)=\left\{x\in B|\exists y\in PyCx\right\}$$
19	4 18	syl5eq	$$⊢K\in \mathrm{V}\to V=\left\{x\in B|\exists y\in PyCx\right\}$$
20	5 19	syl	$$⊢K\in A\to V=\left\{x\in B|\exists y\in PyCx\right\}$$