Theorem paddss

Description: Subset law for projective subspace sum. ( unss analog.) (Contributed by NM, 7-Mar-2012)

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

Proof

Step	Hyp	Ref	Expression
1		paddss.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		paddss.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
3		paddss.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
4		simpl	$$⊢\left(K\in B\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\in S\right)\right)\to K\in B$$
5		simpr1	$$⊢\left(K\in B\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\in S\right)\right)\to X\subseteq A$$
6		simpr2	$$⊢\left(K\in B\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\in S\right)\right)\to Y\subseteq A$$
7	1 2	psubssat	$$⊢\left(K\in B\wedge Z\in S\right)\to Z\subseteq A$$
8	7	3ad2antr3	$$⊢\left(K\in B\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\in S\right)\right)\to Z\subseteq A$$
9	1 3	paddssw1	$$⊢\left(K\in B\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to \left(\left(X\subseteq Z\wedge Y\subseteq Z\right)\to X\underset{\dot{}}{+}Y\subseteq Z\underset{\dot{}}{+}Z\right)$$
10	4 5 6 8 9	syl13anc	$$⊢\left(K\in B\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\in S\right)\right)\to \left(\left(X\subseteq Z\wedge Y\subseteq Z\right)\to X\underset{\dot{}}{+}Y\subseteq Z\underset{\dot{}}{+}Z\right)$$
11	2 3	paddidm	$$⊢\left(K\in B\wedge Z\in S\right)\to Z\underset{\dot{}}{+}Z=Z$$
12	11	3ad2antr3	$$⊢\left(K\in B\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\in S\right)\right)\to Z\underset{\dot{}}{+}Z=Z$$
13	12	sseq2d	$$⊢\left(K\in B\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\in S\right)\right)\to \left(X\underset{\dot{}}{+}Y\subseteq Z\underset{\dot{}}{+}Z\leftrightarrow X\underset{\dot{}}{+}Y\subseteq Z\right)$$
14	10 13	sylibd	$$⊢\left(K\in B\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\in S\right)\right)\to \left(\left(X\subseteq Z\wedge Y\subseteq Z\right)\to X\underset{\dot{}}{+}Y\subseteq Z\right)$$
15	1 3	paddssw2	$$⊢\left(K\in B\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to \left(X\underset{\dot{}}{+}Y\subseteq Z\to \left(X\subseteq Z\wedge Y\subseteq Z\right)\right)$$
16	4 5 6 8 15	syl13anc	$$⊢\left(K\in B\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\in S\right)\right)\to \left(X\underset{\dot{}}{+}Y\subseteq Z\to \left(X\subseteq Z\wedge Y\subseteq Z\right)\right)$$
17	14 16	impbid	$$⊢\left(K\in B\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\in S\right)\right)\to \left(\left(X\subseteq Z\wedge Y\subseteq Z\right)\leftrightarrow X\underset{\dot{}}{+}Y\subseteq Z\right)$$