Theorem xpun

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

	Ref	Expression
Assertion	xpun	|- ( ( A u. B ) X. ( C u. D ) ) = ( ( ( A X. C ) u. ( A X. D ) ) u. ( ( B X. C ) u. ( B X. D ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpundi	|- ( ( A u. B ) X. ( C u. D ) ) = ( ( ( A u. B ) X. C ) u. ( ( A u. B ) X. D ) )
2		xpundir	|- ( ( A u. B ) X. C ) = ( ( A X. C ) u. ( B X. C ) )
3		xpundir	|- ( ( A u. B ) X. D ) = ( ( A X. D ) u. ( B X. D ) )
4	2 3	uneq12i	|- ( ( ( A u. B ) X. C ) u. ( ( A u. B ) X. D ) ) = ( ( ( A X. C ) u. ( B X. C ) ) u. ( ( A X. D ) u. ( B X. D ) ) )
5		un4	|- ( ( ( A X. C ) u. ( B X. C ) ) u. ( ( A X. D ) u. ( B X. D ) ) ) = ( ( ( A X. C ) u. ( A X. D ) ) u. ( ( B X. C ) u. ( B X. D ) ) )
6	1 4 5	3eqtri	|- ( ( A u. B ) X. ( C u. D ) ) = ( ( ( A X. C ) u. ( A X. D ) ) u. ( ( B X. C ) u. ( B X. D ) ) )