Theorem padd02

Description: Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012)

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

Proof

Step	Hyp	Ref	Expression
1		padd0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		padd0.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
3		simpl	$$⊢\left(K\in B\wedge X\subseteq A\right)\to K\in B$$
4		0ss	$$⊢\varnothing \subseteq A$$
5	4	a1i	$$⊢\left(K\in B\wedge X\subseteq A\right)\to \varnothing \subseteq A$$
6		simpr	$$⊢\left(K\in B\wedge X\subseteq A\right)\to X\subseteq A$$
7	3 5 6	3jca	$$⊢\left(K\in B\wedge X\subseteq A\right)\to \left(K\in B\wedge \varnothing \subseteq A\wedge X\subseteq A\right)$$
8		neirr	$$⊢\neg \varnothing \ne \varnothing$$
9	8	intnanr	$$⊢\neg \left(\varnothing \ne \varnothing \wedge X\ne \varnothing \right)$$
10	1 2	paddval0	$$⊢\left(\left(K\in B\wedge \varnothing \subseteq A\wedge X\subseteq A\right)\wedge \neg \left(\varnothing \ne \varnothing \wedge X\ne \varnothing \right)\right)\to \varnothing \underset{\dot{}}{+}X=\varnothing \cup X$$
11	7 9 10	sylancl	$$⊢\left(K\in B\wedge X\subseteq A\right)\to \varnothing \underset{\dot{}}{+}X=\varnothing \cup X$$
12		uncom	$$⊢\varnothing \cup X=X\cup \varnothing$$
13		un0	$$⊢X\cup \varnothing =X$$
14	12 13	eqtri	$$⊢\varnothing \cup X=X$$
15	11 14	eqtrdi	$$⊢\left(K\in B\wedge X\subseteq A\right)\to \varnothing \underset{\dot{}}{+}X=X$$