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