Metamath Proof Explorer

Theorem fprodconst

Description: The product of constant terms ( k is not free in B ). (Contributed by Scott Fenton, 12-Jan-2018)

Ref Expression
Assertion fprodconst 
|- ( ( A e. Fin /\ B e. CC ) -> prod_ k e. A B = ( B ^ ( # ` A ) ) )

Proof

Step Hyp Ref Expression
1 exp0 
 |-  ( B e. CC -> ( B ^ 0 ) = 1 )
2 1 eqcomd 
 |-  ( B e. CC -> 1 = ( B ^ 0 ) )
3 prodeq1 
 |-  ( A = (/) -> prod_ k e. A B = prod_ k e. (/) B )
4 prod0 
 |-  prod_ k e. (/) B = 1
5 3 4 eqtrdi 
 |-  ( A = (/) -> prod_ k e. A B = 1 )
6 fveq2 
 |-  ( A = (/) -> ( # ` A ) = ( # ` (/) ) )
7 hash0 
 |-  ( # ` (/) ) = 0
8 6 7 eqtrdi 
 |-  ( A = (/) -> ( # ` A ) = 0 )
9 8 oveq2d 
 |-  ( A = (/) -> ( B ^ ( # ` A ) ) = ( B ^ 0 ) )
10 5 9 eqeq12d 
 |-  ( A = (/) -> ( prod_ k e. A B = ( B ^ ( # ` A ) ) <-> 1 = ( B ^ 0 ) ) )
11 2 10 syl5ibrcom 
 |-  ( B e. CC -> ( A = (/) -> prod_ k e. A B = ( B ^ ( # ` A ) ) ) )
12 11 adantl 
 |-  ( ( A e. Fin /\ B e. CC ) -> ( A = (/) -> prod_ k e. A B = ( B ^ ( # ` A ) ) ) )
13 eqidd 
 |-  ( k = ( f ` n ) -> B = B )
14 simprl 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN )
15 simprr 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
16 simpllr 
 |-  ( ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ k e. A ) -> B e. CC )
17 simpllr 
 |-  ( ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> B e. CC )
18 elfznn 
 |-  ( n e. ( 1 ... ( # ` A ) ) -> n e. NN )
19 18 adantl 
 |-  ( ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> n e. NN )
20 fvconst2g 
 |-  ( ( B e. CC /\ n e. NN ) -> ( ( NN X. { B } ) ` n ) = B )
21 17 19 20 syl2anc 
 |-  ( ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( NN X. { B } ) ` n ) = B )
22 13 14 15 16 21 fprod 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A B = ( seq 1 ( x. , ( NN X. { B } ) ) ` ( # ` A ) ) )
23 expnnval 
 |-  ( ( B e. CC /\ ( # ` A ) e. NN ) -> ( B ^ ( # ` A ) ) = ( seq 1 ( x. , ( NN X. { B } ) ) ` ( # ` A ) ) )
24 23 ad2ant2lr 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( B ^ ( # ` A ) ) = ( seq 1 ( x. , ( NN X. { B } ) ) ` ( # ` A ) ) )
25 22 24 eqtr4d 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A B = ( B ^ ( # ` A ) ) )
26 25 expr 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A B = ( B ^ ( # ` A ) ) ) )
27 26 exlimdv 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A B = ( B ^ ( # ` A ) ) ) )
28 27 expimpd 
 |-  ( ( A e. Fin /\ B e. CC ) -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> prod_ k e. A B = ( B ^ ( # ` A ) ) ) )
29 fz1f1o 
 |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
30 29 adantr 
 |-  ( ( A e. Fin /\ B e. CC ) -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
31 12 28 30 mpjaod 
 |-  ( ( A e. Fin /\ B e. CC ) -> prod_ k e. A B = ( B ^ ( # ` A ) ) )