xpun

Description: The Cartesian product of two unions. (Contributed by NM, 12-Aug-2004)

		Ref	Expression
	Assertion	xpun	$⊢ (A \cup B) \times (C \cup D) = ((A \times C) \cup (A \times D)) \cup ((B \times C) \cup (B \times D))$

Step	Hyp	Ref	Expression
1		xpundi	$⊢ (A \cup B) \times (C \cup D) = ((A \cup B) \times C) \cup ((A \cup B) \times D)$
2		xpundir	$⊢ (A \cup B) \times C = (A \times C) \cup (B \times C)$
3		xpundir	$⊢ (A \cup B) \times D = (A \times D) \cup (B \times D)$
4	2 3	uneq12i	$⊢ ((A \cup B) \times C) \cup ((A \cup B) \times D) = ((A \times C) \cup (B \times C)) \cup ((A \times D) \cup (B \times D))$
5		un4	$⊢ ((A \times C) \cup (B \times C)) \cup ((A \times D) \cup (B \times D)) = ((A \times C) \cup (A \times D)) \cup ((B \times C) \cup (B \times D))$
6	1 4 5	3eqtri	$⊢ (A \cup B) \times (C \cup D) = ((A \times C) \cup (A \times D)) \cup ((B \times C) \cup (B \times D))$

Metamath Proof Explorer