Theorem sspadd2

Description: A projective subspace sum is a superset of its second summand. ( ssun2 analog.) (Contributed by NM, 3-Jan-2012)

	Ref	Expression
Hypotheses	padd0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	padd0.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
Assertion	sspadd2	$$⊢\left(K\in B\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\subseteq Y\underset{\dot{}}{+}X$$

Proof

Step	Hyp	Ref	Expression
1		padd0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		padd0.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
3		ssun2	$$⊢X\subseteq Y\cup X$$
4		ssun1	$$⊢Y\cup X\subseteq \left(Y\cup X\right)\cup \left\{p\in A|\exists q\in Y\exists r\in Xp{\le }_K\left(q\mathrm{join}\left(K\right)r\right)\right\}$$
5	3 4	sstri	$$⊢X\subseteq \left(Y\cup X\right)\cup \left\{p\in A|\exists q\in Y\exists r\in Xp{\le }_K\left(q\mathrm{join}\left(K\right)r\right)\right\}$$
6		eqid	$$⊢{\le }_K={\le }_K$$
7		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
8	6 7 1 2	paddval	$$⊢\left(K\in B\wedge Y\subseteq A\wedge X\subseteq A\right)\to Y\underset{\dot{}}{+}X=\left(Y\cup X\right)\cup \left\{p\in A|\exists q\in Y\exists r\in Xp{\le }_K\left(q\mathrm{join}\left(K\right)r\right)\right\}$$
9	8	3com23	$$⊢\left(K\in B\wedge X\subseteq A\wedge Y\subseteq A\right)\to Y\underset{\dot{}}{+}X=\left(Y\cup X\right)\cup \left\{p\in A|\exists q\in Y\exists r\in Xp{\le }_K\left(q\mathrm{join}\left(K\right)r\right)\right\}$$
10	5 9	sseqtrrid	$$⊢\left(K\in B\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\subseteq Y\underset{\dot{}}{+}X$$