Theorem psubspi2N

Description: Property of a projective subspace. (Contributed by NM, 13-Jan-2012) (New usage is discouraged.)

	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	psubspi2N	$$⊢\left(\left(K\in D\wedge X\in S\wedge P\in A\right)\wedge \left(Q\in X\wedge R\in X\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\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		oveq1	$$⊢q=Q\to q\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r$$
6	5	breq2d	$$⊢q=Q\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)$$
7		oveq2	$$⊢r=R\to Q\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }R$$
8	7	breq2d	$$⊢r=R\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	6 8	rspc2ev	$$⊢\left(Q\in X\wedge R\in X\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\to \exists q\in X\exists r\in XP\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)$$
10	1 2 3 4	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$$
11	9 10	sylan2	$$⊢\left(\left(K\in D\wedge X\in S\wedge P\in A\right)\wedge \left(Q\in X\wedge R\in X\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\right)\to P\in X$$