Theorem lineset

Description: The set of lines in a Hilbert lattice. (Contributed by NM, 19-Sep-2011)

	Ref	Expression
Hypotheses	lineset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lineset.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	lineset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lineset.n	$$⊢N=\mathrm{Lines}\left(K\right)$$
Assertion	lineset	$$⊢K\in B\to N=\left\{s|\exists q\in A\exists r\in A\left(q\ne r\wedge s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lineset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		lineset.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		lineset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		lineset.n	$$⊢N=\mathrm{Lines}\left(K\right)$$
5		elex	$$⊢K\in B\to K\in \mathrm{V}$$
6		fveq2	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=\mathrm{Atoms}\left(K\right)$$
7	6 3	eqtr4di	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=A$$
8		fveq2	$$⊢k=K\to {\le }_k={\le }_K$$
9	8 1	eqtr4di	$$⊢k=K\to {\le }_k=\underset{\dot{}}{\le }$$
10	9	breqd	$$⊢k=K\to \left(p{\le }_k\left(q\mathrm{join}\left(k\right)r\right)\leftrightarrow p\underset{\dot{}}{\le }\left(q\mathrm{join}\left(k\right)r\right)\right)$$
11		fveq2	$$⊢k=K\to \mathrm{join}\left(k\right)=\mathrm{join}\left(K\right)$$
12	11 2	eqtr4di	$$⊢k=K\to \mathrm{join}\left(k\right)=\underset{\dot{}}{\vee }$$
13	12	oveqd	$$⊢k=K\to q\mathrm{join}\left(k\right)r=q\underset{\dot{}}{\vee }r$$
14	13	breq2d	$$⊢k=K\to \left(p\underset{\dot{}}{\le }\left(q\mathrm{join}\left(k\right)r\right)\leftrightarrow p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right)$$
15	10 14	bitrd	$$⊢k=K\to \left(p{\le }_k\left(q\mathrm{join}\left(k\right)r\right)\leftrightarrow p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right)$$
16	7 15	rabeqbidv	$$⊢k=K\to \left\{p\in \mathrm{Atoms}\left(k\right)|p{\le }_k\left(q\mathrm{join}\left(k\right)r\right)\right\}=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}$$
17	16	eqeq2d	$$⊢k=K\to \left(s=\left\{p\in \mathrm{Atoms}\left(k\right)|p{\le }_k\left(q\mathrm{join}\left(k\right)r\right)\right\}\leftrightarrow s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)$$
18	17	anbi2d	$$⊢k=K\to \left(\left(q\ne r\wedge s=\left\{p\in \mathrm{Atoms}\left(k\right)|p{\le }_k\left(q\mathrm{join}\left(k\right)r\right)\right\}\right)\leftrightarrow \left(q\ne r\wedge s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right)$$
19	7 18	rexeqbidv	$$⊢k=K\to \left(\exists r\in \mathrm{Atoms}\left(k\right)\left(q\ne r\wedge s=\left\{p\in \mathrm{Atoms}\left(k\right)|p{\le }_k\left(q\mathrm{join}\left(k\right)r\right)\right\}\right)\leftrightarrow \exists r\in A\left(q\ne r\wedge s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right)$$
20	7 19	rexeqbidv	$$⊢k=K\to \left(\exists q\in \mathrm{Atoms}\left(k\right)\exists r\in \mathrm{Atoms}\left(k\right)\left(q\ne r\wedge s=\left\{p\in \mathrm{Atoms}\left(k\right)|p{\le }_k\left(q\mathrm{join}\left(k\right)r\right)\right\}\right)\leftrightarrow \exists q\in A\exists r\in A\left(q\ne r\wedge s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right)$$
21	20	abbidv	$$⊢k=K\to \left\{s|\exists q\in \mathrm{Atoms}\left(k\right)\exists r\in \mathrm{Atoms}\left(k\right)\left(q\ne r\wedge s=\left\{p\in \mathrm{Atoms}\left(k\right)|p{\le }_k\left(q\mathrm{join}\left(k\right)r\right)\right\}\right)\right\}=\left\{s|\exists q\in A\exists r\in A\left(q\ne r\wedge s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right\}$$
22		df-lines	$$⊢\mathrm{Lines}=\left(k\in \mathrm{V}⟼\left\{s|\exists q\in \mathrm{Atoms}\left(k\right)\exists r\in \mathrm{Atoms}\left(k\right)\left(q\ne r\wedge s=\left\{p\in \mathrm{Atoms}\left(k\right)|p{\le }_k\left(q\mathrm{join}\left(k\right)r\right)\right\}\right)\right\}\right)$$
23	3	fvexi	$$⊢A\in \mathrm{V}$$
24		df-sn	$$⊢\left\{\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right\}=\left\{s|s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right\}$$
25		snex	$$⊢\left\{\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right\}\in \mathrm{V}$$
26	24 25	eqeltrri	$$⊢\left\{s|s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right\}\in \mathrm{V}$$
27		simpr	$$⊢\left(q\ne r\wedge s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\to s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}$$
28	27	ss2abi	$$⊢\left\{s|\left(q\ne r\wedge s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right\}\subseteq \left\{s|s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right\}$$
29	26 28	ssexi	$$⊢\left\{s|\left(q\ne r\wedge s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right\}\in \mathrm{V}$$
30	23 23 29	ab2rexex2	$$⊢\left\{s|\exists q\in A\exists r\in A\left(q\ne r\wedge s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right\}\in \mathrm{V}$$
31	21 22 30	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{Lines}\left(K\right)=\left\{s|\exists q\in A\exists r\in A\left(q\ne r\wedge s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right\}$$
32	4 31	syl5eq	$$⊢K\in \mathrm{V}\to N=\left\{s|\exists q\in A\exists r\in A\left(q\ne r\wedge s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right\}$$
33	5 32	syl	$$⊢K\in B\to N=\left\{s|\exists q\in A\exists r\in A\left(q\ne r\wedge s=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right\}$$