Metamath Proof Explorer

Theorem gsumpt

Description: Sum of a family that is nonzero at at most one point. (Contributed by Stefan O'Rear, 7-Feb-2015) (Revised by Mario Carneiro, 25-Apr-2016) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsumpt.b 
|- B = ( Base ` G )
gsumpt.z 
|- .0. = ( 0g ` G )
gsumpt.g 
|- ( ph -> G e. Mnd )
gsumpt.a 
|- ( ph -> A e. V )
gsumpt.x 
|- ( ph -> X e. A )
gsumpt.f 
|- ( ph -> F : A --> B )
gsumpt.s 
|- ( ph -> ( F supp .0. ) C_ { X } )
Assertion gsumpt 
|- ( ph -> ( G gsum F ) = ( F ` X ) )

Proof

Step Hyp Ref Expression
1 gsumpt.b 
 |-  B = ( Base ` G )
2 gsumpt.z 
 |-  .0. = ( 0g ` G )
3 gsumpt.g 
 |-  ( ph -> G e. Mnd )
4 gsumpt.a 
 |-  ( ph -> A e. V )
5 gsumpt.x 
 |-  ( ph -> X e. A )
6 gsumpt.f 
 |-  ( ph -> F : A --> B )
7 gsumpt.s 
 |-  ( ph -> ( F supp .0. ) C_ { X } )
8 5 snssd 
 |-  ( ph -> { X } C_ A )
9 6 8 feqresmpt 
 |-  ( ph -> ( F |` { X } ) = ( a e. { X } |-> ( F ` a ) ) )
10 9 oveq2d 
 |-  ( ph -> ( G gsum ( F |` { X } ) ) = ( G gsum ( a e. { X } |-> ( F ` a ) ) ) )
11 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
12 6 5 ffvelcdmd 
 |-  ( ph -> ( F ` X ) e. B )
13 eqidd 
 |-  ( ph -> ( ( F ` X ) ( +g ` G ) ( F ` X ) ) = ( ( F ` X ) ( +g ` G ) ( F ` X ) ) )
14 eqid 
 |-  ( +g ` G ) = ( +g ` G )
15 1 14 11 elcntzsn 
 |-  ( ( F ` X ) e. B -> ( ( F ` X ) e. ( ( Cntz ` G ) ` { ( F ` X ) } ) <-> ( ( F ` X ) e. B /\ ( ( F ` X ) ( +g ` G ) ( F ` X ) ) = ( ( F ` X ) ( +g ` G ) ( F ` X ) ) ) ) )
16 12 15 syl 
 |-  ( ph -> ( ( F ` X ) e. ( ( Cntz ` G ) ` { ( F ` X ) } ) <-> ( ( F ` X ) e. B /\ ( ( F ` X ) ( +g ` G ) ( F ` X ) ) = ( ( F ` X ) ( +g ` G ) ( F ` X ) ) ) ) )
17 12 13 16 mpbir2and 
 |-  ( ph -> ( F ` X ) e. ( ( Cntz ` G ) ` { ( F ` X ) } ) )
18 17 snssd 
 |-  ( ph -> { ( F ` X ) } C_ ( ( Cntz ` G ) ` { ( F ` X ) } ) )
19 eqid 
 |-  ( mrCls ` ( SubMnd ` G ) ) = ( mrCls ` ( SubMnd ` G ) )
20 eqid 
 |-  ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) ) = ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
21 11 19 20 cntzspan 
 |-  ( ( G e. Mnd /\ { ( F ` X ) } C_ ( ( Cntz ` G ) ` { ( F ` X ) } ) ) -> ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) ) e. CMnd )
22 3 18 21 syl2anc 
 |-  ( ph -> ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) ) e. CMnd )
23 1 submacs 
 |-  ( G e. Mnd -> ( SubMnd ` G ) e. ( ACS ` B ) )
24 acsmre 
 |-  ( ( SubMnd ` G ) e. ( ACS ` B ) -> ( SubMnd ` G ) e. ( Moore ` B ) )
25 3 23 24 3syl 
 |-  ( ph -> ( SubMnd ` G ) e. ( Moore ` B ) )
26 12 snssd 
 |-  ( ph -> { ( F ` X ) } C_ B )
27 19 mrccl 
 |-  ( ( ( SubMnd ` G ) e. ( Moore ` B ) /\ { ( F ` X ) } C_ B ) -> ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) e. ( SubMnd ` G ) )
28 25 26 27 syl2anc 
 |-  ( ph -> ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) e. ( SubMnd ` G ) )
29 20 11 submcmn2 
 |-  ( ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) e. ( SubMnd ` G ) -> ( ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) ) e. CMnd <-> ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) C_ ( ( Cntz ` G ) ` ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) ) ) )
30 28 29 syl 
 |-  ( ph -> ( ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) ) e. CMnd <-> ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) C_ ( ( Cntz ` G ) ` ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) ) ) )
31 22 30 mpbid 
 |-  ( ph -> ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) C_ ( ( Cntz ` G ) ` ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) ) )
32 6 ffnd 
 |-  ( ph -> F Fn A )
33 simpr 
 |-  ( ( ( ph /\ a e. A ) /\ a = X ) -> a = X )
34 33 fveq2d 
 |-  ( ( ( ph /\ a e. A ) /\ a = X ) -> ( F ` a ) = ( F ` X ) )
35 25 19 26 mrcssidd 
 |-  ( ph -> { ( F ` X ) } C_ ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
36 fvex 
 |-  ( F ` X ) e. _V
37 36 snss 
 |-  ( ( F ` X ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) <-> { ( F ` X ) } C_ ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
38 35 37 sylibr 
 |-  ( ph -> ( F ` X ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
39 38 ad2antrr 
 |-  ( ( ( ph /\ a e. A ) /\ a = X ) -> ( F ` X ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
40 34 39 eqeltrd 
 |-  ( ( ( ph /\ a e. A ) /\ a = X ) -> ( F ` a ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
41 eldifsn 
 |-  ( a e. ( A \ { X } ) <-> ( a e. A /\ a =/= X ) )
42 2 fvexi 
 |-  .0. e. _V
43 42 a1i 
 |-  ( ph -> .0. e. _V )
44 6 7 4 43 suppssr 
 |-  ( ( ph /\ a e. ( A \ { X } ) ) -> ( F ` a ) = .0. )
45 41 44 sylan2br 
 |-  ( ( ph /\ ( a e. A /\ a =/= X ) ) -> ( F ` a ) = .0. )
46 2 subm0cl 
 |-  ( ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) e. ( SubMnd ` G ) -> .0. e. ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
47 28 46 syl 
 |-  ( ph -> .0. e. ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
48 47 adantr 
 |-  ( ( ph /\ ( a e. A /\ a =/= X ) ) -> .0. e. ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
49 45 48 eqeltrd 
 |-  ( ( ph /\ ( a e. A /\ a =/= X ) ) -> ( F ` a ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
50 49 anassrs 
 |-  ( ( ( ph /\ a e. A ) /\ a =/= X ) -> ( F ` a ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
51 40 50 pm2.61dane 
 |-  ( ( ph /\ a e. A ) -> ( F ` a ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
52 51 ralrimiva 
 |-  ( ph -> A. a e. A ( F ` a ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
53 ffnfv 
 |-  ( F : A --> ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) <-> ( F Fn A /\ A. a e. A ( F ` a ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) ) )
54 32 52 53 sylanbrc 
 |-  ( ph -> F : A --> ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
55 54 frnd 
 |-  ( ph -> ran F C_ ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) )
56 11 cntzidss 
 |-  ( ( ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) C_ ( ( Cntz ` G ) ` ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) ) /\ ran F C_ ( ( mrCls ` ( SubMnd ` G ) ) ` { ( F ` X ) } ) ) -> ran F C_ ( ( Cntz ` G ) ` ran F ) )
57 31 55 56 syl2anc 
 |-  ( ph -> ran F C_ ( ( Cntz ` G ) ` ran F ) )
58 6 ffund 
 |-  ( ph -> Fun F )
59 snfi 
 |-  { X } e. Fin
60 ssfi 
 |-  ( ( { X } e. Fin /\ ( F supp .0. ) C_ { X } ) -> ( F supp .0. ) e. Fin )
61 59 7 60 sylancr 
 |-  ( ph -> ( F supp .0. ) e. Fin )
62 6 4 fexd 
 |-  ( ph -> F e. _V )
63 isfsupp 
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( F finSupp .0. <-> ( Fun F /\ ( F supp .0. ) e. Fin ) ) )
64 62 43 63 syl2anc 
 |-  ( ph -> ( F finSupp .0. <-> ( Fun F /\ ( F supp .0. ) e. Fin ) ) )
65 58 61 64 mpbir2and 
 |-  ( ph -> F finSupp .0. )
66 1 2 11 3 4 6 57 7 65 gsumzres 
 |-  ( ph -> ( G gsum ( F |` { X } ) ) = ( G gsum F ) )
67 fveq2 
 |-  ( a = X -> ( F ` a ) = ( F ` X ) )
68 1 67 gsumsn 
 |-  ( ( G e. Mnd /\ X e. A /\ ( F ` X ) e. B ) -> ( G gsum ( a e. { X } |-> ( F ` a ) ) ) = ( F ` X ) )
69 3 5 12 68 syl3anc 
 |-  ( ph -> ( G gsum ( a e. { X } |-> ( F ` a ) ) ) = ( F ` X ) )
70 10 66 69 3eqtr3d 
 |-  ( ph -> ( G gsum F ) = ( F ` X ) )