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 ( 𝐶 × ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 iineq1 ⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ ∅ 𝐵 )
2 0iin ⊢ ∩ 𝑥 ∈ ∅ 𝐵 = V
3 1 2 eqtrdi ⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = V )
4 3 ineq2d ⊢ ( 𝐴 = ∅ → ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) = ( 𝐷 ∩ V ) )
5 inv1 ⊢ ( 𝐷 ∩ V ) = 𝐷
6 4 5 eqtrdi ⊢ ( 𝐴 = ∅ → ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) = 𝐷 )
7 6 xpeq2d ⊢ ( 𝐴 = ∅ → ( 𝐶 × ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( 𝐶 × 𝐷 ) )
8 iineq1 ⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) = ∩ 𝑥 ∈ ∅ ( 𝐶 × 𝐵 ) )
9 0iin ⊢ ∩ 𝑥 ∈ ∅ ( 𝐶 × 𝐵 ) = V
10 8 9 eqtrdi ⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) = V )
11 10 ineq2d ⊢ ( 𝐴 = ∅ → ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ V ) )
12 inv1 ⊢ ( ( 𝐶 × 𝐷 ) ∩ V ) = ( 𝐶 × 𝐷 )
13 11 12 eqtrdi ⊢ ( 𝐴 = ∅ → ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) = ( 𝐶 × 𝐷 ) )
14 7 13 eqtr4d ⊢ ( 𝐴 = ∅ → ( 𝐶 × ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) )
15 xpindi ⊢ ( 𝐶 × ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) )
16 xpiindi ⊢ ( 𝐴 ≠ ∅ → ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) = ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) )
17 16 ineq2d ⊢ ( 𝐴 ≠ ∅ → ( ( 𝐶 × 𝐷 ) ∩ ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) )
18 15 17 eqtrid ⊢ ( 𝐴 ≠ ∅ → ( 𝐶 × ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) )
19 14 18 pm2.61ine ⊢ ( 𝐶 × ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) )