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 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐼 ∖ 𝐴 ) ) ∧ ( 𝑓 ∈ { ℎ ∈ 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 )