This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( 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 ) )