xpdjuen

Description: Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of Enderton p. 142. (Contributed by NM, 26-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

		Ref	Expression
	Assertion	xpdjuen	$⊢ (A \in V \land B \in W \land C \in X) \to (A \times (B ⊔︀ C)) \approx ((A \times B) ⊔︀ (A \times C))$

Proof

Step	Hyp	Ref	Expression
1		enrefg	$⊢ A \in V \to A \approx A$
2	1	3ad2ant1	$⊢ (A \in V \land B \in W \land C \in X) \to A \approx A$
3		0ex	$⊢ \emptyset \in V$
4		simp2	$⊢ (A \in V \land B \in W \land C \in X) \to B \in W$
5		xpsnen2g	$⊢ (\emptyset \in V \land B \in W) \to (\{\emptyset\} \times B) \approx B$
6	3 4 5	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to (\{\emptyset\} \times B) \approx B$
7	6	ensymd	$⊢ (A \in V \land B \in W \land C \in X) \to B \approx (\{\emptyset\} \times B)$
8		xpen	$⊢ (A \approx A \land B \approx (\{\emptyset\} \times B)) \to (A \times B) \approx (A \times (\{\emptyset\} \times B))$
9	2 7 8	syl2anc	$⊢ (A \in V \land B \in W \land C \in X) \to (A \times B) \approx (A \times (\{\emptyset\} \times B))$
10		1on	$⊢ 1_{𝑜} \in On$
11		simp3	$⊢ (A \in V \land B \in W \land C \in X) \to C \in X$
12		xpsnen2g	$⊢ (1_{𝑜} \in On \land C \in X) \to (\{1_{𝑜}\} \times C) \approx C$
13	10 11 12	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to (\{1_{𝑜}\} \times C) \approx C$
14	13	ensymd	$⊢ (A \in V \land B \in W \land C \in X) \to C \approx (\{1_{𝑜}\} \times C)$
15		xpen	$⊢ (A \approx A \land C \approx (\{1_{𝑜}\} \times C)) \to (A \times C) \approx (A \times (\{1_{𝑜}\} \times C))$
16	2 14 15	syl2anc	$⊢ (A \in V \land B \in W \land C \in X) \to (A \times C) \approx (A \times (\{1_{𝑜}\} \times C))$
17		xp01disjl	$⊢ (\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times C) = \emptyset$
18	17	xpeq2i	$⊢ A \times ((\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times C)) = A \times \emptyset$
19		xpindi	$⊢ A \times ((\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times C)) = (A \times (\{\emptyset\} \times B)) \cap (A \times (\{1_{𝑜}\} \times C))$
20		xp0	$⊢ A \times \emptyset = \emptyset$
21	18 19 20	3eqtr3i	$⊢ (A \times (\{\emptyset\} \times B)) \cap (A \times (\{1_{𝑜}\} \times C)) = \emptyset$
22	21	a1i	$⊢ (A \in V \land B \in W \land C \in X) \to (A \times (\{\emptyset\} \times B)) \cap (A \times (\{1_{𝑜}\} \times C)) = \emptyset$
23		djuenun	$⊢ ((A \times B) \approx (A \times (\{\emptyset\} \times B)) \land (A \times C) \approx (A \times (\{1_{𝑜}\} \times C)) \land (A \times (\{\emptyset\} \times B)) \cap (A \times (\{1_{𝑜}\} \times C)) = \emptyset) \to ((A \times B) ⊔︀ (A \times C)) \approx ((A \times (\{\emptyset\} \times B)) \cup (A \times (\{1_{𝑜}\} \times C)))$
24	9 16 22 23	syl3anc	$⊢ (A \in V \land B \in W \land C \in X) \to ((A \times B) ⊔︀ (A \times C)) \approx ((A \times (\{\emptyset\} \times B)) \cup (A \times (\{1_{𝑜}\} \times C)))$
25		df-dju	$⊢ (B ⊔︀ C) = (\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C)$
26	25	xpeq2i	$⊢ A \times (B ⊔︀ C) = A \times ((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C))$
27		xpundi	$⊢ A \times ((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C)) = (A \times (\{\emptyset\} \times B)) \cup (A \times (\{1_{𝑜}\} \times C))$
28	26 27	eqtri	$⊢ A \times (B ⊔︀ C) = (A \times (\{\emptyset\} \times B)) \cup (A \times (\{1_{𝑜}\} \times C))$
29	24 28	breqtrrdi	$⊢ (A \in V \land B \in W \land C \in X) \to ((A \times B) ⊔︀ (A \times C)) \approx (A \times (B ⊔︀ C))$
30	29	ensymd	$⊢ (A \in V \land B \in W \land C \in X) \to (A \times (B ⊔︀ C)) \approx ((A \times B) ⊔︀ (A \times C))$

Metamath Proof Explorer

Theorem xpdjuen

Proof