Theorem ispsubsp2

Description: The predicate "is a projective subspace". (Contributed by NM, 13-Jan-2012)

	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	ispsubsp2	$$⊢K\in D\to \left(X\in S\leftrightarrow \left(X\subseteq A\wedge \forall p\in A\left(\exists q\in X\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\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	ispsubsp	$$⊢K\in D\to \left(X\in S\leftrightarrow \left(X\subseteq A\wedge \forall q\in X\forall r\in X\forall p\in A\left(p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\right)\right)$$
6		ralcom	$$⊢\forall r\in X\forall p\in A\left(p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\leftrightarrow \forall p\in A\forall r\in X\left(p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)$$
7		r19.23v	$$⊢\forall r\in X\left(p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\leftrightarrow \left(\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)$$
8	7	ralbii	$$⊢\forall p\in A\forall r\in X\left(p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\leftrightarrow \forall p\in A\left(\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)$$
9	6 8	bitri	$$⊢\forall r\in X\forall p\in A\left(p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\leftrightarrow \forall p\in A\left(\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)$$
10	9	ralbii	$$⊢\forall q\in X\forall r\in X\forall p\in A\left(p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\leftrightarrow \forall q\in X\forall p\in A\left(\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)$$
11		ralcom	$$⊢\forall q\in X\forall p\in A\left(\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\leftrightarrow \forall p\in A\forall q\in X\left(\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)$$
12		r19.23v	$$⊢\forall q\in X\left(\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\leftrightarrow \left(\exists q\in X\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)$$
13	12	ralbii	$$⊢\forall p\in A\forall q\in X\left(\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\leftrightarrow \forall p\in A\left(\exists q\in X\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)$$
14	11 13	bitri	$$⊢\forall q\in X\forall p\in A\left(\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\leftrightarrow \forall p\in A\left(\exists q\in X\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)$$
15	10 14	bitri	$$⊢\forall q\in X\forall r\in X\forall p\in A\left(p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\leftrightarrow \forall p\in A\left(\exists q\in X\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)$$
16	15	a1i	$$⊢K\in D\to \left(\forall q\in X\forall r\in X\forall p\in A\left(p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\leftrightarrow \forall p\in A\left(\exists q\in X\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\right)$$
17	16	anbi2d	$$⊢K\in D\to \left(\left(X\subseteq A\wedge \forall q\in X\forall r\in X\forall p\in A\left(p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\right)\leftrightarrow \left(X\subseteq A\wedge \forall p\in A\left(\exists q\in X\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\right)\right)$$
18	5 17	bitrd	$$⊢K\in D\to \left(X\in S\leftrightarrow \left(X\subseteq A\wedge \forall p\in A\left(\exists q\in X\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\to p\in X\right)\right)\right)$$