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𝐺 )
dmdprdsplitlem.w 𝑊 = { X 𝑖𝐼 ( 𝑆𝑖 ) ∣ finSupp 0 }
dmdprdsplitlem.1 ( 𝜑𝐺 dom DProd 𝑆 )
dmdprdsplitlem.2 ( 𝜑 → dom 𝑆 = 𝐼 )
dmdprdsplitlem.3 ( 𝜑𝐴𝐼 )
dmdprdsplitlem.4 ( 𝜑𝐹𝑊 )
dmdprdsplitlem.5 ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd ( 𝑆𝐴 ) ) )
Assertion dmdprdsplitlem ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) → ( 𝐹𝑋 ) = 0 )

Proof

Step Hyp Ref Expression
1 dmdprdsplitlem.0 0 = ( 0g𝐺 )
2 dmdprdsplitlem.w 𝑊 = { X 𝑖𝐼 ( 𝑆𝑖 ) ∣ finSupp 0 }
3 dmdprdsplitlem.1 ( 𝜑𝐺 dom DProd 𝑆 )
4 dmdprdsplitlem.2 ( 𝜑 → dom 𝑆 = 𝐼 )
5 dmdprdsplitlem.3 ( 𝜑𝐴𝐼 )
6 dmdprdsplitlem.4 ( 𝜑𝐹𝑊 )
7 dmdprdsplitlem.5 ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd ( 𝑆𝐴 ) ) )
8 3 4 dprdf2 ( 𝜑𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
9 8 5 fssresd ( 𝜑 → ( 𝑆𝐴 ) : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) )
10 fdm ( ( 𝑆𝐴 ) : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) → dom ( 𝑆𝐴 ) = 𝐴 )
11 eqid { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } = { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 }
12 1 11 eldprd ( dom ( 𝑆𝐴 ) = 𝐴 → ( ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd ( 𝑆𝐴 ) ) ↔ ( 𝐺 dom DProd ( 𝑆𝐴 ) ∧ ∃ 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) )
13 9 10 12 3syl ( 𝜑 → ( ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd ( 𝑆𝐴 ) ) ↔ ( 𝐺 dom DProd ( 𝑆𝐴 ) ∧ ∃ 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) )
14 7 13 mpbid ( 𝜑 → ( 𝐺 dom DProd ( 𝑆𝐴 ) ∧ ∃ 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) )
15 14 simprd ( 𝜑 → ∃ 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) )
16 15 adantr ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) → ∃ 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) )
17 simprr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) )
18 14 simpld ( 𝜑𝐺 dom DProd ( 𝑆𝐴 ) )
19 18 ad2antrr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝐺 dom DProd ( 𝑆𝐴 ) )
20 9 10 syl ( 𝜑 → dom ( 𝑆𝐴 ) = 𝐴 )
21 20 ad2antrr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → dom ( 𝑆𝐴 ) = 𝐴 )
22 simprl ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } )
23 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
24 11 19 21 22 23 dprdff ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝑓 : 𝐴 ⟶ ( Base ‘ 𝐺 ) )
25 24 feqmptd ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝑓 = ( 𝑛𝐴 ↦ ( 𝑓𝑛 ) ) )
26 5 ad2antrr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝐴𝐼 )
27 26 resmptd ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ↾ 𝐴 ) = ( 𝑛𝐴 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) )
28 iftrue ( 𝑛𝐴 → if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) = ( 𝑓𝑛 ) )
29 28 mpteq2ia ( 𝑛𝐴 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) = ( 𝑛𝐴 ↦ ( 𝑓𝑛 ) )
30 27 29 eqtrdi ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ↾ 𝐴 ) = ( 𝑛𝐴 ↦ ( 𝑓𝑛 ) ) )
31 25 30 eqtr4d ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝑓 = ( ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ↾ 𝐴 ) )
32 31 oveq2d ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝐺 Σg 𝑓 ) = ( 𝐺 Σg ( ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ↾ 𝐴 ) ) )
33 eqid ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
34 3 ad2antrr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝐺 dom DProd 𝑆 )
35 dprdgrp ( 𝐺 dom DProd 𝑆𝐺 ∈ Grp )
36 grpmnd ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
37 34 35 36 3syl ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝐺 ∈ Mnd )
38 3 4 dprddomcld ( 𝜑𝐼 ∈ V )
39 38 ad2antrr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝐼 ∈ V )
40 4 ad2antrr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → dom 𝑆 = 𝐼 )
41 19 adantr ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛𝐼 ) → 𝐺 dom DProd ( 𝑆𝐴 ) )
42 21 adantr ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛𝐼 ) → dom ( 𝑆𝐴 ) = 𝐴 )
43 simplrl ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛𝐼 ) → 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } )
44 11 41 42 43 dprdfcl ( ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛𝐼 ) ∧ 𝑛𝐴 ) → ( 𝑓𝑛 ) ∈ ( ( 𝑆𝐴 ) ‘ 𝑛 ) )
45 fvres ( 𝑛𝐴 → ( ( 𝑆𝐴 ) ‘ 𝑛 ) = ( 𝑆𝑛 ) )
46 45 adantl ( ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛𝐼 ) ∧ 𝑛𝐴 ) → ( ( 𝑆𝐴 ) ‘ 𝑛 ) = ( 𝑆𝑛 ) )
47 44 46 eleqtrd ( ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛𝐼 ) ∧ 𝑛𝐴 ) → ( 𝑓𝑛 ) ∈ ( 𝑆𝑛 ) )
48 8 ad2antrr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
49 48 ffvelrnda ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛𝐼 ) → ( 𝑆𝑛 ) ∈ ( SubGrp ‘ 𝐺 ) )
50 1 subg0cl ( ( 𝑆𝑛 ) ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ ( 𝑆𝑛 ) )
51 49 50 syl ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛𝐼 ) → 0 ∈ ( 𝑆𝑛 ) )
52 51 adantr ( ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛𝐼 ) ∧ ¬ 𝑛𝐴 ) → 0 ∈ ( 𝑆𝑛 ) )
53 47 52 ifclda ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛𝐼 ) → if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ∈ ( 𝑆𝑛 ) )
54 38 mptexd ( 𝜑 → ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ∈ V )
55 54 ad2antrr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ∈ V )
56 funmpt Fun ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) )
57 56 a1i ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → Fun ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) )
58 11 19 21 22 dprdffsupp ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝑓 finSupp 0 )
59 simpr ( ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) ∧ 𝑛𝐴 ) → 𝑛𝐴 )
60 eldifn ( 𝑛 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) → ¬ 𝑛 ∈ ( 𝑓 supp 0 ) )
61 60 ad2antlr ( ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) ∧ 𝑛𝐴 ) → ¬ 𝑛 ∈ ( 𝑓 supp 0 ) )
62 59 61 eldifd ( ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) ∧ 𝑛𝐴 ) → 𝑛 ∈ ( 𝐴 ∖ ( 𝑓 supp 0 ) ) )
63 ssidd ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑓 supp 0 ) ⊆ ( 𝑓 supp 0 ) )
64 38 5 ssexd ( 𝜑𝐴 ∈ V )
65 64 ad2antrr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝐴 ∈ V )
66 1 fvexi 0 ∈ V
67 66 a1i ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 0 ∈ V )
68 24 63 65 67 suppssr ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛 ∈ ( 𝐴 ∖ ( 𝑓 supp 0 ) ) ) → ( 𝑓𝑛 ) = 0 )
69 68 adantlr ( ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) ∧ 𝑛 ∈ ( 𝐴 ∖ ( 𝑓 supp 0 ) ) ) → ( 𝑓𝑛 ) = 0 )
70 62 69 syldan ( ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) ∧ 𝑛𝐴 ) → ( 𝑓𝑛 ) = 0 )
71 70 ifeq1da ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) = if ( 𝑛𝐴 , 0 , 0 ) )
72 ifid if ( 𝑛𝐴 , 0 , 0 ) = 0
73 71 72 eqtrdi ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) = 0 )
74 73 39 suppss2 ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) supp 0 ) ⊆ ( 𝑓 supp 0 ) )
75 fsuppsssupp ( ( ( ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ∈ V ∧ Fun ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) supp 0 ) ⊆ ( 𝑓 supp 0 ) ) ) → ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) finSupp 0 )
76 55 57 58 74 75 syl22anc ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) finSupp 0 )
77 2 34 40 53 76 dprdwd ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ∈ 𝑊 )
78 2 34 40 77 23 dprdff ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
79 2 34 40 77 33 dprdfcntz ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ran ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ) )
80 eldifn ( 𝑛 ∈ ( 𝐼𝐴 ) → ¬ 𝑛𝐴 )
81 80 adantl ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛 ∈ ( 𝐼𝐴 ) ) → ¬ 𝑛𝐴 )
82 81 iffalsed ( ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑛 ∈ ( 𝐼𝐴 ) ) → if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) = 0 )
83 82 39 suppss2 ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) supp 0 ) ⊆ 𝐴 )
84 23 1 33 37 39 78 79 83 76 gsumzres ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝐺 Σg ( ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ↾ 𝐴 ) ) = ( 𝐺 Σg ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ) )
85 17 32 84 3eqtrd ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ) )
86 6 ad2antrr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝐹𝑊 )
87 1 2 34 40 86 77 dprdf11 ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ) ↔ 𝐹 = ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ) )
88 85 87 mpbid ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝐹 = ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) )
89 88 fveq1d ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝐹𝑋 ) = ( ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ‘ 𝑋 ) )
90 eldifi ( 𝑋 ∈ ( 𝐼𝐴 ) → 𝑋𝐼 )
91 90 ad2antlr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → 𝑋𝐼 )
92 eleq1 ( 𝑛 = 𝑋 → ( 𝑛𝐴𝑋𝐴 ) )
93 fveq2 ( 𝑛 = 𝑋 → ( 𝑓𝑛 ) = ( 𝑓𝑋 ) )
94 92 93 ifbieq1d ( 𝑛 = 𝑋 → if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) = if ( 𝑋𝐴 , ( 𝑓𝑋 ) , 0 ) )
95 eqid ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) = ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) )
96 fvex ( 𝑓𝑛 ) ∈ V
97 96 66 ifex if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ∈ V
98 94 95 97 fvmpt3i ( 𝑋𝐼 → ( ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ‘ 𝑋 ) = if ( 𝑋𝐴 , ( 𝑓𝑋 ) , 0 ) )
99 91 98 syl ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( ( 𝑛𝐼 ↦ if ( 𝑛𝐴 , ( 𝑓𝑛 ) , 0 ) ) ‘ 𝑋 ) = if ( 𝑋𝐴 , ( 𝑓𝑋 ) , 0 ) )
100 eldifn ( 𝑋 ∈ ( 𝐼𝐴 ) → ¬ 𝑋𝐴 )
101 100 ad2antlr ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ¬ 𝑋𝐴 )
102 101 iffalsed ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → if ( 𝑋𝐴 , ( 𝑓𝑋 ) , 0 ) = 0 )
103 89 99 102 3eqtrd ( ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) ∧ ( 𝑓 ∈ { X 𝑖𝐴 ( ( 𝑆𝐴 ) ‘ 𝑖 ) ∣ finSupp 0 } ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝐹𝑋 ) = 0 )
104 16 103 rexlimddv ( ( 𝜑𝑋 ∈ ( 𝐼𝐴 ) ) → ( 𝐹𝑋 ) = 0 )