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𝐺 )
eldprdi.w 𝑊 = { X 𝑖𝐼 ( 𝑆𝑖 ) ∣ finSupp 0 }
eldprdi.1 ( 𝜑𝐺 dom DProd 𝑆 )
eldprdi.2 ( 𝜑 → dom 𝑆 = 𝐼 )
eldprdi.3 ( 𝜑𝐹𝑊 )
Assertion dprdfeq0 ( 𝜑 → ( ( 𝐺 Σg 𝐹 ) = 0𝐹 = ( 𝑥𝐼0 ) ) )

Proof

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