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 ) )