Metamath Proof Explorer

Theorem fprodexp

Description: Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodexp.kph 
|- F/ k ph
fprodexp.n 
|- ( ph -> N e. NN0 )
fprodexp.a 
|- ( ph -> A e. Fin )
fprodexp.b 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fprodexp 
|- ( ph -> prod_ k e. A ( B ^ N ) = ( prod_ k e. A B ^ N ) )

Proof

Step Hyp Ref Expression
1 fprodexp.kph 
 |-  F/ k ph
2 fprodexp.n 
 |-  ( ph -> N e. NN0 )
3 fprodexp.a 
 |-  ( ph -> A e. Fin )
4 fprodexp.b 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
5 prodeq1 
 |-  ( x = (/) -> prod_ k e. x ( B ^ N ) = prod_ k e. (/) ( B ^ N ) )
6 prodeq1 
 |-  ( x = (/) -> prod_ k e. x B = prod_ k e. (/) B )
7 6 oveq1d 
 |-  ( x = (/) -> ( prod_ k e. x B ^ N ) = ( prod_ k e. (/) B ^ N ) )
8 5 7 eqeq12d 
 |-  ( x = (/) -> ( prod_ k e. x ( B ^ N ) = ( prod_ k e. x B ^ N ) <-> prod_ k e. (/) ( B ^ N ) = ( prod_ k e. (/) B ^ N ) ) )
9 prodeq1 
 |-  ( x = y -> prod_ k e. x ( B ^ N ) = prod_ k e. y ( B ^ N ) )
10 prodeq1 
 |-  ( x = y -> prod_ k e. x B = prod_ k e. y B )
11 10 oveq1d 
 |-  ( x = y -> ( prod_ k e. x B ^ N ) = ( prod_ k e. y B ^ N ) )
12 9 11 eqeq12d 
 |-  ( x = y -> ( prod_ k e. x ( B ^ N ) = ( prod_ k e. x B ^ N ) <-> prod_ k e. y ( B ^ N ) = ( prod_ k e. y B ^ N ) ) )
13 prodeq1 
 |-  ( x = ( y u. { z } ) -> prod_ k e. x ( B ^ N ) = prod_ k e. ( y u. { z } ) ( B ^ N ) )
14 prodeq1 
 |-  ( x = ( y u. { z } ) -> prod_ k e. x B = prod_ k e. ( y u. { z } ) B )
15 14 oveq1d 
 |-  ( x = ( y u. { z } ) -> ( prod_ k e. x B ^ N ) = ( prod_ k e. ( y u. { z } ) B ^ N ) )
16 13 15 eqeq12d 
 |-  ( x = ( y u. { z } ) -> ( prod_ k e. x ( B ^ N ) = ( prod_ k e. x B ^ N ) <-> prod_ k e. ( y u. { z } ) ( B ^ N ) = ( prod_ k e. ( y u. { z } ) B ^ N ) ) )
17 prodeq1 
 |-  ( x = A -> prod_ k e. x ( B ^ N ) = prod_ k e. A ( B ^ N ) )
18 prodeq1 
 |-  ( x = A -> prod_ k e. x B = prod_ k e. A B )
19 18 oveq1d 
 |-  ( x = A -> ( prod_ k e. x B ^ N ) = ( prod_ k e. A B ^ N ) )
20 17 19 eqeq12d 
 |-  ( x = A -> ( prod_ k e. x ( B ^ N ) = ( prod_ k e. x B ^ N ) <-> prod_ k e. A ( B ^ N ) = ( prod_ k e. A B ^ N ) ) )
21 2 nn0zd 
 |-  ( ph -> N e. ZZ )
22 1exp 
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )
23 21 22 syl 
 |-  ( ph -> ( 1 ^ N ) = 1 )
24 23 eqcomd 
 |-  ( ph -> 1 = ( 1 ^ N ) )
25 prod0 
 |-  prod_ k e. (/) ( B ^ N ) = 1
26 25 a1i 
 |-  ( ph -> prod_ k e. (/) ( B ^ N ) = 1 )
27 prod0 
 |-  prod_ k e. (/) B = 1
28 27 oveq1i 
 |-  ( prod_ k e. (/) B ^ N ) = ( 1 ^ N )
29 28 a1i 
 |-  ( ph -> ( prod_ k e. (/) B ^ N ) = ( 1 ^ N ) )
30 24 26 29 3eqtr4d 
 |-  ( ph -> prod_ k e. (/) ( B ^ N ) = ( prod_ k e. (/) B ^ N ) )
31 nfv 
 |-  F/ k ( y C_ A /\ z e. ( A \ y ) )
32 1 31 nfan 
 |-  F/ k ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) )
33 3 adantr 
 |-  ( ( ph /\ y C_ A ) -> A e. Fin )
34 simpr 
 |-  ( ( ph /\ y C_ A ) -> y C_ A )
35 ssfi 
 |-  ( ( A e. Fin /\ y C_ A ) -> y e. Fin )
36 33 34 35 syl2anc 
 |-  ( ( ph /\ y C_ A ) -> y e. Fin )
37 36 adantrr 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> y e. Fin )
38 simpll 
 |-  ( ( ( ph /\ y C_ A ) /\ k e. y ) -> ph )
39 34 sselda 
 |-  ( ( ( ph /\ y C_ A ) /\ k e. y ) -> k e. A )
40 38 39 4 syl2anc 
 |-  ( ( ( ph /\ y C_ A ) /\ k e. y ) -> B e. CC )
41 40 adantlrr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> B e. CC )
42 32 37 41 fprodclf 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> prod_ k e. y B e. CC )
43 simpl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ph )
44 simprr 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. ( A \ y ) )
45 44 eldifad 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. A )
46 nfv 
 |-  F/ k z e. A
47 1 46 nfan 
 |-  F/ k ( ph /\ z e. A )
48 nfcsb1v 
 |-  F/_ k [_ z / k ]_ B
49 48 nfel1 
 |-  F/ k [_ z / k ]_ B e. CC
50 47 49 nfim 
 |-  F/ k ( ( ph /\ z e. A ) -> [_ z / k ]_ B e. CC )
51 eleq1w 
 |-  ( k = z -> ( k e. A <-> z e. A ) )
52 51 anbi2d 
 |-  ( k = z -> ( ( ph /\ k e. A ) <-> ( ph /\ z e. A ) ) )
53 csbeq1a 
 |-  ( k = z -> B = [_ z / k ]_ B )
54 53 eleq1d 
 |-  ( k = z -> ( B e. CC <-> [_ z / k ]_ B e. CC ) )
55 52 54 imbi12d 
 |-  ( k = z -> ( ( ( ph /\ k e. A ) -> B e. CC ) <-> ( ( ph /\ z e. A ) -> [_ z / k ]_ B e. CC ) ) )
56 50 55 4 chvarfv 
 |-  ( ( ph /\ z e. A ) -> [_ z / k ]_ B e. CC )
57 43 45 56 syl2anc 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> [_ z / k ]_ B e. CC )
58 2 adantr 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> N e. NN0 )
59 mulexp 
 |-  ( ( prod_ k e. y B e. CC /\ [_ z / k ]_ B e. CC /\ N e. NN0 ) -> ( ( prod_ k e. y B x. [_ z / k ]_ B ) ^ N ) = ( ( prod_ k e. y B ^ N ) x. ( [_ z / k ]_ B ^ N ) ) )
60 42 57 58 59 syl3anc 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( prod_ k e. y B x. [_ z / k ]_ B ) ^ N ) = ( ( prod_ k e. y B ^ N ) x. ( [_ z / k ]_ B ^ N ) ) )
61 60 eqcomd 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( prod_ k e. y B ^ N ) x. ( [_ z / k ]_ B ^ N ) ) = ( ( prod_ k e. y B x. [_ z / k ]_ B ) ^ N ) )
62 61 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ prod_ k e. y ( B ^ N ) = ( prod_ k e. y B ^ N ) ) -> ( ( prod_ k e. y B ^ N ) x. ( [_ z / k ]_ B ^ N ) ) = ( ( prod_ k e. y B x. [_ z / k ]_ B ) ^ N ) )
63 nfcv 
 |-  F/_ k ^
64 nfcv 
 |-  F/_ k N
65 48 63 64 nfov 
 |-  F/_ k ( [_ z / k ]_ B ^ N )
66 44 eldifbd 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> -. z e. y )
67 2 ad2antrr 
 |-  ( ( ( ph /\ y C_ A ) /\ k e. y ) -> N e. NN0 )
68 40 67 expcld 
 |-  ( ( ( ph /\ y C_ A ) /\ k e. y ) -> ( B ^ N ) e. CC )
69 68 adantlrr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> ( B ^ N ) e. CC )
70 53 oveq1d 
 |-  ( k = z -> ( B ^ N ) = ( [_ z / k ]_ B ^ N ) )
71 57 58 expcld 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( [_ z / k ]_ B ^ N ) e. CC )
72 32 65 37 44 66 69 70 71 fprodsplitsn 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> prod_ k e. ( y u. { z } ) ( B ^ N ) = ( prod_ k e. y ( B ^ N ) x. ( [_ z / k ]_ B ^ N ) ) )
73 72 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ prod_ k e. y ( B ^ N ) = ( prod_ k e. y B ^ N ) ) -> prod_ k e. ( y u. { z } ) ( B ^ N ) = ( prod_ k e. y ( B ^ N ) x. ( [_ z / k ]_ B ^ N ) ) )
74 oveq1 
 |-  ( prod_ k e. y ( B ^ N ) = ( prod_ k e. y B ^ N ) -> ( prod_ k e. y ( B ^ N ) x. ( [_ z / k ]_ B ^ N ) ) = ( ( prod_ k e. y B ^ N ) x. ( [_ z / k ]_ B ^ N ) ) )
75 74 adantl 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ prod_ k e. y ( B ^ N ) = ( prod_ k e. y B ^ N ) ) -> ( prod_ k e. y ( B ^ N ) x. ( [_ z / k ]_ B ^ N ) ) = ( ( prod_ k e. y B ^ N ) x. ( [_ z / k ]_ B ^ N ) ) )
76 73 75 eqtrd 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ prod_ k e. y ( B ^ N ) = ( prod_ k e. y B ^ N ) ) -> prod_ k e. ( y u. { z } ) ( B ^ N ) = ( ( prod_ k e. y B ^ N ) x. ( [_ z / k ]_ B ^ N ) ) )
77 32 48 37 44 66 41 53 57 fprodsplitsn 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> prod_ k e. ( y u. { z } ) B = ( prod_ k e. y B x. [_ z / k ]_ B ) )
78 77 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ prod_ k e. y ( B ^ N ) = ( prod_ k e. y B ^ N ) ) -> prod_ k e. ( y u. { z } ) B = ( prod_ k e. y B x. [_ z / k ]_ B ) )
79 78 oveq1d 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ prod_ k e. y ( B ^ N ) = ( prod_ k e. y B ^ N ) ) -> ( prod_ k e. ( y u. { z } ) B ^ N ) = ( ( prod_ k e. y B x. [_ z / k ]_ B ) ^ N ) )
80 62 76 79 3eqtr4d 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ prod_ k e. y ( B ^ N ) = ( prod_ k e. y B ^ N ) ) -> prod_ k e. ( y u. { z } ) ( B ^ N ) = ( prod_ k e. ( y u. { z } ) B ^ N ) )
81 80 ex 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( prod_ k e. y ( B ^ N ) = ( prod_ k e. y B ^ N ) -> prod_ k e. ( y u. { z } ) ( B ^ N ) = ( prod_ k e. ( y u. { z } ) B ^ N ) ) )
82 8 12 16 20 30 81 3 findcard2d 
 |-  ( ph -> prod_ k e. A ( B ^ N ) = ( prod_ k e. A B ^ N ) )