Theorem padd01

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	padd01	$$⊢\left(K\in B\wedge X\subseteq A\right)\to X\underset{\dot{}}{+}\varnothing =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		simpr	$$⊢\left(K\in B\wedge X\subseteq A\right)\to X\subseteq A$$
5		0ss	$$⊢\varnothing \subseteq A$$
6	5	a1i	$$⊢\left(K\in B\wedge X\subseteq A\right)\to \varnothing \subseteq A$$
7	3 4 6	3jca	$$⊢\left(K\in B\wedge X\subseteq A\right)\to \left(K\in B\wedge X\subseteq A\wedge \varnothing \subseteq A\right)$$
8		neirr	$$⊢\neg \varnothing \ne \varnothing$$
9	8	intnan	$$⊢\neg \left(X\ne \varnothing \wedge \varnothing \ne \varnothing \right)$$
10	1 2	paddval0	$$⊢\left(\left(K\in B\wedge X\subseteq A\wedge \varnothing \subseteq A\right)\wedge \neg \left(X\ne \varnothing \wedge \varnothing \ne \varnothing \right)\right)\to X\underset{\dot{}}{+}\varnothing =X\cup \varnothing$$
11	7 9 10	sylancl	$$⊢\left(K\in B\wedge X\subseteq A\right)\to X\underset{\dot{}}{+}\varnothing =X\cup \varnothing$$
12		un0	$$⊢X\cup \varnothing =X$$
13	11 12	eqtrdi	$$⊢\left(K\in B\wedge X\subseteq A\right)\to X\underset{\dot{}}{+}\varnothing =X$$