Metamath Proof Explorer

Theorem gsumzoppg

Description: The opposite of a group sum is the same as the original. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsumzoppg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumzoppg.0 ⊢ 0 = ( 0g ‘ 𝐺 )
gsumzoppg.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
gsumzoppg.o ⊢ 𝑂 = ( oppg ‘ 𝐺 )
gsumzoppg.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsumzoppg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumzoppg.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumzoppg.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
gsumzoppg.n ⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion gsumzoppg ( 𝜑 → ( 𝑂 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 ) )

Proof

Step Hyp Ref Expression
1 gsumzoppg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumzoppg.0 ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumzoppg.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
4 gsumzoppg.o ⊢ 𝑂 = ( oppg ‘ 𝐺 )
5 gsumzoppg.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
6 gsumzoppg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7 gsumzoppg.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8 gsumzoppg.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
9 gsumzoppg.n ⊢ ( 𝜑 → 𝐹 finSupp 0 )
10 4 oppgmnd ⊢ ( 𝐺 ∈ Mnd → 𝑂 ∈ Mnd )
11 5 10 syl ⊢ ( 𝜑 → 𝑂 ∈ Mnd )
12 4 2 oppgid ⊢ 0 = ( 0g ‘ 𝑂 )
13 12 gsumz ⊢ ( ( 𝑂 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝑂 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
14 11 6 13 syl2anc ⊢ ( 𝜑 → ( 𝑂 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
15 2 gsumz ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
16 5 6 15 syl2anc ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
17 14 16 eqtr4d ⊢ ( 𝜑 → ( 𝑂 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) )
18 17 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝑂 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) )
19 2 fvexi ⊢ 0 ∈ V
20 19 a1i ⊢ ( 𝜑 → 0 ∈ V )
21 ssid ⊢ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) )
22 fex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
23 7 6 22 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ V )
24 suppimacnv ⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
25 23 19 24 sylancl ⊢ ( 𝜑 → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
26 25 sseq1d ⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ↔ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) )
27 21 26 mpbiri ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
28 7 6 20 27 gsumcllem ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 0 ) )
29 28 oveq2d ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝑂 Σg 𝐹 ) = ( 𝑂 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) )
30 28 oveq2d ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) )
31 18 29 30 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝑂 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 ) )
32 31 ex ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ → ( 𝑂 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 ) ) )
33 simprl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ )
34 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
35 33 34 eleqtrdi ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ( ℤ≥ ‘ 1 ) )
36 7 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
37 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
38 dffn4 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 )
39 37 38 sylib ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 –onto→ ran 𝐹 )
40 fof ⊢ ( 𝐹 : 𝐴 –onto→ ran 𝐹 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
41 36 39 40 3syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝐹 : 𝐴 ⟶ ran 𝐹 )
42 5 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝐺 ∈ Mnd )
43 1 submacs ⊢ ( 𝐺 ∈ Mnd → ( SubMnd ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
44 acsmre ⊢ ( ( SubMnd ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) → ( SubMnd ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
45 42 43 44 3syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( SubMnd ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
46 eqid ⊢ ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) = ( mrCls ‘ ( SubMnd ‘ 𝐺 ) )
47 36 frnd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ran 𝐹 ⊆ 𝐵 )
48 45 46 47 mrcssidd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ran 𝐹 ⊆ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) )
49 41 48 fssd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝐹 : 𝐴 ⟶ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) )
50 f1of1 ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
51 50 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
52 cnvimass ⊢ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ dom 𝐹
53 52 36 fssdm ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ 𝐴 )
54 f1ss ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ 𝐴 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ 𝐴 )
55 51 53 54 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ 𝐴 )
56 f1f ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ⟶ 𝐴 )
57 55 56 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ⟶ 𝐴 )
58 fco ⊢ ( ( 𝐹 : 𝐴 ⟶ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ⟶ 𝐴 ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ⟶ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) )
59 49 57 58 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ⟶ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) )
60 59 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) )
61 46 mrccl ⊢ ( ( ( SubMnd ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ ran 𝐹 ⊆ 𝐵 ) → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ∈ ( SubMnd ‘ 𝐺 ) )
62 45 47 61 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ∈ ( SubMnd ‘ 𝐺 ) )
63 4 oppgsubm ⊢ ( SubMnd ‘ 𝐺 ) = ( SubMnd ‘ 𝑂 )
64 62 63 eleqtrdi ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ∈ ( SubMnd ‘ 𝑂 ) )
65 eqid ⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 )
66 65 submcl ⊢ ( ( ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ∈ ( SubMnd ‘ 𝑂 ) ∧ 𝑥 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ∧ 𝑦 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) → ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) )
67 66 3expb ⊢ ( ( ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ∈ ( SubMnd ‘ 𝑂 ) ∧ ( 𝑥 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ∧ 𝑦 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) ) → ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) )
68 64 67 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ ( 𝑥 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ∧ 𝑦 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) ) → ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) )
69 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
70 69 4 65 oppgplus ⊢ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 )
71 8 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
72 eqid ⊢ ( 𝐺 ↾s ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) = ( 𝐺 ↾s ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) )
73 3 46 72 cntzspan ⊢ ( ( 𝐺 ∈ Mnd ∧ ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) ) → ( 𝐺 ↾s ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) ∈ CMnd )
74 42 71 73 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐺 ↾s ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) ∈ CMnd )
75 72 3 submcmn2 ⊢ ( ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ∈ ( SubMnd ‘ 𝐺 ) → ( ( 𝐺 ↾s ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) ∈ CMnd ↔ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ⊆ ( 𝑍 ‘ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) ) )
76 62 75 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ( 𝐺 ↾s ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) ∈ CMnd ↔ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ⊆ ( 𝑍 ‘ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) ) )
77 74 76 mpbid ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ⊆ ( 𝑍 ‘ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) )
78 77 sselda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ 𝑥 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) → 𝑥 ∈ ( 𝑍 ‘ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) )
79 69 3 cntzi ⊢ ( ( 𝑥 ∈ ( 𝑍 ‘ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) ∧ 𝑦 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
80 78 79 sylan ⊢ ( ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ 𝑥 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) ∧ 𝑦 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
81 70 80 eqtr4id ⊢ ( ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ 𝑥 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) ∧ 𝑦 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) → ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
82 81 anasss ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ ( 𝑥 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ∧ 𝑦 ∈ ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ ran 𝐹 ) ) ) → ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
83 35 60 68 82 seqfeq4 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( seq 1 ( ( +g ‘ 𝑂 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) )
84 4 1 oppgbas ⊢ 𝐵 = ( Base ‘ 𝑂 )
85 eqid ⊢ ( Cntz ‘ 𝑂 ) = ( Cntz ‘ 𝑂 )
86 42 10 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝑂 ∈ Mnd )
87 6 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝐴 ∈ 𝑉 )
88 4 3 oppgcntz ⊢ ( 𝑍 ‘ ran 𝐹 ) = ( ( Cntz ‘ 𝑂 ) ‘ ran 𝐹 )
89 71 88 sseqtrdi ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ran 𝐹 ⊆ ( ( Cntz ‘ 𝑂 ) ‘ ran 𝐹 ) )
90 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
91 25 90 eqsstrrdi ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ dom 𝐹 )
92 7 91 fssdmd ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ 𝐴 )
93 92 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ 𝐴 )
94 51 93 54 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ 𝐴 )
95 26 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ↔ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) )
96 21 95 mpbiri ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
97 f1ofo ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
98 forn ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → ran 𝑓 = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
99 97 98 syl ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → ran 𝑓 = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
100 99 sseq2d ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → ( ( 𝐹 supp 0 ) ⊆ ran 𝑓 ↔ ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) )
101 100 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ( 𝐹 supp 0 ) ⊆ ran 𝑓 ↔ ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) )
102 96 101 mpbird ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐹 supp 0 ) ⊆ ran 𝑓 )
103 eqid ⊢ ( ( 𝐹 ∘ 𝑓 ) supp 0 ) = ( ( 𝐹 ∘ 𝑓 ) supp 0 )
104 84 12 65 85 86 87 36 89 33 94 102 103 gsumval3 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝑂 Σg 𝐹 ) = ( seq 1 ( ( +g ‘ 𝑂 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) )
105 27 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
106 105 101 mpbird ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐹 supp 0 ) ⊆ ran 𝑓 )
107 1 2 69 3 42 87 36 71 33 94 106 103 gsumval3 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) )
108 83 104 107 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝑂 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 ) )
109 108 expr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → ( 𝑂 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 ) ) )
110 109 exlimdv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → ( 𝑂 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 ) ) )
111 110 expimpd ⊢ ( 𝜑 → ( ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) → ( 𝑂 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 ) ) )
112 9 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
113 25 112 eqeltrrd ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ∈ Fin )
114 fz1f1o ⊢ ( ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ∈ Fin → ( ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ∨ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) )
115 113 114 syl ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ∨ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) )
116 32 111 115 mpjaod ⊢ ( 𝜑 → ( 𝑂 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 ) )