Theorem prodpr

Description: A product over a pair is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022)

	Ref	Expression
Hypotheses	prodpr.1	$$⊢k=A\to D=E$$
	prodpr.2	$$⊢k=B\to D=F$$
	prodpr.a	$$⊢\phi \to A\in V$$
	prodpr.b	$$⊢\phi \to B\in W$$
	prodpr.e	$$⊢\phi \to E\in ℂ$$
	prodpr.f	$$⊢\phi \to F\in ℂ$$
	prodpr.3	$$⊢\phi \to A\ne B$$
Assertion	prodpr	$$⊢\phi \to \prod _{k\in \left\{A,B\right\}}D=EF$$

Proof

Step	Hyp	Ref	Expression
1		prodpr.1	$$⊢k=A\to D=E$$
2		prodpr.2	$$⊢k=B\to D=F$$
3		prodpr.a	$$⊢\phi \to A\in V$$
4		prodpr.b	$$⊢\phi \to B\in W$$
5		prodpr.e	$$⊢\phi \to E\in ℂ$$
6		prodpr.f	$$⊢\phi \to F\in ℂ$$
7		prodpr.3	$$⊢\phi \to A\ne B$$
8		disjsn2	$$⊢A\ne B\to \left\{A\right\}\cap \left\{B\right\}=\varnothing$$
9	7 8	syl	$$⊢\phi \to \left\{A\right\}\cap \left\{B\right\}=\varnothing$$
10		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
11	10	a1i	$$⊢\phi \to \left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
12		prfi	$$⊢\left\{A,B\right\}\in \mathrm{Fin}$$
13	12	a1i	$$⊢\phi \to \left\{A,B\right\}\in \mathrm{Fin}$$
14		vex	$$⊢k\in \mathrm{V}$$
15	14	elpr	$$⊢k\in \left\{A,B\right\}\leftrightarrow \left(k=A\vee k=B\right)$$
16	1	adantl	$$⊢\left(\phi \wedge k=A\right)\to D=E$$
17	5	adantr	$$⊢\left(\phi \wedge k=A\right)\to E\in ℂ$$
18	16 17	eqeltrd	$$⊢\left(\phi \wedge k=A\right)\to D\in ℂ$$
19	2	adantl	$$⊢\left(\phi \wedge k=B\right)\to D=F$$
20	6	adantr	$$⊢\left(\phi \wedge k=B\right)\to F\in ℂ$$
21	19 20	eqeltrd	$$⊢\left(\phi \wedge k=B\right)\to D\in ℂ$$
22	18 21	jaodan	$$⊢\left(\phi \wedge \left(k=A\vee k=B\right)\right)\to D\in ℂ$$
23	15 22	sylan2b	$$⊢\left(\phi \wedge k\in \left\{A,B\right\}\right)\to D\in ℂ$$
24	9 11 13 23	fprodsplit	$$⊢\phi \to \prod _{k\in \left\{A,B\right\}}D=\prod _{k\in \left\{A\right\}}D\prod _{k\in \left\{B\right\}}D$$
25	1	prodsn	$$⊢\left(A\in V\wedge E\in ℂ\right)\to \prod _{k\in \left\{A\right\}}D=E$$
26	3 5 25	syl2anc	$$⊢\phi \to \prod _{k\in \left\{A\right\}}D=E$$
27	2	prodsn	$$⊢\left(B\in W\wedge F\in ℂ\right)\to \prod _{k\in \left\{B\right\}}D=F$$
28	4 6 27	syl2anc	$$⊢\phi \to \prod _{k\in \left\{B\right\}}D=F$$
29	26 28	oveq12d	$$⊢\phi \to \prod _{k\in \left\{A\right\}}D\prod _{k\in \left\{B\right\}}D=EF$$
30	24 29	eqtrd	$$⊢\phi \to \prod _{k\in \left\{A,B\right\}}D=EF$$