This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmdprdsplitlem

Description: Lemma for dmdprdsplit . (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses dmdprdsplitlem.0 
|- .0. = ( 0g ` G )
dmdprdsplitlem.w 
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
dmdprdsplitlem.1 
|- ( ph -> G dom DProd S )
dmdprdsplitlem.2 
|- ( ph -> dom S = I )
dmdprdsplitlem.3 
|- ( ph -> A C_ I )
dmdprdsplitlem.4 
|- ( ph -> F e. W )
dmdprdsplitlem.5 
|- ( ph -> ( G gsum F ) e. ( G DProd ( S |` A ) ) )
Assertion dmdprdsplitlem 
|- ( ( ph /\ X e. ( I \ A ) ) -> ( F ` X ) = .0. )

Proof

Step Hyp Ref Expression
1 dmdprdsplitlem.0 
 |-  .0. = ( 0g ` G )
2 dmdprdsplitlem.w 
 |-  W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
3 dmdprdsplitlem.1 
 |-  ( ph -> G dom DProd S )
4 dmdprdsplitlem.2 
 |-  ( ph -> dom S = I )
5 dmdprdsplitlem.3 
 |-  ( ph -> A C_ I )
6 dmdprdsplitlem.4 
 |-  ( ph -> F e. W )
7 dmdprdsplitlem.5 
 |-  ( ph -> ( G gsum F ) e. ( G DProd ( S |` A ) ) )
8 3 4 dprdf2 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
9 8 5 fssresd 
 |-  ( ph -> ( S |` A ) : A --> ( SubGrp ` G ) )
10 fdm 
 |-  ( ( S |` A ) : A --> ( SubGrp ` G ) -> dom ( S |` A ) = A )
11 eqid 
 |-  { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } = { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. }
12 1 11 eldprd 
 |-  ( dom ( S |` A ) = A -> ( ( G gsum F ) e. ( G DProd ( S |` A ) ) <-> ( G dom DProd ( S |` A ) /\ E. f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } ( G gsum F ) = ( G gsum f ) ) ) )
13 9 10 12 3syl 
 |-  ( ph -> ( ( G gsum F ) e. ( G DProd ( S |` A ) ) <-> ( G dom DProd ( S |` A ) /\ E. f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } ( G gsum F ) = ( G gsum f ) ) ) )
14 7 13 mpbid 
 |-  ( ph -> ( G dom DProd ( S |` A ) /\ E. f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } ( G gsum F ) = ( G gsum f ) ) )
15 14 simprd 
 |-  ( ph -> E. f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } ( G gsum F ) = ( G gsum f ) )
16 15 adantr 
 |-  ( ( ph /\ X e. ( I \ A ) ) -> E. f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } ( G gsum F ) = ( G gsum f ) )
17 simprr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( G gsum F ) = ( G gsum f ) )
18 14 simpld 
 |-  ( ph -> G dom DProd ( S |` A ) )
19 18 ad2antrr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> G dom DProd ( S |` A ) )
20 9 10 syl 
 |-  ( ph -> dom ( S |` A ) = A )
21 20 ad2antrr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> dom ( S |` A ) = A )
22 simprl 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } )
23 eqid 
 |-  ( Base ` G ) = ( Base ` G )
24 11 19 21 22 23 dprdff 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> f : A --> ( Base ` G ) )
25 24 feqmptd 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> f = ( n e. A |-> ( f ` n ) ) )
26 5 ad2antrr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> A C_ I )
27 26 resmptd 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) |` A ) = ( n e. A |-> if ( n e. A , ( f ` n ) , .0. ) ) )
28 iftrue 
 |-  ( n e. A -> if ( n e. A , ( f ` n ) , .0. ) = ( f ` n ) )
29 28 mpteq2ia 
 |-  ( n e. A |-> if ( n e. A , ( f ` n ) , .0. ) ) = ( n e. A |-> ( f ` n ) )
30 27 29 eqtrdi 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) |` A ) = ( n e. A |-> ( f ` n ) ) )
31 25 30 eqtr4d 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> f = ( ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) |` A ) )
32 31 oveq2d 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( G gsum f ) = ( G gsum ( ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) |` A ) ) )
33 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
34 3 ad2antrr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> G dom DProd S )
35 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
36 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
37 34 35 36 3syl 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> G e. Mnd )
38 3 4 dprddomcld 
 |-  ( ph -> I e. _V )
39 38 ad2antrr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> I e. _V )
40 4 ad2antrr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> dom S = I )
41 19 adantr 
 |-  ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. I ) -> G dom DProd ( S |` A ) )
42 21 adantr 
 |-  ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. I ) -> dom ( S |` A ) = A )
43 simplrl 
 |-  ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. I ) -> f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } )
44 11 41 42 43 dprdfcl 
 |-  ( ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. I ) /\ n e. A ) -> ( f ` n ) e. ( ( S |` A ) ` n ) )
45 fvres 
 |-  ( n e. A -> ( ( S |` A ) ` n ) = ( S ` n ) )
46 45 adantl 
 |-  ( ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. I ) /\ n e. A ) -> ( ( S |` A ) ` n ) = ( S ` n ) )
47 44 46 eleqtrd 
 |-  ( ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. I ) /\ n e. A ) -> ( f ` n ) e. ( S ` n ) )
48 8 ad2antrr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> S : I --> ( SubGrp ` G ) )
49 48 ffvelcdmda 
 |-  ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. I ) -> ( S ` n ) e. ( SubGrp ` G ) )
50 1 subg0cl 
 |-  ( ( S ` n ) e. ( SubGrp ` G ) -> .0. e. ( S ` n ) )
51 49 50 syl 
 |-  ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. I ) -> .0. e. ( S ` n ) )
52 51 adantr 
 |-  ( ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. I ) /\ -. n e. A ) -> .0. e. ( S ` n ) )
53 47 52 ifclda 
 |-  ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. I ) -> if ( n e. A , ( f ` n ) , .0. ) e. ( S ` n ) )
54 38 mptexd 
 |-  ( ph -> ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) e. _V )
55 54 ad2antrr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) e. _V )
56 funmpt 
 |-  Fun ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) )
57 56 a1i 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> Fun ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) )
58 11 19 21 22 dprdffsupp 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> f finSupp .0. )
59 simpr 
 |-  ( ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. ( I \ ( f supp .0. ) ) ) /\ n e. A ) -> n e. A )
60 eldifn 
 |-  ( n e. ( I \ ( f supp .0. ) ) -> -. n e. ( f supp .0. ) )
61 60 ad2antlr 
 |-  ( ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. ( I \ ( f supp .0. ) ) ) /\ n e. A ) -> -. n e. ( f supp .0. ) )
62 59 61 eldifd 
 |-  ( ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. ( I \ ( f supp .0. ) ) ) /\ n e. A ) -> n e. ( A \ ( f supp .0. ) ) )
63 ssidd 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( f supp .0. ) C_ ( f supp .0. ) )
64 38 5 ssexd 
 |-  ( ph -> A e. _V )
65 64 ad2antrr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> A e. _V )
66 1 fvexi 
 |-  .0. e. _V
67 66 a1i 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> .0. e. _V )
68 24 63 65 67 suppssr 
 |-  ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. ( A \ ( f supp .0. ) ) ) -> ( f ` n ) = .0. )
69 68 adantlr 
 |-  ( ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. ( I \ ( f supp .0. ) ) ) /\ n e. ( A \ ( f supp .0. ) ) ) -> ( f ` n ) = .0. )
70 62 69 syldan 
 |-  ( ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. ( I \ ( f supp .0. ) ) ) /\ n e. A ) -> ( f ` n ) = .0. )
71 70 ifeq1da 
 |-  ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. ( I \ ( f supp .0. ) ) ) -> if ( n e. A , ( f ` n ) , .0. ) = if ( n e. A , .0. , .0. ) )
72 ifid 
 |-  if ( n e. A , .0. , .0. ) = .0.
73 71 72 eqtrdi 
 |-  ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. ( I \ ( f supp .0. ) ) ) -> if ( n e. A , ( f ` n ) , .0. ) = .0. )
74 73 39 suppss2 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) supp .0. ) C_ ( f supp .0. ) )
75 fsuppsssupp 
 |-  ( ( ( ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) e. _V /\ Fun ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) ) /\ ( f finSupp .0. /\ ( ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) supp .0. ) C_ ( f supp .0. ) ) ) -> ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) finSupp .0. )
76 55 57 58 74 75 syl22anc 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) finSupp .0. )
77 2 34 40 53 76 dprdwd 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) e. W )
78 2 34 40 77 23 dprdff 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) : I --> ( Base ` G ) )
79 2 34 40 77 33 dprdfcntz 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ran ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) C_ ( ( Cntz ` G ) ` ran ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) ) )
80 eldifn 
 |-  ( n e. ( I \ A ) -> -. n e. A )
81 80 adantl 
 |-  ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. ( I \ A ) ) -> -. n e. A )
82 81 iffalsed 
 |-  ( ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) /\ n e. ( I \ A ) ) -> if ( n e. A , ( f ` n ) , .0. ) = .0. )
83 82 39 suppss2 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) supp .0. ) C_ A )
84 23 1 33 37 39 78 79 83 76 gsumzres 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( G gsum ( ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) |` A ) ) = ( G gsum ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) ) )
85 17 32 84 3eqtrd 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( G gsum F ) = ( G gsum ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) ) )
86 6 ad2antrr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> F e. W )
87 1 2 34 40 86 77 dprdf11 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( ( G gsum F ) = ( G gsum ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) ) <-> F = ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) ) )
88 85 87 mpbid 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> F = ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) )
89 88 fveq1d 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( F ` X ) = ( ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) ` X ) )
90 eldifi 
 |-  ( X e. ( I \ A ) -> X e. I )
91 90 ad2antlr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> X e. I )
92 eleq1 
 |-  ( n = X -> ( n e. A <-> X e. A ) )
93 fveq2 
 |-  ( n = X -> ( f ` n ) = ( f ` X ) )
94 92 93 ifbieq1d 
 |-  ( n = X -> if ( n e. A , ( f ` n ) , .0. ) = if ( X e. A , ( f ` X ) , .0. ) )
95 eqid 
 |-  ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) = ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) )
96 fvex 
 |-  ( f ` n ) e. _V
97 96 66 ifex 
 |-  if ( n e. A , ( f ` n ) , .0. ) e. _V
98 94 95 97 fvmpt3i 
 |-  ( X e. I -> ( ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) ` X ) = if ( X e. A , ( f ` X ) , .0. ) )
99 91 98 syl 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( ( n e. I |-> if ( n e. A , ( f ` n ) , .0. ) ) ` X ) = if ( X e. A , ( f ` X ) , .0. ) )
100 eldifn 
 |-  ( X e. ( I \ A ) -> -. X e. A )
101 100 ad2antlr 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> -. X e. A )
102 101 iffalsed 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> if ( X e. A , ( f ` X ) , .0. ) = .0. )
103 89 99 102 3eqtrd 
 |-  ( ( ( ph /\ X e. ( I \ A ) ) /\ ( f e. { h e. X_ i e. A ( ( S |` A ) ` i ) | h finSupp .0. } /\ ( G gsum F ) = ( G gsum f ) ) ) -> ( F ` X ) = .0. )
104 16 103 rexlimddv 
 |-  ( ( ph /\ X e. ( I \ A ) ) -> ( F ` X ) = .0. )