padd01

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

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

Step	Hyp	Ref	Expression
1		padd0.a	$⊢ A = Atoms (K)$
2		padd0.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		simpl	$⊢ (K \in B \land X \subseteq A) \to K \in B$
4		simpr	$⊢ (K \in B \land X \subseteq A) \to X \subseteq A$
5		0ss	$⊢ \emptyset \subseteq A$
6	5	a1i	$⊢ (K \in B \land X \subseteq A) \to \emptyset \subseteq A$
7	3 4 6	3jca	$⊢ (K \in B \land X \subseteq A) \to (K \in B \land X \subseteq A \land \emptyset \subseteq A)$
8		neirr	$⊢ \neg \emptyset \neq \emptyset$
9	8	intnan	$⊢ \neg (X \neq \emptyset \land \emptyset \neq \emptyset)$
10	1 2	paddval0	$⊢ ((K \in B \land X \subseteq A \land \emptyset \subseteq A) \land \neg (X \neq \emptyset \land \emptyset \neq \emptyset)) \to X \underset{˙}{+} \emptyset = X \cup \emptyset$
11	7 9 10	sylancl	$⊢ (K \in B \land X \subseteq A) \to X \underset{˙}{+} \emptyset = X \cup \emptyset$
12		un0	$⊢ X \cup \emptyset = X$
13	11 12	eqtrdi	$⊢ (K \in B \land X \subseteq A) \to X \underset{˙}{+} \emptyset = X$

Metamath Proof Explorer