Metamath Proof Explorer


Theorem fprodmul

Description: The product of two finite products. (Contributed by Scott Fenton, 14-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 fprodmul.1
 |-  ( ph -> A e. Fin )
2 fprodmul.2
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 fprodmul.3
 |-  ( ( ph /\ k e. A ) -> C e. CC )
4 1t1e1
 |-  ( 1 x. 1 ) = 1
5 prod0
 |-  prod_ k e. (/) B = 1
6 prod0
 |-  prod_ k e. (/) C = 1
7 5 6 oveq12i
 |-  ( prod_ k e. (/) B x. prod_ k e. (/) C ) = ( 1 x. 1 )
8 prod0
 |-  prod_ k e. (/) ( B x. C ) = 1
9 4 7 8 3eqtr4ri
 |-  prod_ k e. (/) ( B x. C ) = ( prod_ k e. (/) B x. prod_ k e. (/) C )
10 prodeq1
 |-  ( A = (/) -> prod_ k e. A ( B x. C ) = prod_ k e. (/) ( B x. C ) )
11 prodeq1
 |-  ( A = (/) -> prod_ k e. A B = prod_ k e. (/) B )
12 prodeq1
 |-  ( A = (/) -> prod_ k e. A C = prod_ k e. (/) C )
13 11 12 oveq12d
 |-  ( A = (/) -> ( prod_ k e. A B x. prod_ k e. A C ) = ( prod_ k e. (/) B x. prod_ k e. (/) C ) )
14 9 10 13 3eqtr4a
 |-  ( A = (/) -> prod_ k e. A ( B x. C ) = ( prod_ k e. A B x. prod_ k e. A C ) )
15 14 a1i
 |-  ( ph -> ( A = (/) -> prod_ k e. A ( B x. C ) = ( prod_ k e. A B x. prod_ k e. A C ) ) )
16 simprl
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN )
17 nnuz
 |-  NN = ( ZZ>= ` 1 )
18 16 17 eleqtrdi
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. ( ZZ>= ` 1 ) )
19 2 fmpttd
 |-  ( ph -> ( k e. A |-> B ) : A --> CC )
20 19 adantr
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> B ) : A --> CC )
21 f1of
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) --> A )
22 21 ad2antll
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) --> A )
23 fco
 |-  ( ( ( k e. A |-> B ) : A --> CC /\ f : ( 1 ... ( # ` A ) ) --> A ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> CC )
24 20 22 23 syl2anc
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> CC )
25 24 ffvelrnda
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` n ) e. CC )
26 3 fmpttd
 |-  ( ph -> ( k e. A |-> C ) : A --> CC )
27 26 adantr
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> C ) : A --> CC )
28 fco
 |-  ( ( ( k e. A |-> C ) : A --> CC /\ f : ( 1 ... ( # ` A ) ) --> A ) -> ( ( k e. A |-> C ) o. f ) : ( 1 ... ( # ` A ) ) --> CC )
29 27 22 28 syl2anc
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> C ) o. f ) : ( 1 ... ( # ` A ) ) --> CC )
30 29 ffvelrnda
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> C ) o. f ) ` n ) e. CC )
31 22 ffvelrnda
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( f ` n ) e. A )
32 simpr
 |-  ( ( ph /\ k e. A ) -> k e. A )
33 2 3 mulcld
 |-  ( ( ph /\ k e. A ) -> ( B x. C ) e. CC )
34 eqid
 |-  ( k e. A |-> ( B x. C ) ) = ( k e. A |-> ( B x. C ) )
35 34 fvmpt2
 |-  ( ( k e. A /\ ( B x. C ) e. CC ) -> ( ( k e. A |-> ( B x. C ) ) ` k ) = ( B x. C ) )
36 32 33 35 syl2anc
 |-  ( ( ph /\ k e. A ) -> ( ( k e. A |-> ( B x. C ) ) ` k ) = ( B x. C ) )
37 eqid
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
38 37 fvmpt2
 |-  ( ( k e. A /\ B e. CC ) -> ( ( k e. A |-> B ) ` k ) = B )
39 32 2 38 syl2anc
 |-  ( ( ph /\ k e. A ) -> ( ( k e. A |-> B ) ` k ) = B )
40 eqid
 |-  ( k e. A |-> C ) = ( k e. A |-> C )
41 40 fvmpt2
 |-  ( ( k e. A /\ C e. CC ) -> ( ( k e. A |-> C ) ` k ) = C )
42 32 3 41 syl2anc
 |-  ( ( ph /\ k e. A ) -> ( ( k e. A |-> C ) ` k ) = C )
43 39 42 oveq12d
 |-  ( ( ph /\ k e. A ) -> ( ( ( k e. A |-> B ) ` k ) x. ( ( k e. A |-> C ) ` k ) ) = ( B x. C ) )
44 36 43 eqtr4d
 |-  ( ( ph /\ k e. A ) -> ( ( k e. A |-> ( B x. C ) ) ` k ) = ( ( ( k e. A |-> B ) ` k ) x. ( ( k e. A |-> C ) ` k ) ) )
45 44 ralrimiva
 |-  ( ph -> A. k e. A ( ( k e. A |-> ( B x. C ) ) ` k ) = ( ( ( k e. A |-> B ) ` k ) x. ( ( k e. A |-> C ) ` k ) ) )
46 45 ad2antrr
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> A. k e. A ( ( k e. A |-> ( B x. C ) ) ` k ) = ( ( ( k e. A |-> B ) ` k ) x. ( ( k e. A |-> C ) ` k ) ) )
47 nffvmpt1
 |-  F/_ k ( ( k e. A |-> ( B x. C ) ) ` ( f ` n ) )
48 nffvmpt1
 |-  F/_ k ( ( k e. A |-> B ) ` ( f ` n ) )
49 nfcv
 |-  F/_ k x.
50 nffvmpt1
 |-  F/_ k ( ( k e. A |-> C ) ` ( f ` n ) )
51 48 49 50 nfov
 |-  F/_ k ( ( ( k e. A |-> B ) ` ( f ` n ) ) x. ( ( k e. A |-> C ) ` ( f ` n ) ) )
52 47 51 nfeq
 |-  F/ k ( ( k e. A |-> ( B x. C ) ) ` ( f ` n ) ) = ( ( ( k e. A |-> B ) ` ( f ` n ) ) x. ( ( k e. A |-> C ) ` ( f ` n ) ) )
53 fveq2
 |-  ( k = ( f ` n ) -> ( ( k e. A |-> ( B x. C ) ) ` k ) = ( ( k e. A |-> ( B x. C ) ) ` ( f ` n ) ) )
54 fveq2
 |-  ( k = ( f ` n ) -> ( ( k e. A |-> B ) ` k ) = ( ( k e. A |-> B ) ` ( f ` n ) ) )
55 fveq2
 |-  ( k = ( f ` n ) -> ( ( k e. A |-> C ) ` k ) = ( ( k e. A |-> C ) ` ( f ` n ) ) )
56 54 55 oveq12d
 |-  ( k = ( f ` n ) -> ( ( ( k e. A |-> B ) ` k ) x. ( ( k e. A |-> C ) ` k ) ) = ( ( ( k e. A |-> B ) ` ( f ` n ) ) x. ( ( k e. A |-> C ) ` ( f ` n ) ) ) )
57 53 56 eqeq12d
 |-  ( k = ( f ` n ) -> ( ( ( k e. A |-> ( B x. C ) ) ` k ) = ( ( ( k e. A |-> B ) ` k ) x. ( ( k e. A |-> C ) ` k ) ) <-> ( ( k e. A |-> ( B x. C ) ) ` ( f ` n ) ) = ( ( ( k e. A |-> B ) ` ( f ` n ) ) x. ( ( k e. A |-> C ) ` ( f ` n ) ) ) ) )
58 52 57 rspc
 |-  ( ( f ` n ) e. A -> ( A. k e. A ( ( k e. A |-> ( B x. C ) ) ` k ) = ( ( ( k e. A |-> B ) ` k ) x. ( ( k e. A |-> C ) ` k ) ) -> ( ( k e. A |-> ( B x. C ) ) ` ( f ` n ) ) = ( ( ( k e. A |-> B ) ` ( f ` n ) ) x. ( ( k e. A |-> C ) ` ( f ` n ) ) ) ) )
59 31 46 58 sylc
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( k e. A |-> ( B x. C ) ) ` ( f ` n ) ) = ( ( ( k e. A |-> B ) ` ( f ` n ) ) x. ( ( k e. A |-> C ) ` ( f ` n ) ) ) )
60 fvco3
 |-  ( ( f : ( 1 ... ( # ` A ) ) --> A /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> ( B x. C ) ) o. f ) ` n ) = ( ( k e. A |-> ( B x. C ) ) ` ( f ` n ) ) )
61 22 60 sylan
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> ( B x. C ) ) o. f ) ` n ) = ( ( k e. A |-> ( B x. C ) ) ` ( f ` n ) ) )
62 fvco3
 |-  ( ( f : ( 1 ... ( # ` A ) ) --> A /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` n ) = ( ( k e. A |-> B ) ` ( f ` n ) ) )
63 22 62 sylan
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` n ) = ( ( k e. A |-> B ) ` ( f ` n ) ) )
64 fvco3
 |-  ( ( f : ( 1 ... ( # ` A ) ) --> A /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> C ) o. f ) ` n ) = ( ( k e. A |-> C ) ` ( f ` n ) ) )
65 22 64 sylan
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> C ) o. f ) ` n ) = ( ( k e. A |-> C ) ` ( f ` n ) ) )
66 63 65 oveq12d
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( ( k e. A |-> B ) o. f ) ` n ) x. ( ( ( k e. A |-> C ) o. f ) ` n ) ) = ( ( ( k e. A |-> B ) ` ( f ` n ) ) x. ( ( k e. A |-> C ) ` ( f ` n ) ) ) )
67 59 61 66 3eqtr4d
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> ( B x. C ) ) o. f ) ` n ) = ( ( ( ( k e. A |-> B ) o. f ) ` n ) x. ( ( ( k e. A |-> C ) o. f ) ` n ) ) )
68 18 25 30 67 prodfmul
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( seq 1 ( x. , ( ( k e. A |-> ( B x. C ) ) o. f ) ) ` ( # ` A ) ) = ( ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) x. ( seq 1 ( x. , ( ( k e. A |-> C ) o. f ) ) ` ( # ` A ) ) ) )
69 fveq2
 |-  ( m = ( f ` n ) -> ( ( k e. A |-> ( B x. C ) ) ` m ) = ( ( k e. A |-> ( B x. C ) ) ` ( f ` n ) ) )
70 simprr
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
71 33 fmpttd
 |-  ( ph -> ( k e. A |-> ( B x. C ) ) : A --> CC )
72 71 adantr
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> ( B x. C ) ) : A --> CC )
73 72 ffvelrnda
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> ( B x. C ) ) ` m ) e. CC )
74 69 16 70 73 61 fprod
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ m e. A ( ( k e. A |-> ( B x. C ) ) ` m ) = ( seq 1 ( x. , ( ( k e. A |-> ( B x. C ) ) o. f ) ) ` ( # ` A ) ) )
75 fveq2
 |-  ( m = ( f ` n ) -> ( ( k e. A |-> B ) ` m ) = ( ( k e. A |-> B ) ` ( f ` n ) ) )
76 20 ffvelrnda
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> B ) ` m ) e. CC )
77 75 16 70 76 63 fprod
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ m e. A ( ( k e. A |-> B ) ` m ) = ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) )
78 fveq2
 |-  ( m = ( f ` n ) -> ( ( k e. A |-> C ) ` m ) = ( ( k e. A |-> C ) ` ( f ` n ) ) )
79 27 ffvelrnda
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> C ) ` m ) e. CC )
80 78 16 70 79 65 fprod
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ m e. A ( ( k e. A |-> C ) ` m ) = ( seq 1 ( x. , ( ( k e. A |-> C ) o. f ) ) ` ( # ` A ) ) )
81 77 80 oveq12d
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( prod_ m e. A ( ( k e. A |-> B ) ` m ) x. prod_ m e. A ( ( k e. A |-> C ) ` m ) ) = ( ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) x. ( seq 1 ( x. , ( ( k e. A |-> C ) o. f ) ) ` ( # ` A ) ) ) )
82 68 74 81 3eqtr4d
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ m e. A ( ( k e. A |-> ( B x. C ) ) ` m ) = ( prod_ m e. A ( ( k e. A |-> B ) ` m ) x. prod_ m e. A ( ( k e. A |-> C ) ` m ) ) )
83 prodfc
 |-  prod_ m e. A ( ( k e. A |-> ( B x. C ) ) ` m ) = prod_ k e. A ( B x. C )
84 prodfc
 |-  prod_ m e. A ( ( k e. A |-> B ) ` m ) = prod_ k e. A B
85 prodfc
 |-  prod_ m e. A ( ( k e. A |-> C ) ` m ) = prod_ k e. A C
86 84 85 oveq12i
 |-  ( prod_ m e. A ( ( k e. A |-> B ) ` m ) x. prod_ m e. A ( ( k e. A |-> C ) ` m ) ) = ( prod_ k e. A B x. prod_ k e. A C )
87 82 83 86 3eqtr3g
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A ( B x. C ) = ( prod_ k e. A B x. prod_ k e. A C ) )
88 87 expr
 |-  ( ( ph /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A ( B x. C ) = ( prod_ k e. A B x. prod_ k e. A C ) ) )
89 88 exlimdv
 |-  ( ( ph /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A ( B x. C ) = ( prod_ k e. A B x. prod_ k e. A C ) ) )
90 89 expimpd
 |-  ( ph -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> prod_ k e. A ( B x. C ) = ( prod_ k e. A B x. prod_ k e. A C ) ) )
91 fz1f1o
 |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
92 1 91 syl
 |-  ( ph -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
93 15 90 92 mpjaod
 |-  ( ph -> prod_ k e. A ( B x. C ) = ( prod_ k e. A B x. prod_ k e. A C ) )