Theorem fprodcom

Description: Interchange product order. (Contributed by Scott Fenton, 2-Feb-2018)

	Ref	Expression
Hypotheses	fprodcom.1	|- ( ph -> A e. Fin )
	fprodcom.2	|- ( ph -> B e. Fin )
	fprodcom.3	|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
Assertion	fprodcom	|- ( ph -> prod_ j e. A prod_ k e. B C = prod_ k e. B prod_ j e. A C )

Proof

Step	Hyp	Ref	Expression
1		fprodcom.1	|- ( ph -> A e. Fin )
2		fprodcom.2	|- ( ph -> B e. Fin )
3		fprodcom.3	|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
4	2	adantr	|- ( ( ph /\ j e. A ) -> B e. Fin )
5		ancom	|- ( ( j e. A /\ k e. B ) <-> ( k e. B /\ j e. A ) )
6	5	a1i	|- ( ph -> ( ( j e. A /\ k e. B ) <-> ( k e. B /\ j e. A ) ) )
7	1 2 4 6 3	fprodcom2	|- ( ph -> prod_ j e. A prod_ k e. B C = prod_ k e. B prod_ j e. A C )