Metamath Proof Explorer

Theorem dprdfeq0

Description: The zero function is the only function that sums to zero in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses eldprdi.0 
|- .0. = ( 0g ` G )
eldprdi.w 
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
eldprdi.1 
|- ( ph -> G dom DProd S )
eldprdi.2 
|- ( ph -> dom S = I )
eldprdi.3 
|- ( ph -> F e. W )
Assertion dprdfeq0 
|- ( ph -> ( ( G gsum F ) = .0. <-> F = ( x e. I |-> .0. ) ) )

Proof

Step Hyp Ref Expression
1 eldprdi.0 
 |-  .0. = ( 0g ` G )
2 eldprdi.w 
 |-  W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
3 eldprdi.1 
 |-  ( ph -> G dom DProd S )
4 eldprdi.2 
 |-  ( ph -> dom S = I )
5 eldprdi.3 
 |-  ( ph -> F e. W )
6 eqid 
 |-  ( Base ` G ) = ( Base ` G )
7 2 3 4 5 6 dprdff 
 |-  ( ph -> F : I --> ( Base ` G ) )
8 7 feqmptd 
 |-  ( ph -> F = ( x e. I |-> ( F ` x ) ) )
9 8 adantr 
 |-  ( ( ph /\ ( G gsum F ) = .0. ) -> F = ( x e. I |-> ( F ` x ) ) )
10 2 3 4 5 dprdfcl 
 |-  ( ( ph /\ x e. I ) -> ( F ` x ) e. ( S ` x ) )
11 10 adantlr 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( F ` x ) e. ( S ` x ) )
12 3 ad2antrr 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> G dom DProd S )
13 4 ad2antrr 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> dom S = I )
14 simpr 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> x e. I )
15 eqid 
 |-  ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) = ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) )
16 1 2 12 13 14 11 15 dprdfid 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) e. W /\ ( G gsum ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) ) = ( F ` x ) ) )
17 16 simpld 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) e. W )
18 5 ad2antrr 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> F e. W )
19 eqid 
 |-  ( -g ` G ) = ( -g ` G )
20 1 2 12 13 17 18 19 dprdfsub 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( ( ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) oF ( -g ` G ) F ) e. W /\ ( G gsum ( ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) oF ( -g ` G ) F ) ) = ( ( G gsum ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) ) ( -g ` G ) ( G gsum F ) ) ) )
21 20 simprd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( G gsum ( ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) oF ( -g ` G ) F ) ) = ( ( G gsum ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) ) ( -g ` G ) ( G gsum F ) ) )
22 3 4 dprddomcld 
 |-  ( ph -> I e. _V )
23 22 ad2antrr 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> I e. _V )
24 fvex 
 |-  ( F ` x ) e. _V
25 1 fvexi 
 |-  .0. e. _V
26 24 25 ifex 
 |-  if ( y = x , ( F ` x ) , .0. ) e. _V
27 26 a1i 
 |-  ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) -> if ( y = x , ( F ` x ) , .0. ) e. _V )
28 fvexd 
 |-  ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) -> ( F ` y ) e. _V )
29 eqidd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) = ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) )
30 7 ad2antrr 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> F : I --> ( Base ` G ) )
31 30 feqmptd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> F = ( y e. I |-> ( F ` y ) ) )
32 23 27 28 29 31 offval2 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) oF ( -g ` G ) F ) = ( y e. I |-> ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) ) )
33 32 oveq2d 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( G gsum ( ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) oF ( -g ` G ) F ) ) = ( G gsum ( y e. I |-> ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) ) ) )
34 16 simprd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( G gsum ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) ) = ( F ` x ) )
35 simplr 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( G gsum F ) = .0. )
36 34 35 oveq12d 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( ( G gsum ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) ) ( -g ` G ) ( G gsum F ) ) = ( ( F ` x ) ( -g ` G ) .0. ) )
37 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
38 12 37 syl 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> G e. Grp )
39 30 14 ffvelrnd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( F ` x ) e. ( Base ` G ) )
40 6 1 19 grpsubid1 
 |-  ( ( G e. Grp /\ ( F ` x ) e. ( Base ` G ) ) -> ( ( F ` x ) ( -g ` G ) .0. ) = ( F ` x ) )
41 38 39 40 syl2anc 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( ( F ` x ) ( -g ` G ) .0. ) = ( F ` x ) )
42 36 41 eqtrd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( ( G gsum ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) ) ( -g ` G ) ( G gsum F ) ) = ( F ` x ) )
43 21 33 42 3eqtr3d 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( G gsum ( y e. I |-> ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) ) ) = ( F ` x ) )
44 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
45 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
46 3 37 45 3syl 
 |-  ( ph -> G e. Mnd )
47 46 ad2antrr 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> G e. Mnd )
48 6 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
49 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
50 38 48 49 3syl 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
51 imassrn 
 |-  ( S " ( I \ { x } ) ) C_ ran S
52 3 4 dprdf2 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
53 52 ad2antrr 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> S : I --> ( SubGrp ` G ) )
54 53 frnd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ran S C_ ( SubGrp ` G ) )
55 mresspw 
 |-  ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
56 50 55 syl 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
57 54 56 sstrd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ran S C_ ~P ( Base ` G ) )
58 51 57 sstrid 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( S " ( I \ { x } ) ) C_ ~P ( Base ` G ) )
59 sspwuni 
 |-  ( ( S " ( I \ { x } ) ) C_ ~P ( Base ` G ) <-> U. ( S " ( I \ { x } ) ) C_ ( Base ` G ) )
60 58 59 sylib 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> U. ( S " ( I \ { x } ) ) C_ ( Base ` G ) )
61 eqid 
 |-  ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
62 61 mrccl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ( S " ( I \ { x } ) ) C_ ( Base ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) e. ( SubGrp ` G ) )
63 50 60 62 syl2anc 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) e. ( SubGrp ` G ) )
64 subgsubm 
 |-  ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) e. ( SubGrp ` G ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) e. ( SubMnd ` G ) )
65 63 64 syl 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) e. ( SubMnd ` G ) )
66 oveq1 
 |-  ( ( F ` x ) = if ( y = x , ( F ` x ) , .0. ) -> ( ( F ` x ) ( -g ` G ) ( F ` y ) ) = ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) )
67 66 eleq1d 
 |-  ( ( F ` x ) = if ( y = x , ( F ` x ) , .0. ) -> ( ( ( F ` x ) ( -g ` G ) ( F ` y ) ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) <-> ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) )
68 oveq1 
 |-  ( .0. = if ( y = x , ( F ` x ) , .0. ) -> ( .0. ( -g ` G ) ( F ` y ) ) = ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) )
69 68 eleq1d 
 |-  ( .0. = if ( y = x , ( F ` x ) , .0. ) -> ( ( .0. ( -g ` G ) ( F ` y ) ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) <-> ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) )
70 simpr 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ y = x ) -> y = x )
71 70 fveq2d 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ y = x ) -> ( F ` y ) = ( F ` x ) )
72 71 oveq2d 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ y = x ) -> ( ( F ` x ) ( -g ` G ) ( F ` y ) ) = ( ( F ` x ) ( -g ` G ) ( F ` x ) ) )
73 6 1 19 grpsubid 
 |-  ( ( G e. Grp /\ ( F ` x ) e. ( Base ` G ) ) -> ( ( F ` x ) ( -g ` G ) ( F ` x ) ) = .0. )
74 38 39 73 syl2anc 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( ( F ` x ) ( -g ` G ) ( F ` x ) ) = .0. )
75 1 subg0cl 
 |-  ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) e. ( SubGrp ` G ) -> .0. e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
76 63 75 syl 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> .0. e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
77 74 76 eqeltrd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( ( F ` x ) ( -g ` G ) ( F ` x ) ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
78 77 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ y = x ) -> ( ( F ` x ) ( -g ` G ) ( F ` x ) ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
79 72 78 eqeltrd 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ y = x ) -> ( ( F ` x ) ( -g ` G ) ( F ` y ) ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
80 63 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ -. y = x ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) e. ( SubGrp ` G ) )
81 80 75 syl 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ -. y = x ) -> .0. e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
82 50 61 60 mrcssidd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> U. ( S " ( I \ { x } ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
83 82 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ -. y = x ) -> U. ( S " ( I \ { x } ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
84 2 12 13 18 dprdfcl 
 |-  ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) -> ( F ` y ) e. ( S ` y ) )
85 84 adantr 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ -. y = x ) -> ( F ` y ) e. ( S ` y ) )
86 53 ffnd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> S Fn I )
87 86 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ -. y = x ) -> S Fn I )
88 difssd 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ -. y = x ) -> ( I \ { x } ) C_ I )
89 df-ne 
 |-  ( y =/= x <-> -. y = x )
90 eldifsn 
 |-  ( y e. ( I \ { x } ) <-> ( y e. I /\ y =/= x ) )
91 90 biimpri 
 |-  ( ( y e. I /\ y =/= x ) -> y e. ( I \ { x } ) )
92 89 91 sylan2br 
 |-  ( ( y e. I /\ -. y = x ) -> y e. ( I \ { x } ) )
93 92 adantll 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ -. y = x ) -> y e. ( I \ { x } ) )
94 fnfvima 
 |-  ( ( S Fn I /\ ( I \ { x } ) C_ I /\ y e. ( I \ { x } ) ) -> ( S ` y ) e. ( S " ( I \ { x } ) ) )
95 87 88 93 94 syl3anc 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ -. y = x ) -> ( S ` y ) e. ( S " ( I \ { x } ) ) )
96 elunii 
 |-  ( ( ( F ` y ) e. ( S ` y ) /\ ( S ` y ) e. ( S " ( I \ { x } ) ) ) -> ( F ` y ) e. U. ( S " ( I \ { x } ) ) )
97 85 95 96 syl2anc 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ -. y = x ) -> ( F ` y ) e. U. ( S " ( I \ { x } ) ) )
98 83 97 sseldd 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ -. y = x ) -> ( F ` y ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
99 19 subgsubcl 
 |-  ( ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) e. ( SubGrp ` G ) /\ .0. e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) /\ ( F ` y ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) -> ( .0. ( -g ` G ) ( F ` y ) ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
100 80 81 98 99 syl3anc 
 |-  ( ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) /\ -. y = x ) -> ( .0. ( -g ` G ) ( F ` y ) ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
101 67 69 79 100 ifbothda 
 |-  ( ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) /\ y e. I ) -> ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
102 101 fmpttd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( y e. I |-> ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) ) : I --> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
103 20 simpld 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( ( y e. I |-> if ( y = x , ( F ` x ) , .0. ) ) oF ( -g ` G ) F ) e. W )
104 32 103 eqeltrrd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( y e. I |-> ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) ) e. W )
105 2 12 13 104 44 dprdfcntz 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ran ( y e. I |-> ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) ) C_ ( ( Cntz ` G ) ` ran ( y e. I |-> ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) ) ) )
106 2 12 13 104 dprdffsupp 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( y e. I |-> ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) ) finSupp .0. )
107 1 44 47 23 65 102 105 106 gsumzsubmcl 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( G gsum ( y e. I |-> ( if ( y = x , ( F ` x ) , .0. ) ( -g ` G ) ( F ` y ) ) ) ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
108 43 107 eqeltrrd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( F ` x ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
109 11 108 elind 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( F ` x ) e. ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) )
110 12 13 14 1 61 dprddisj 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } )
111 109 110 eleqtrd 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( F ` x ) e. { .0. } )
112 elsni 
 |-  ( ( F ` x ) e. { .0. } -> ( F ` x ) = .0. )
113 111 112 syl 
 |-  ( ( ( ph /\ ( G gsum F ) = .0. ) /\ x e. I ) -> ( F ` x ) = .0. )
114 113 mpteq2dva 
 |-  ( ( ph /\ ( G gsum F ) = .0. ) -> ( x e. I |-> ( F ` x ) ) = ( x e. I |-> .0. ) )
115 9 114 eqtrd 
 |-  ( ( ph /\ ( G gsum F ) = .0. ) -> F = ( x e. I |-> .0. ) )
116 115 ex 
 |-  ( ph -> ( ( G gsum F ) = .0. -> F = ( x e. I |-> .0. ) ) )
117 1 gsumz 
 |-  ( ( G e. Mnd /\ I e. _V ) -> ( G gsum ( x e. I |-> .0. ) ) = .0. )
118 46 22 117 syl2anc 
 |-  ( ph -> ( G gsum ( x e. I |-> .0. ) ) = .0. )
119 oveq2 
 |-  ( F = ( x e. I |-> .0. ) -> ( G gsum F ) = ( G gsum ( x e. I |-> .0. ) ) )
120 119 eqeq1d 
 |-  ( F = ( x e. I |-> .0. ) -> ( ( G gsum F ) = .0. <-> ( G gsum ( x e. I |-> .0. ) ) = .0. ) )
121 118 120 syl5ibrcom 
 |-  ( ph -> ( F = ( x e. I |-> .0. ) -> ( G gsum F ) = .0. ) )
122 116 121 impbid 
 |-  ( ph -> ( ( G gsum F ) = .0. <-> F = ( x e. I |-> .0. ) ) )