Theorem sspadd1

Description: A projective subspace sum is a superset of its first summand. ( ssun1 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	sspadd1	$$⊢\left(K\in B\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\subseteq X\underset{\dot{}}{+}Y$$

Proof

Step	Hyp	Ref	Expression
1		padd0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		padd0.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
3		ssun1	$$⊢X\subseteq X\cup Y$$
4		ssun1	$$⊢X\cup Y\subseteq \left(X\cup Y\right)\cup \left\{p\in A|\exists q\in X\exists r\in Yp{\le }_K\left(q\mathrm{join}\left(K\right)r\right)\right\}$$
5	3 4	sstri	$$⊢X\subseteq \left(X\cup Y\right)\cup \left\{p\in A|\exists q\in X\exists r\in Yp{\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 X\subseteq A\wedge Y\subseteq A\right)\to X\underset{\dot{}}{+}Y=\left(X\cup Y\right)\cup \left\{p\in A|\exists q\in X\exists r\in Yp{\le }_K\left(q\mathrm{join}\left(K\right)r\right)\right\}$$
9	5 8	sseqtrrid	$$⊢\left(K\in B\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\subseteq X\underset{\dot{}}{+}Y$$