Theorem psubspi

Description: Property of 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	psubspi	$$⊢\left(\left(K\in D\wedge X\in S\wedge P\in A\right)\wedge \exists q\in X\exists r\in XP\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right)\to P\in X$$

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	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)$$
6	5	simplbda	$$⊢\left(K\in D\wedge X\in S\right)\to \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)$$
7	6	ex	$$⊢K\in D\to \left(X\in S\to \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)$$
8		breq1	$$⊢p=P\to \left(p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\leftrightarrow P\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right)$$
9	8	2rexbidv	$$⊢p=P\to \left(\exists q\in X\exists r\in Xp\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\leftrightarrow \exists q\in X\exists r\in XP\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right)$$
10		eleq1	$$⊢p=P\to \left(p\in X\leftrightarrow P\in X\right)$$
11	9 10	imbi12d	$$⊢p=P\to \left(\left(\exists q\in X\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)\right)$$
12	11	rspccv	$$⊢\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)\to \left(P\in A\to \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)$$
13	7 12	syl6	$$⊢K\in D\to \left(X\in S\to \left(P\in A\to \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)$$
14	13	3imp1	$$⊢\left(\left(K\in D\wedge X\in S\wedge P\in A\right)\wedge \exists q\in X\exists r\in XP\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right)\to P\in X$$