Theorem psubspset

Description: The set of projective subspaces in a Hilbert lattice. (Contributed by NM, 2-Oct-2011)

	Ref	Expression
Hypotheses	psubspset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	psubspset.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	psubspset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	psubspset.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
Assertion	psubspset	$$⊢K\in B\to S=\left\{s|\left(s\subseteq A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		psubspset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		psubspset.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		psubspset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		psubspset.s	$$⊢S=\mathrm{PSubSp}\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	7	sseq2d	$$⊢k=K\to \left(s\subseteq \mathrm{Atoms}\left(k\right)\leftrightarrow s\subseteq A\right)$$
9		fveq2	$$⊢k=K\to \mathrm{join}\left(k\right)=\mathrm{join}\left(K\right)$$
10	9 2	eqtr4di	$$⊢k=K\to \mathrm{join}\left(k\right)=\underset{\dot{}}{\vee }$$
11	10	oveqd	$$⊢k=K\to p\mathrm{join}\left(k\right)q=p\underset{\dot{}}{\vee }q$$
12	11	breq2d	$$⊢k=K\to \left(r{\le }_k\left(p\mathrm{join}\left(k\right)q\right)\leftrightarrow r{\le }_k\left(p\underset{\dot{}}{\vee }q\right)\right)$$
13		fveq2	$$⊢k=K\to {\le }_k={\le }_K$$
14	13 1	eqtr4di	$$⊢k=K\to {\le }_k=\underset{\dot{}}{\le }$$
15	14	breqd	$$⊢k=K\to \left(r{\le }_k\left(p\underset{\dot{}}{\vee }q\right)\leftrightarrow r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)$$
16	12 15	bitrd	$$⊢k=K\to \left(r{\le }_k\left(p\mathrm{join}\left(k\right)q\right)\leftrightarrow r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)$$
17	16	imbi1d	$$⊢k=K\to \left(\left(r{\le }_k\left(p\mathrm{join}\left(k\right)q\right)\to r\in s\right)\leftrightarrow \left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)$$
18	7 17	raleqbidv	$$⊢k=K\to \left(\forall r\in \mathrm{Atoms}\left(k\right)\left(r{\le }_k\left(p\mathrm{join}\left(k\right)q\right)\to r\in s\right)\leftrightarrow \forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)$$
19	18	2ralbidv	$$⊢k=K\to \left(\forall p\in s\forall q\in s\forall r\in \mathrm{Atoms}\left(k\right)\left(r{\le }_k\left(p\mathrm{join}\left(k\right)q\right)\to r\in s\right)\leftrightarrow \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)$$
20	8 19	anbi12d	$$⊢k=K\to \left(\left(s\subseteq \mathrm{Atoms}\left(k\right)\wedge \forall p\in s\forall q\in s\forall r\in \mathrm{Atoms}\left(k\right)\left(r{\le }_k\left(p\mathrm{join}\left(k\right)q\right)\to r\in s\right)\right)\leftrightarrow \left(s\subseteq A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)\right)$$
21	20	abbidv	$$⊢k=K\to \left\{s|\left(s\subseteq \mathrm{Atoms}\left(k\right)\wedge \forall p\in s\forall q\in s\forall r\in \mathrm{Atoms}\left(k\right)\left(r{\le }_k\left(p\mathrm{join}\left(k\right)q\right)\to r\in s\right)\right)\right\}=\left\{s|\left(s\subseteq A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)\right\}$$
22		df-psubsp	$$⊢\mathrm{PSubSp}=\left(k\in \mathrm{V}⟼\left\{s|\left(s\subseteq \mathrm{Atoms}\left(k\right)\wedge \forall p\in s\forall q\in s\forall r\in \mathrm{Atoms}\left(k\right)\left(r{\le }_k\left(p\mathrm{join}\left(k\right)q\right)\to r\in s\right)\right)\right\}\right)$$
23	3	fvexi	$$⊢A\in \mathrm{V}$$
24	23	pwex	$$⊢𝒫A\in \mathrm{V}$$
25		velpw	$$⊢s\in 𝒫A\leftrightarrow s\subseteq A$$
26	25	anbi1i	$$⊢\left(s\in 𝒫A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)\leftrightarrow \left(s\subseteq A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)$$
27	26	abbii	$$⊢\left\{s|\left(s\in 𝒫A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)\right\}=\left\{s|\left(s\subseteq A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)\right\}$$
28		ssab2	$$⊢\left\{s|\left(s\in 𝒫A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)\right\}\subseteq 𝒫A$$
29	27 28	eqsstrri	$$⊢\left\{s|\left(s\subseteq A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)\right\}\subseteq 𝒫A$$
30	24 29	ssexi	$$⊢\left\{s|\left(s\subseteq A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)\right\}\in \mathrm{V}$$
31	21 22 30	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{PSubSp}\left(K\right)=\left\{s|\left(s\subseteq A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)\right\}$$
32	4 31	syl5eq	$$⊢K\in \mathrm{V}\to S=\left\{s|\left(s\subseteq A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)\right\}$$
33	5 32	syl	$$⊢K\in B\to S=\left\{s|\left(s\subseteq A\wedge \forall p\in s\forall q\in s\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in s\right)\right)\right\}$$