Theorem xpriindi

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

	Ref	Expression
Assertion	xpriindi	$$⊢C\times \left(D\cap \bigcap _{x\in A}B\right)=\left(C\times D\right)\cap \bigcap _{x\in A}\left(C\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		iineq1	$$⊢A=\varnothing \to \bigcap _{x\in A}B=\bigcap _{x\in \varnothing }B$$
2		0iin	$$⊢\bigcap _{x\in \varnothing }B=\mathrm{V}$$
3	1 2	eqtrdi	$$⊢A=\varnothing \to \bigcap _{x\in A}B=\mathrm{V}$$
4	3	ineq2d	$$⊢A=\varnothing \to D\cap \bigcap _{x\in A}B=D\cap \mathrm{V}$$
5		inv1	$$⊢D\cap \mathrm{V}=D$$
6	4 5	eqtrdi	$$⊢A=\varnothing \to D\cap \bigcap _{x\in A}B=D$$
7	6	xpeq2d	$$⊢A=\varnothing \to C\times \left(D\cap \bigcap _{x\in A}B\right)=C\times D$$
8		iineq1	$$⊢A=\varnothing \to \bigcap _{x\in A}\left(C\times B\right)=\bigcap _{x\in \varnothing }\left(C\times B\right)$$
9		0iin	$$⊢\bigcap _{x\in \varnothing }\left(C\times B\right)=\mathrm{V}$$
10	8 9	eqtrdi	$$⊢A=\varnothing \to \bigcap _{x\in A}\left(C\times B\right)=\mathrm{V}$$
11	10	ineq2d	$$⊢A=\varnothing \to \left(C\times D\right)\cap \bigcap _{x\in A}\left(C\times B\right)=\left(C\times D\right)\cap \mathrm{V}$$
12		inv1	$$⊢\left(C\times D\right)\cap \mathrm{V}=C\times D$$
13	11 12	eqtrdi	$$⊢A=\varnothing \to \left(C\times D\right)\cap \bigcap _{x\in A}\left(C\times B\right)=C\times D$$
14	7 13	eqtr4d	$$⊢A=\varnothing \to C\times \left(D\cap \bigcap _{x\in A}B\right)=\left(C\times D\right)\cap \bigcap _{x\in A}\left(C\times B\right)$$
15		xpindi	$$⊢C\times \left(D\cap \bigcap _{x\in A}B\right)=\left(C\times D\right)\cap \left(C\times \bigcap _{x\in A}B\right)$$
16		xpiindi	$$⊢A\ne \varnothing \to C\times \bigcap _{x\in A}B=\bigcap _{x\in A}\left(C\times B\right)$$
17	16	ineq2d	$$⊢A\ne \varnothing \to \left(C\times D\right)\cap \left(C\times \bigcap _{x\in A}B\right)=\left(C\times D\right)\cap \bigcap _{x\in A}\left(C\times B\right)$$
18	15 17	syl5eq	$$⊢A\ne \varnothing \to C\times \left(D\cap \bigcap _{x\in A}B\right)=\left(C\times D\right)\cap \bigcap _{x\in A}\left(C\times B\right)$$
19	14 18	pm2.61ine	$$⊢C\times \left(D\cap \bigcap _{x\in A}B\right)=\left(C\times D\right)\cap \bigcap _{x\in A}\left(C\times B\right)$$