Theorem paddval0

Description: Projective subspace sum with at least one 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	paddval0	$$⊢\left(\left(K\in B\wedge X\subseteq A\wedge Y\subseteq A\right)\wedge \neg \left(X\ne \varnothing \wedge Y\ne \varnothing \right)\right)\to X\underset{\dot{}}{+}Y=X\cup Y$$

Proof

Step	Hyp	Ref	Expression
1		padd0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		padd0.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
3	1 2	elpadd0	$$⊢\left(\left(K\in B\wedge X\subseteq A\wedge Y\subseteq A\right)\wedge \neg \left(X\ne \varnothing \wedge Y\ne \varnothing \right)\right)\to \left(q\in \left(X\underset{\dot{}}{+}Y\right)\leftrightarrow \left(q\in X\vee q\in Y\right)\right)$$
4		elun	$$⊢q\in \left(X\cup Y\right)\leftrightarrow \left(q\in X\vee q\in Y\right)$$
5	3 4	bitr4di	$$⊢\left(\left(K\in B\wedge X\subseteq A\wedge Y\subseteq A\right)\wedge \neg \left(X\ne \varnothing \wedge Y\ne \varnothing \right)\right)\to \left(q\in \left(X\underset{\dot{}}{+}Y\right)\leftrightarrow q\in \left(X\cup Y\right)\right)$$
6	5	eqrdv	$$⊢\left(\left(K\in B\wedge X\subseteq A\wedge Y\subseteq A\right)\wedge \neg \left(X\ne \varnothing \wedge Y\ne \varnothing \right)\right)\to X\underset{\dot{}}{+}Y=X\cup Y$$