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