Theorem ispsubsp

Description: The predicate "is a projective subspace". (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	ispsubsp	$$⊢K\in D\to \left(X\in S\leftrightarrow \left(X\subseteq A\wedge \forall p\in X\forall q\in X\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in X\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	1 2 3 4	psubspset	$$⊢K\in D\to S=\left\{x|\left(x\subseteq A\wedge \forall p\in x\forall q\in x\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in x\right)\right)\right\}$$
6	5	eleq2d	$$⊢K\in D\to \left(X\in S\leftrightarrow X\in \left\{x|\left(x\subseteq A\wedge \forall p\in x\forall q\in x\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in x\right)\right)\right\}\right)$$
7	3	fvexi	$$⊢A\in \mathrm{V}$$
8	7	ssex	$$⊢X\subseteq A\to X\in \mathrm{V}$$
9	8	adantr	$$⊢\left(X\subseteq A\wedge \forall p\in X\forall q\in X\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in X\right)\right)\to X\in \mathrm{V}$$
10		sseq1	$$⊢x=X\to \left(x\subseteq A\leftrightarrow X\subseteq A\right)$$
11		eleq2	$$⊢x=X\to \left(r\in x\leftrightarrow r\in X\right)$$
12	11	imbi2d	$$⊢x=X\to \left(\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in x\right)\leftrightarrow \left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in X\right)\right)$$
13	12	ralbidv	$$⊢x=X\to \left(\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in x\right)\leftrightarrow \forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in X\right)\right)$$
14	13	raleqbi1dv	$$⊢x=X\to \left(\forall q\in x\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in x\right)\leftrightarrow \forall q\in X\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in X\right)\right)$$
15	14	raleqbi1dv	$$⊢x=X\to \left(\forall p\in x\forall q\in x\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in x\right)\leftrightarrow \forall p\in X\forall q\in X\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in X\right)\right)$$
16	10 15	anbi12d	$$⊢x=X\to \left(\left(x\subseteq A\wedge \forall p\in x\forall q\in x\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in x\right)\right)\leftrightarrow \left(X\subseteq A\wedge \forall p\in X\forall q\in X\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in X\right)\right)\right)$$
17	9 16	elab3	$$⊢X\in \left\{x|\left(x\subseteq A\wedge \forall p\in x\forall q\in x\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in x\right)\right)\right\}\leftrightarrow \left(X\subseteq A\wedge \forall p\in X\forall q\in X\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in X\right)\right)$$
18	6 17	syl6bb	$$⊢K\in D\to \left(X\in S\leftrightarrow \left(X\subseteq A\wedge \forall p\in X\forall q\in X\forall r\in A\left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\to r\in X\right)\right)\right)$$