Step |
Hyp |
Ref |
Expression |
1 |
|
gsummgp0.g |
|- G = ( mulGrp ` R ) |
2 |
|
gsummgp0.0 |
|- .0. = ( 0g ` R ) |
3 |
|
gsummgp0.r |
|- ( ph -> R e. CRing ) |
4 |
|
gsummgp0.n |
|- ( ph -> N e. Fin ) |
5 |
|
gsummgp0.a |
|- ( ( ph /\ n e. N ) -> A e. ( Base ` R ) ) |
6 |
|
gsummgp0.e |
|- ( ( ph /\ n = i ) -> A = B ) |
7 |
|
gsummgp0.b |
|- ( ph -> E. i e. N B = .0. ) |
8 |
|
difsnid |
|- ( i e. N -> ( ( N \ { i } ) u. { i } ) = N ) |
9 |
8
|
eqcomd |
|- ( i e. N -> N = ( ( N \ { i } ) u. { i } ) ) |
10 |
9
|
ad2antrl |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> N = ( ( N \ { i } ) u. { i } ) ) |
11 |
10
|
mpteq1d |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( n e. N |-> A ) = ( n e. ( ( N \ { i } ) u. { i } ) |-> A ) ) |
12 |
11
|
oveq2d |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( G gsum ( n e. N |-> A ) ) = ( G gsum ( n e. ( ( N \ { i } ) u. { i } ) |-> A ) ) ) |
13 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
14 |
1 13
|
mgpbas |
|- ( Base ` R ) = ( Base ` G ) |
15 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
16 |
1 15
|
mgpplusg |
|- ( .r ` R ) = ( +g ` G ) |
17 |
1
|
crngmgp |
|- ( R e. CRing -> G e. CMnd ) |
18 |
3 17
|
syl |
|- ( ph -> G e. CMnd ) |
19 |
18
|
adantr |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> G e. CMnd ) |
20 |
|
diffi |
|- ( N e. Fin -> ( N \ { i } ) e. Fin ) |
21 |
4 20
|
syl |
|- ( ph -> ( N \ { i } ) e. Fin ) |
22 |
21
|
adantr |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( N \ { i } ) e. Fin ) |
23 |
|
simpl |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ph ) |
24 |
|
eldifi |
|- ( n e. ( N \ { i } ) -> n e. N ) |
25 |
23 24 5
|
syl2an |
|- ( ( ( ph /\ ( i e. N /\ B = .0. ) ) /\ n e. ( N \ { i } ) ) -> A e. ( Base ` R ) ) |
26 |
|
simprl |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> i e. N ) |
27 |
|
neldifsnd |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> -. i e. ( N \ { i } ) ) |
28 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
29 |
3 28
|
syl |
|- ( ph -> R e. Ring ) |
30 |
|
ringmnd |
|- ( R e. Ring -> R e. Mnd ) |
31 |
13 2
|
mndidcl |
|- ( R e. Mnd -> .0. e. ( Base ` R ) ) |
32 |
29 30 31
|
3syl |
|- ( ph -> .0. e. ( Base ` R ) ) |
33 |
32
|
adantr |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> .0. e. ( Base ` R ) ) |
34 |
|
eleq1 |
|- ( B = .0. -> ( B e. ( Base ` R ) <-> .0. e. ( Base ` R ) ) ) |
35 |
34
|
ad2antll |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( B e. ( Base ` R ) <-> .0. e. ( Base ` R ) ) ) |
36 |
33 35
|
mpbird |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> B e. ( Base ` R ) ) |
37 |
6
|
adantlr |
|- ( ( ( ph /\ ( i e. N /\ B = .0. ) ) /\ n = i ) -> A = B ) |
38 |
14 16 19 22 25 26 27 36 37
|
gsumunsnd |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( G gsum ( n e. ( ( N \ { i } ) u. { i } ) |-> A ) ) = ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) B ) ) |
39 |
|
oveq2 |
|- ( B = .0. -> ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) B ) = ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) .0. ) ) |
40 |
39
|
ad2antll |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) B ) = ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) .0. ) ) |
41 |
24 5
|
sylan2 |
|- ( ( ph /\ n e. ( N \ { i } ) ) -> A e. ( Base ` R ) ) |
42 |
41
|
ralrimiva |
|- ( ph -> A. n e. ( N \ { i } ) A e. ( Base ` R ) ) |
43 |
14 18 21 42
|
gsummptcl |
|- ( ph -> ( G gsum ( n e. ( N \ { i } ) |-> A ) ) e. ( Base ` R ) ) |
44 |
43
|
adantr |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( G gsum ( n e. ( N \ { i } ) |-> A ) ) e. ( Base ` R ) ) |
45 |
13 15 2
|
ringrz |
|- ( ( R e. Ring /\ ( G gsum ( n e. ( N \ { i } ) |-> A ) ) e. ( Base ` R ) ) -> ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) .0. ) = .0. ) |
46 |
29 44 45
|
syl2an2r |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) .0. ) = .0. ) |
47 |
40 46
|
eqtrd |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) B ) = .0. ) |
48 |
12 38 47
|
3eqtrd |
|- ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( G gsum ( n e. N |-> A ) ) = .0. ) |
49 |
7 48
|
rexlimddv |
|- ( ph -> ( G gsum ( n e. N |-> A ) ) = .0. ) |