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 = ( 0_g ‘ 𝐺 )
	gsumzoppg.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
	gsumzoppg.o	⊢ 𝑂 = ( opp_g ‘ 𝐺 )
	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 = ( 0_g ‘ 𝐺 )
3		gsumzoppg.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
4		gsumzoppg.o	⊢ 𝑂 = ( opp_g ‘ 𝐺 )
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 = ( 0_g ‘ 𝑂 )
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 𝐹 ) )

Metamath Proof Explorer

Theorem gsumzoppg

Proof