paddval0

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

	Ref	Expression
Hypotheses	padd0.a	$⊢ A = Atoms (K)$
	padd0.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	paddval0	$⊢ ((K \in B \land X \subseteq A \land Y \subseteq A) \land \neg (X \neq \emptyset \land Y \neq \emptyset)) \to X \underset{˙}{+} Y = X \cup Y$

Step	Hyp	Ref	Expression
1		padd0.a	$⊢ A = Atoms (K)$
2		padd0.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3	1 2	elpadd0	$⊢ ((K \in B \land X \subseteq A \land Y \subseteq A) \land \neg (X \neq \emptyset \land Y \neq \emptyset)) \to (q \in (X \underset{˙}{+} Y) \leftrightarrow (q \in X \lor q \in Y))$
4		elun	$⊢ q \in (X \cup Y) \leftrightarrow (q \in X \lor q \in Y)$
5	3 4	bitr4di	$⊢ ((K \in B \land X \subseteq A \land Y \subseteq A) \land \neg (X \neq \emptyset \land Y \neq \emptyset)) \to (q \in (X \underset{˙}{+} Y) \leftrightarrow q \in (X \cup Y))$
6	5	eqrdv	$⊢ ((K \in B \land X \subseteq A \land Y \subseteq A) \land \neg (X \neq \emptyset \land Y \neq \emptyset)) \to X \underset{˙}{+} Y = X \cup Y$

Metamath Proof Explorer