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 ffvelrnda
 |-  ( ( ( ( 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. )