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

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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝐺 Σ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 ) ) )