Metamath Proof Explorer

Theorem gsumconst

Description: Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gsumconst.b 
|- B = ( Base ` G )
gsumconst.m 
|- .x. = ( .g ` G )
Assertion gsumconst 
|- ( ( G e. Mnd /\ A e. Fin /\ X e. B ) -> ( G gsum ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) )

Proof

Step Hyp Ref Expression
1 gsumconst.b 
 |-  B = ( Base ` G )
2 gsumconst.m 
 |-  .x. = ( .g ` G )
3 simpl3 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ A = (/) ) -> X e. B )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 1 4 2 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
6 3 5 syl 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ A = (/) ) -> ( 0 .x. X ) = ( 0g ` G ) )
7 fveq2 
 |-  ( A = (/) -> ( # ` A ) = ( # ` (/) ) )
8 7 adantl 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ A = (/) ) -> ( # ` A ) = ( # ` (/) ) )
9 hash0 
 |-  ( # ` (/) ) = 0
10 8 9 eqtrdi 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ A = (/) ) -> ( # ` A ) = 0 )
11 10 oveq1d 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ A = (/) ) -> ( ( # ` A ) .x. X ) = ( 0 .x. X ) )
12 mpteq1 
 |-  ( A = (/) -> ( k e. A |-> X ) = ( k e. (/) |-> X ) )
13 12 adantl 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ A = (/) ) -> ( k e. A |-> X ) = ( k e. (/) |-> X ) )
14 mpt0 
 |-  ( k e. (/) |-> X ) = (/)
15 13 14 eqtrdi 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ A = (/) ) -> ( k e. A |-> X ) = (/) )
16 15 oveq2d 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ A = (/) ) -> ( G gsum ( k e. A |-> X ) ) = ( G gsum (/) ) )
17 4 gsum0 
 |-  ( G gsum (/) ) = ( 0g ` G )
18 16 17 eqtrdi 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ A = (/) ) -> ( G gsum ( k e. A |-> X ) ) = ( 0g ` G ) )
19 6 11 18 3eqtr4rd 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ A = (/) ) -> ( G gsum ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) )
20 19 ex 
 |-  ( ( G e. Mnd /\ A e. Fin /\ X e. B ) -> ( A = (/) -> ( G gsum ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) ) )
21 simprl 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN )
22 nnuz 
 |-  NN = ( ZZ>= ` 1 )
23 21 22 eleqtrdi 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. ( ZZ>= ` 1 ) )
24 simpr 
 |-  ( ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> x e. ( 1 ... ( # ` A ) ) )
25 simpl3 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> X e. B )
26 25 adantr 
 |-  ( ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> X e. B )
27 eqid 
 |-  ( x e. ( 1 ... ( # ` A ) ) |-> X ) = ( x e. ( 1 ... ( # ` A ) ) |-> X )
28 27 fvmpt2 
 |-  ( ( x e. ( 1 ... ( # ` A ) ) /\ X e. B ) -> ( ( x e. ( 1 ... ( # ` A ) ) |-> X ) ` x ) = X )
29 24 26 28 syl2anc 
 |-  ( ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( x e. ( 1 ... ( # ` A ) ) |-> X ) ` x ) = X )
30 f1of 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) --> A )
31 30 ad2antll 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) --> A )
32 31 ffvelcdmda 
 |-  ( ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( f ` x ) e. A )
33 31 feqmptd 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f = ( x e. ( 1 ... ( # ` A ) ) |-> ( f ` x ) ) )
34 eqidd 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> X ) = ( k e. A |-> X ) )
35 eqidd 
 |-  ( k = ( f ` x ) -> X = X )
36 32 33 34 35 fmptco 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> X ) o. f ) = ( x e. ( 1 ... ( # ` A ) ) |-> X ) )
37 36 fveq1d 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( ( k e. A |-> X ) o. f ) ` x ) = ( ( x e. ( 1 ... ( # ` A ) ) |-> X ) ` x ) )
38 37 adantr 
 |-  ( ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> X ) o. f ) ` x ) = ( ( x e. ( 1 ... ( # ` A ) ) |-> X ) ` x ) )
39 elfznn 
 |-  ( x e. ( 1 ... ( # ` A ) ) -> x e. NN )
40 fvconst2g 
 |-  ( ( X e. B /\ x e. NN ) -> ( ( NN X. { X } ) ` x ) = X )
41 25 39 40 syl2an 
 |-  ( ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( NN X. { X } ) ` x ) = X )
42 29 38 41 3eqtr4d 
 |-  ( ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> X ) o. f ) ` x ) = ( ( NN X. { X } ) ` x ) )
43 23 42 seqfveq 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( seq 1 ( ( +g ` G ) , ( ( k e. A |-> X ) o. f ) ) ` ( # ` A ) ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` ( # ` A ) ) )
44 eqid 
 |-  ( +g ` G ) = ( +g ` G )
45 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
46 simpl1 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> G e. Mnd )
47 simpl2 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> A e. Fin )
48 25 adantr 
 |-  ( ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ k e. A ) -> X e. B )
49 48 fmpttd 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> X ) : A --> B )
50 eqidd 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( X ( +g ` G ) X ) = ( X ( +g ` G ) X ) )
51 1 44 45 elcntzsn 
 |-  ( X e. B -> ( X e. ( ( Cntz ` G ) ` { X } ) <-> ( X e. B /\ ( X ( +g ` G ) X ) = ( X ( +g ` G ) X ) ) ) )
52 25 51 syl 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( X e. ( ( Cntz ` G ) ` { X } ) <-> ( X e. B /\ ( X ( +g ` G ) X ) = ( X ( +g ` G ) X ) ) ) )
53 25 50 52 mpbir2and 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> X e. ( ( Cntz ` G ) ` { X } ) )
54 53 snssd 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> { X } C_ ( ( Cntz ` G ) ` { X } ) )
55 snidg 
 |-  ( X e. B -> X e. { X } )
56 25 55 syl 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> X e. { X } )
57 56 adantr 
 |-  ( ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ k e. A ) -> X e. { X } )
58 57 fmpttd 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> X ) : A --> { X } )
59 58 frnd 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ran ( k e. A |-> X ) C_ { X } )
60 45 cntzidss 
 |-  ( ( { X } C_ ( ( Cntz ` G ) ` { X } ) /\ ran ( k e. A |-> X ) C_ { X } ) -> ran ( k e. A |-> X ) C_ ( ( Cntz ` G ) ` ran ( k e. A |-> X ) ) )
61 54 59 60 syl2anc 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ran ( k e. A |-> X ) C_ ( ( Cntz ` G ) ` ran ( k e. A |-> X ) ) )
62 f1of1 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) -1-1-> A )
63 62 ad2antll 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-> A )
64 suppssdm 
 |-  ( ( k e. A |-> X ) supp ( 0g ` G ) ) C_ dom ( k e. A |-> X )
65 eqid 
 |-  ( k e. A |-> X ) = ( k e. A |-> X )
66 65 dmmptss 
 |-  dom ( k e. A |-> X ) C_ A
67 66 a1i 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> dom ( k e. A |-> X ) C_ A )
68 64 67 sstrid 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> X ) supp ( 0g ` G ) ) C_ A )
69 f1ofo 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) -onto-> A )
70 forn 
 |-  ( f : ( 1 ... ( # ` A ) ) -onto-> A -> ran f = A )
71 69 70 syl 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ran f = A )
72 71 ad2antll 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ran f = A )
73 68 72 sseqtrrd 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> X ) supp ( 0g ` G ) ) C_ ran f )
74 eqid 
 |-  ( ( ( k e. A |-> X ) o. f ) supp ( 0g ` G ) ) = ( ( ( k e. A |-> X ) o. f ) supp ( 0g ` G ) )
75 1 4 44 45 46 47 49 61 21 63 73 74 gsumval3 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( G gsum ( k e. A |-> X ) ) = ( seq 1 ( ( +g ` G ) , ( ( k e. A |-> X ) o. f ) ) ` ( # ` A ) ) )
76 eqid 
 |-  seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` G ) , ( NN X. { X } ) )
77 1 44 2 76 mulgnn 
 |-  ( ( ( # ` A ) e. NN /\ X e. B ) -> ( ( # ` A ) .x. X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` ( # ` A ) ) )
78 21 25 77 syl2anc 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( # ` A ) .x. X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` ( # ` A ) ) )
79 43 75 78 3eqtr4d 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( G gsum ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) )
80 79 expr 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( G gsum ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) ) )
81 80 exlimdv 
 |-  ( ( ( G e. Mnd /\ A e. Fin /\ X e. B ) /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( G gsum ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) ) )
82 81 expimpd 
 |-  ( ( G e. Mnd /\ A e. Fin /\ X e. B ) -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( G gsum ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) ) )
83 fz1f1o 
 |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
84 83 3ad2ant2 
 |-  ( ( G e. Mnd /\ A e. Fin /\ X e. B ) -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
85 20 82 84 mpjaod 
 |-  ( ( G e. Mnd /\ A e. Fin /\ X e. B ) -> ( G gsum ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) )