Theorem lplnset

Description: The set of lattice planes in a Hilbert lattice. (Contributed by NM, 16-Jun-2012)

	Ref	Expression
Hypotheses	lplnset.b	$$⊢B={\mathrm{Base}}_K$$
	lplnset.c	$$⊢C={⋖}_K$$
	lplnset.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
	lplnset.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
Assertion	lplnset	$$⊢K\in A\to P=\left\{x\in B|\exists y\in NyCx\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lplnset.b	$$⊢B={\mathrm{Base}}_K$$
2		lplnset.c	$$⊢C={⋖}_K$$
3		lplnset.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
4		lplnset.p	$$⊢P=\mathrm{LPlanes}\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{LLines}\left(k\right)=\mathrm{LLines}\left(K\right)$$
9	8 3	eqtr4di	$$⊢k=K\to \mathrm{LLines}\left(k\right)=N$$
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{LLines}\left(k\right)y{⋖}_{k}x\leftrightarrow \exists y\in NyCx\right)$$
14	7 13	rabeqbidv	$$⊢k=K\to \left\{x\in {\mathrm{Base}}_k|\exists y\in \mathrm{LLines}\left(k\right)y{⋖}_{k}x\right\}=\left\{x\in B|\exists y\in NyCx\right\}$$
15		df-lplanes	$$⊢\mathrm{LPlanes}=\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|\exists y\in \mathrm{LLines}\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 NyCx\right\}\in \mathrm{V}$$
18	14 15 17	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{LPlanes}\left(K\right)=\left\{x\in B|\exists y\in NyCx\right\}$$
19	4 18	eqtrid	$$⊢K\in \mathrm{V}\to P=\left\{x\in B|\exists y\in NyCx\right\}$$
20	5 19	syl	$$⊢K\in A\to P=\left\{x\in B|\exists y\in NyCx\right\}$$