Theorem llnset

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

	Ref	Expression
Hypotheses	llnset.b	$$⊢B={\mathrm{Base}}_K$$
	llnset.c	$$⊢C={⋖}_K$$
	llnset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	llnset.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
Assertion	llnset	$$⊢K\in D\to N=\left\{x\in B|\exists p\in ApCx\right\}$$

Proof

Step	Hyp	Ref	Expression
1		llnset.b	$$⊢B={\mathrm{Base}}_K$$
2		llnset.c	$$⊢C={⋖}_K$$
3		llnset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		llnset.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
5		elex	$$⊢K\in D\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 {⋖}_k={⋖}_K$$
11	10 2	eqtr4di	$$⊢k=K\to {⋖}_k=C$$
12	11	breqd	$$⊢k=K\to \left(p{⋖}_{k}x\leftrightarrow pCx\right)$$
13	9 12	rexeqbidv	$$⊢k=K\to \left(\exists p\in \mathrm{Atoms}\left(k\right)p{⋖}_{k}x\leftrightarrow \exists p\in ApCx\right)$$
14	7 13	rabeqbidv	$$⊢k=K\to \left\{x\in {\mathrm{Base}}_k|\exists p\in \mathrm{Atoms}\left(k\right)p{⋖}_{k}x\right\}=\left\{x\in B|\exists p\in ApCx\right\}$$
15		df-llines	$$⊢\mathrm{LLines}=\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|\exists p\in \mathrm{Atoms}\left(k\right)p{⋖}_{k}x\right\}\right)$$
16	1	fvexi	$$⊢B\in \mathrm{V}$$
17	16	rabex	$$⊢\left\{x\in B|\exists p\in ApCx\right\}\in \mathrm{V}$$
18	14 15 17	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{LLines}\left(K\right)=\left\{x\in B|\exists p\in ApCx\right\}$$
19	4 18	syl5eq	$$⊢K\in \mathrm{V}\to N=\left\{x\in B|\exists p\in ApCx\right\}$$
20	5 19	syl	$$⊢K\in D\to N=\left\{x\in B|\exists p\in ApCx\right\}$$