Metamath Proof Explorer

Theorem fproddiv

Description: The quotient of two finite products. (Contributed by Scott Fenton, 15-Jan-2018)

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