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	syl6eq	⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = V )
4	3	ineq2d	⊢ ( 𝐴 = ∅ → ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) = ( 𝐷 ∩ V ) )
5		inv1	⊢ ( 𝐷 ∩ V ) = 𝐷
6	4 5	syl6eq	⊢ ( 𝐴 = ∅ → ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) = 𝐷 )
7	6	xpeq2d	⊢ ( 𝐴 = ∅ → ( 𝐶 × ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( 𝐶 × 𝐷 ) )
8		iineq1	⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) = ∩ 𝑥 ∈ ∅ ( 𝐶 × 𝐵 ) )
9		0iin	⊢ ∩ 𝑥 ∈ ∅ ( 𝐶 × 𝐵 ) = V
10	8 9	syl6eq	⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) = V )
11	10	ineq2d	⊢ ( 𝐴 = ∅ → ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ V ) )
12		inv1	⊢ ( ( 𝐶 × 𝐷 ) ∩ V ) = ( 𝐶 × 𝐷 )
13	11 12	syl6eq	⊢ ( 𝐴 = ∅ → ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) = ( 𝐶 × 𝐷 ) )
14	7 13	eqtr4d	⊢ ( 𝐴 = ∅ → ( 𝐶 × ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) )
15		xpindi	⊢ ( 𝐶 × ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) )
16		xpiindi	⊢ ( 𝐴 ≠ ∅ → ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) = ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) )
17	16	ineq2d	⊢ ( 𝐴 ≠ ∅ → ( ( 𝐶 × 𝐷 ) ∩ ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) )
18	15 17	syl5eq	⊢ ( 𝐴 ≠ ∅ → ( 𝐶 × ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) )
19	14 18	pm2.61ine	⊢ ( 𝐶 × ( 𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ) = ( ( 𝐶 × 𝐷 ) ∩ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) )