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 -> D = E )
	prodpr.2	|- ( k = B -> D = F )
	prodpr.a	|- ( ph -> A e. V )
	prodpr.b	|- ( ph -> B e. W )
	prodpr.e	|- ( ph -> E e. CC )
	prodpr.f	|- ( ph -> F e. CC )
	prodpr.3	|- ( ph -> A =/= B )
Assertion	prodpr	|- ( ph -> prod_ k e. { A , B } D = ( E x. F ) )

Proof

Step	Hyp	Ref	Expression
1		prodpr.1	|- ( k = A -> D = E )
2		prodpr.2	|- ( k = B -> D = F )
3		prodpr.a	|- ( ph -> A e. V )
4		prodpr.b	|- ( ph -> B e. W )
5		prodpr.e	|- ( ph -> E e. CC )
6		prodpr.f	|- ( ph -> F e. CC )
7		prodpr.3	|- ( ph -> A =/= B )
8		disjsn2	|- ( A =/= B -> ( { A } i^i { B } ) = (/) )
9	7 8	syl	|- ( ph -> ( { A } i^i { B } ) = (/) )
10		df-pr	|- { A , B } = ( { A } u. { B } )
11	10	a1i	|- ( ph -> { A , B } = ( { A } u. { B } ) )
12		prfi	|- { A , B } e. Fin
13	12	a1i	|- ( ph -> { A , B } e. Fin )
14		vex	|- k e. _V
15	14	elpr	|- ( k e. { A , B } <-> ( k = A \/ k = B ) )
16	1	adantl	|- ( ( ph /\ k = A ) -> D = E )
17	5	adantr	|- ( ( ph /\ k = A ) -> E e. CC )
18	16 17	eqeltrd	|- ( ( ph /\ k = A ) -> D e. CC )
19	2	adantl	|- ( ( ph /\ k = B ) -> D = F )
20	6	adantr	|- ( ( ph /\ k = B ) -> F e. CC )
21	19 20	eqeltrd	|- ( ( ph /\ k = B ) -> D e. CC )
22	18 21	jaodan	|- ( ( ph /\ ( k = A \/ k = B ) ) -> D e. CC )
23	15 22	sylan2b	|- ( ( ph /\ k e. { A , B } ) -> D e. CC )
24	9 11 13 23	fprodsplit	|- ( ph -> prod_ k e. { A , B } D = ( prod_ k e. { A } D x. prod_ k e. { B } D ) )
25	1	prodsn	|- ( ( A e. V /\ E e. CC ) -> prod_ k e. { A } D = E )
26	3 5 25	syl2anc	|- ( ph -> prod_ k e. { A } D = E )
27	2	prodsn	|- ( ( B e. W /\ F e. CC ) -> prod_ k e. { B } D = F )
28	4 6 27	syl2anc	|- ( ph -> prod_ k e. { B } D = F )
29	26 28	oveq12d	|- ( ph -> ( prod_ k e. { A } D x. prod_ k e. { B } D ) = ( E x. F ) )
30	24 29	eqtrd	|- ( ph -> prod_ k e. { A , B } D = ( E x. F ) )