Metamath Proof Explorer

Theorem fprodabs2

Description: The absolute value of a finite product . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodabs2.a 
|- ( ph -> A e. Fin )
fprodabs2.b 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fprodabs2 
|- ( ph -> ( abs ` prod_ k e. A B ) = prod_ k e. A ( abs ` B ) )

Proof

Step Hyp Ref Expression
1 fprodabs2.a 
 |-  ( ph -> A e. Fin )
2 fprodabs2.b 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 prodeq1 
 |-  ( x = (/) -> prod_ k e. x B = prod_ k e. (/) B )
4 3 fveq2d 
 |-  ( x = (/) -> ( abs ` prod_ k e. x B ) = ( abs ` prod_ k e. (/) B ) )
5 prodeq1 
 |-  ( x = (/) -> prod_ k e. x ( abs ` B ) = prod_ k e. (/) ( abs ` B ) )
6 4 5 eqeq12d 
 |-  ( x = (/) -> ( ( abs ` prod_ k e. x B ) = prod_ k e. x ( abs ` B ) <-> ( abs ` prod_ k e. (/) B ) = prod_ k e. (/) ( abs ` B ) ) )
7 prodeq1 
 |-  ( x = y -> prod_ k e. x B = prod_ k e. y B )
8 7 fveq2d 
 |-  ( x = y -> ( abs ` prod_ k e. x B ) = ( abs ` prod_ k e. y B ) )
9 prodeq1 
 |-  ( x = y -> prod_ k e. x ( abs ` B ) = prod_ k e. y ( abs ` B ) )
10 8 9 eqeq12d 
 |-  ( x = y -> ( ( abs ` prod_ k e. x B ) = prod_ k e. x ( abs ` B ) <-> ( abs ` prod_ k e. y B ) = prod_ k e. y ( abs ` B ) ) )
11 prodeq1 
 |-  ( x = ( y u. { z } ) -> prod_ k e. x B = prod_ k e. ( y u. { z } ) B )
12 11 fveq2d 
 |-  ( x = ( y u. { z } ) -> ( abs ` prod_ k e. x B ) = ( abs ` prod_ k e. ( y u. { z } ) B ) )
13 prodeq1 
 |-  ( x = ( y u. { z } ) -> prod_ k e. x ( abs ` B ) = prod_ k e. ( y u. { z } ) ( abs ` B ) )
14 12 13 eqeq12d 
 |-  ( x = ( y u. { z } ) -> ( ( abs ` prod_ k e. x B ) = prod_ k e. x ( abs ` B ) <-> ( abs ` prod_ k e. ( y u. { z } ) B ) = prod_ k e. ( y u. { z } ) ( abs ` B ) ) )
15 prodeq1 
 |-  ( x = A -> prod_ k e. x B = prod_ k e. A B )
16 15 fveq2d 
 |-  ( x = A -> ( abs ` prod_ k e. x B ) = ( abs ` prod_ k e. A B ) )
17 prodeq1 
 |-  ( x = A -> prod_ k e. x ( abs ` B ) = prod_ k e. A ( abs ` B ) )
18 16 17 eqeq12d 
 |-  ( x = A -> ( ( abs ` prod_ k e. x B ) = prod_ k e. x ( abs ` B ) <-> ( abs ` prod_ k e. A B ) = prod_ k e. A ( abs ` B ) ) )
19 abs1 
 |-  ( abs ` 1 ) = 1
20 prod0 
 |-  prod_ k e. (/) B = 1
21 20 fveq2i 
 |-  ( abs ` prod_ k e. (/) B ) = ( abs ` 1 )
22 prod0 
 |-  prod_ k e. (/) ( abs ` B ) = 1
23 19 21 22 3eqtr4i 
 |-  ( abs ` prod_ k e. (/) B ) = prod_ k e. (/) ( abs ` B )
24 23 a1i 
 |-  ( ph -> ( abs ` prod_ k e. (/) B ) = prod_ k e. (/) ( abs ` B ) )
25 eqidd 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( abs ` prod_ k e. y B ) = prod_ k e. y ( abs ` B ) ) -> ( prod_ k e. y ( abs ` B ) x. ( abs ` [_ z / k ]_ B ) ) = ( prod_ k e. y ( abs ` B ) x. ( abs ` [_ z / k ]_ B ) ) )
26 nfv 
 |-  F/ k ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) )
27 nfcsb1v 
 |-  F/_ k [_ z / k ]_ B
28 1 adantr 
 |-  ( ( ph /\ y C_ A ) -> A e. Fin )
29 simpr 
 |-  ( ( ph /\ y C_ A ) -> y C_ A )
30 ssfi 
 |-  ( ( A e. Fin /\ y C_ A ) -> y e. Fin )
31 28 29 30 syl2anc 
 |-  ( ( ph /\ y C_ A ) -> y e. Fin )
32 31 adantrr 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> y e. Fin )
33 simprr 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. ( A \ y ) )
34 33 eldifbd 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> -. z e. y )
35 simpll 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> ph )
36 29 sselda 
 |-  ( ( ( ph /\ y C_ A ) /\ k e. y ) -> k e. A )
37 36 adantlrr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> k e. A )
38 35 37 2 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> B e. CC )
39 csbeq1a 
 |-  ( k = z -> B = [_ z / k ]_ B )
40 simpl 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ph )
41 33 eldifad 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> z e. A )
42 nfv 
 |-  F/ k ( ph /\ z e. A )
43 27 nfel1 
 |-  F/ k [_ z / k ]_ B e. CC
44 42 43 nfim 
 |-  F/ k ( ( ph /\ z e. A ) -> [_ z / k ]_ B e. CC )
45 eleq1w 
 |-  ( k = z -> ( k e. A <-> z e. A ) )
46 45 anbi2d 
 |-  ( k = z -> ( ( ph /\ k e. A ) <-> ( ph /\ z e. A ) ) )
47 39 eleq1d 
 |-  ( k = z -> ( B e. CC <-> [_ z / k ]_ B e. CC ) )
48 46 47 imbi12d 
 |-  ( k = z -> ( ( ( ph /\ k e. A ) -> B e. CC ) <-> ( ( ph /\ z e. A ) -> [_ z / k ]_ B e. CC ) ) )
49 44 48 2 chvarfv 
 |-  ( ( ph /\ z e. A ) -> [_ z / k ]_ B e. CC )
50 40 41 49 syl2anc 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> [_ z / k ]_ B e. CC )
51 26 27 32 33 34 38 39 50 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 ) )
52 51 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( abs ` prod_ k e. y B ) = prod_ k e. y ( abs ` B ) ) -> prod_ k e. ( y u. { z } ) B = ( prod_ k e. y B x. [_ z / k ]_ B ) )
53 52 fveq2d 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( abs ` prod_ k e. y B ) = prod_ k e. y ( abs ` B ) ) -> ( abs ` prod_ k e. ( y u. { z } ) B ) = ( abs ` ( prod_ k e. y B x. [_ z / k ]_ B ) ) )
54 26 32 38 fprodclf 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> prod_ k e. y B e. CC )
55 54 50 absmuld 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( abs ` ( prod_ k e. y B x. [_ z / k ]_ B ) ) = ( ( abs ` prod_ k e. y B ) x. ( abs ` [_ z / k ]_ B ) ) )
56 55 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( abs ` prod_ k e. y B ) = prod_ k e. y ( abs ` B ) ) -> ( abs ` ( prod_ k e. y B x. [_ z / k ]_ B ) ) = ( ( abs ` prod_ k e. y B ) x. ( abs ` [_ z / k ]_ B ) ) )
57 oveq1 
 |-  ( ( abs ` prod_ k e. y B ) = prod_ k e. y ( abs ` B ) -> ( ( abs ` prod_ k e. y B ) x. ( abs ` [_ z / k ]_ B ) ) = ( prod_ k e. y ( abs ` B ) x. ( abs ` [_ z / k ]_ B ) ) )
58 57 adantl 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( abs ` prod_ k e. y B ) = prod_ k e. y ( abs ` B ) ) -> ( ( abs ` prod_ k e. y B ) x. ( abs ` [_ z / k ]_ B ) ) = ( prod_ k e. y ( abs ` B ) x. ( abs ` [_ z / k ]_ B ) ) )
59 53 56 58 3eqtrd 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( abs ` prod_ k e. y B ) = prod_ k e. y ( abs ` B ) ) -> ( abs ` prod_ k e. ( y u. { z } ) B ) = ( prod_ k e. y ( abs ` B ) x. ( abs ` [_ z / k ]_ B ) ) )
60 nfcv 
 |-  F/_ k abs
61 60 27 nffv 
 |-  F/_ k ( abs ` [_ z / k ]_ B )
62 38 abscld 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> ( abs ` B ) e. RR )
63 62 recnd 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ k e. y ) -> ( abs ` B ) e. CC )
64 39 fveq2d 
 |-  ( k = z -> ( abs ` B ) = ( abs ` [_ z / k ]_ B ) )
65 50 abscld 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( abs ` [_ z / k ]_ B ) e. RR )
66 65 recnd 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( abs ` [_ z / k ]_ B ) e. CC )
67 26 61 32 33 34 63 64 66 fprodsplitsn 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> prod_ k e. ( y u. { z } ) ( abs ` B ) = ( prod_ k e. y ( abs ` B ) x. ( abs ` [_ z / k ]_ B ) ) )
68 67 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( abs ` prod_ k e. y B ) = prod_ k e. y ( abs ` B ) ) -> prod_ k e. ( y u. { z } ) ( abs ` B ) = ( prod_ k e. y ( abs ` B ) x. ( abs ` [_ z / k ]_ B ) ) )
69 25 59 68 3eqtr4d 
 |-  ( ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) /\ ( abs ` prod_ k e. y B ) = prod_ k e. y ( abs ` B ) ) -> ( abs ` prod_ k e. ( y u. { z } ) B ) = prod_ k e. ( y u. { z } ) ( abs ` B ) )
70 69 ex 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( ( abs ` prod_ k e. y B ) = prod_ k e. y ( abs ` B ) -> ( abs ` prod_ k e. ( y u. { z } ) B ) = prod_ k e. ( y u. { z } ) ( abs ` B ) ) )
71 6 10 14 18 24 70 1 findcard2d 
 |-  ( ph -> ( abs ` prod_ k e. A B ) = prod_ k e. A ( abs ` B ) )