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