Theorem xpun

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

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

Proof

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