Theorem xpriindi

Description: Distributive law for Cartesian product over relativized indexed intersection. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	xpriindi	|- ( C X. ( D i^i |^|_ x e. A B ) ) = ( ( C X. D ) i^i |^|_ x e. A ( C X. B ) )

Proof

Step	Hyp	Ref	Expression
1		iineq1	|- ( A = (/) -> |^|_ x e. A B = |^|_ x e. (/) B )
2		0iin	|- |^|_ x e. (/) B = _V
3	1 2	eqtrdi	|- ( A = (/) -> |^|_ x e. A B = _V )
4	3	ineq2d	|- ( A = (/) -> ( D i^i |^|_ x e. A B ) = ( D i^i _V ) )
5		inv1	|- ( D i^i _V ) = D
6	4 5	eqtrdi	|- ( A = (/) -> ( D i^i |^|_ x e. A B ) = D )
7	6	xpeq2d	|- ( A = (/) -> ( C X. ( D i^i |^|_ x e. A B ) ) = ( C X. D ) )
8		iineq1	|- ( A = (/) -> |^|_ x e. A ( C X. B ) = |^|_ x e. (/) ( C X. B ) )
9		0iin	|- |^|_ x e. (/) ( C X. B ) = _V
10	8 9	eqtrdi	|- ( A = (/) -> |^|_ x e. A ( C X. B ) = _V )
11	10	ineq2d	|- ( A = (/) -> ( ( C X. D ) i^i |^|_ x e. A ( C X. B ) ) = ( ( C X. D ) i^i _V ) )
12		inv1	|- ( ( C X. D ) i^i _V ) = ( C X. D )
13	11 12	eqtrdi	|- ( A = (/) -> ( ( C X. D ) i^i |^|_ x e. A ( C X. B ) ) = ( C X. D ) )
14	7 13	eqtr4d	|- ( A = (/) -> ( C X. ( D i^i |^|_ x e. A B ) ) = ( ( C X. D ) i^i |^|_ x e. A ( C X. B ) ) )
15		xpindi	|- ( C X. ( D i^i |^|_ x e. A B ) ) = ( ( C X. D ) i^i ( C X. |^|_ x e. A B ) )
16		xpiindi	|- ( A =/= (/) -> ( C X. |^|_ x e. A B ) = |^|_ x e. A ( C X. B ) )
17	16	ineq2d	|- ( A =/= (/) -> ( ( C X. D ) i^i ( C X. |^|_ x e. A B ) ) = ( ( C X. D ) i^i |^|_ x e. A ( C X. B ) ) )
18	15 17	syl5eq	|- ( A =/= (/) -> ( C X. ( D i^i |^|_ x e. A B ) ) = ( ( C X. D ) i^i |^|_ x e. A ( C X. B ) ) )
19	14 18	pm2.61ine	|- ( C X. ( D i^i |^|_ x e. A B ) ) = ( ( C X. D ) i^i |^|_ x e. A ( C X. B ) )