MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsumzoppg Structured version   Visualization version   GIF version

Theorem gsumzoppg 19962
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.)
Hypotheses
Ref Expression
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
Ref Expression
gsumzoppg (𝜑 → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹))

Proof of Theorem gsumzoppg
Dummy variables 𝑓 𝑘 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumzoppg.g . . . . . . . 8 (𝜑𝐺 ∈ Mnd)
2 gsumzoppg.o . . . . . . . . 9 𝑂 = (oppg𝐺)
32oppgmnd 19373 . . . . . . . 8 (𝐺 ∈ Mnd → 𝑂 ∈ Mnd)
41, 3syl 17 . . . . . . 7 (𝜑𝑂 ∈ Mnd)
5 gsumzoppg.a . . . . . . 7 (𝜑𝐴𝑉)
6 gsumzoppg.0 . . . . . . . . 9 0 = (0g𝐺)
72, 6oppgid 19375 . . . . . . . 8 0 = (0g𝑂)
87gsumz 18849 . . . . . . 7 ((𝑂 ∈ Mnd ∧ 𝐴𝑉) → (𝑂 Σg (𝑘𝐴0 )) = 0 )
94, 5, 8syl2anc 584 . . . . . 6 (𝜑 → (𝑂 Σg (𝑘𝐴0 )) = 0 )
106gsumz 18849 . . . . . . 7 ((𝐺 ∈ Mnd ∧ 𝐴𝑉) → (𝐺 Σg (𝑘𝐴0 )) = 0 )
111, 5, 10syl2anc 584 . . . . . 6 (𝜑 → (𝐺 Σg (𝑘𝐴0 )) = 0 )
129, 11eqtr4d 2780 . . . . 5 (𝜑 → (𝑂 Σg (𝑘𝐴0 )) = (𝐺 Σg (𝑘𝐴0 )))
1312adantr 480 . . . 4 ((𝜑 ∧ (𝐹 “ (V ∖ { 0 })) = ∅) → (𝑂 Σg (𝑘𝐴0 )) = (𝐺 Σg (𝑘𝐴0 )))
14 gsumzoppg.f . . . . . 6 (𝜑𝐹:𝐴𝐵)
156fvexi 6920 . . . . . . 7 0 ∈ V
1615a1i 11 . . . . . 6 (𝜑0 ∈ V)
17 ssid 4006 . . . . . . 7 (𝐹 “ (V ∖ { 0 })) ⊆ (𝐹 “ (V ∖ { 0 }))
1814, 5fexd 7247 . . . . . . . . 9 (𝜑𝐹 ∈ V)
19 suppimacnv 8199 . . . . . . . . 9 ((𝐹 ∈ V ∧ 0 ∈ V) → (𝐹 supp 0 ) = (𝐹 “ (V ∖ { 0 })))
2018, 15, 19sylancl 586 . . . . . . . 8 (𝜑 → (𝐹 supp 0 ) = (𝐹 “ (V ∖ { 0 })))
2120sseq1d 4015 . . . . . . 7 (𝜑 → ((𝐹 supp 0 ) ⊆ (𝐹 “ (V ∖ { 0 })) ↔ (𝐹 “ (V ∖ { 0 })) ⊆ (𝐹 “ (V ∖ { 0 }))))
2217, 21mpbiri 258 . . . . . 6 (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 “ (V ∖ { 0 })))
2314, 5, 16, 22gsumcllem 19926 . . . . 5 ((𝜑 ∧ (𝐹 “ (V ∖ { 0 })) = ∅) → 𝐹 = (𝑘𝐴0 ))
2423oveq2d 7447 . . . 4 ((𝜑 ∧ (𝐹 “ (V ∖ { 0 })) = ∅) → (𝑂 Σg 𝐹) = (𝑂 Σg (𝑘𝐴0 )))
2523oveq2d 7447 . . . 4 ((𝜑 ∧ (𝐹 “ (V ∖ { 0 })) = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑘𝐴0 )))
2613, 24, 253eqtr4d 2787 . . 3 ((𝜑 ∧ (𝐹 “ (V ∖ { 0 })) = ∅) → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹))
2726ex 412 . 2 (𝜑 → ((𝐹 “ (V ∖ { 0 })) = ∅ → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹)))
28 simprl 771 . . . . . . . 8 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ)
29 nnuz 12921 . . . . . . . 8 ℕ = (ℤ‘1)
3028, 29eleqtrdi 2851 . . . . . . 7 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (♯‘(𝐹 “ (V ∖ { 0 }))) ∈ (ℤ‘1))
3114adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → 𝐹:𝐴𝐵)
32 ffn 6736 . . . . . . . . . . . 12 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
33 dffn4 6826 . . . . . . . . . . . 12 (𝐹 Fn 𝐴𝐹:𝐴onto→ran 𝐹)
3432, 33sylib 218 . . . . . . . . . . 11 (𝐹:𝐴𝐵𝐹:𝐴onto→ran 𝐹)
35 fof 6820 . . . . . . . . . . 11 (𝐹:𝐴onto→ran 𝐹𝐹:𝐴⟶ran 𝐹)
3631, 34, 353syl 18 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → 𝐹:𝐴⟶ran 𝐹)
371adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → 𝐺 ∈ Mnd)
38 gsumzoppg.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝐺)
3938submacs 18840 . . . . . . . . . . . 12 (𝐺 ∈ Mnd → (SubMnd‘𝐺) ∈ (ACS‘𝐵))
40 acsmre 17695 . . . . . . . . . . . 12 ((SubMnd‘𝐺) ∈ (ACS‘𝐵) → (SubMnd‘𝐺) ∈ (Moore‘𝐵))
4137, 39, 403syl 18 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (SubMnd‘𝐺) ∈ (Moore‘𝐵))
42 eqid 2737 . . . . . . . . . . 11 (mrCls‘(SubMnd‘𝐺)) = (mrCls‘(SubMnd‘𝐺))
4331frnd 6744 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → ran 𝐹𝐵)
4441, 42, 43mrcssidd 17668 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
4536, 44fssd 6753 . . . . . . . . 9 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → 𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
46 f1of1 6847 . . . . . . . . . . . 12 (𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })) → 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1→(𝐹 “ (V ∖ { 0 })))
4746ad2antll 729 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1→(𝐹 “ (V ∖ { 0 })))
48 cnvimass 6100 . . . . . . . . . . . 12 (𝐹 “ (V ∖ { 0 })) ⊆ dom 𝐹
4948, 31fssdm 6755 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (𝐹 “ (V ∖ { 0 })) ⊆ 𝐴)
50 f1ss 6809 . . . . . . . . . . 11 ((𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1→(𝐹 “ (V ∖ { 0 })) ∧ (𝐹 “ (V ∖ { 0 })) ⊆ 𝐴) → 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1𝐴)
5147, 49, 50syl2anc 584 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1𝐴)
52 f1f 6804 . . . . . . . . . 10 (𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1𝐴𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))⟶𝐴)
5351, 52syl 17 . . . . . . . . 9 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))⟶𝐴)
54 fco 6760 . . . . . . . . 9 ((𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))⟶𝐴) → (𝐹𝑓):(1...(♯‘(𝐹 “ (V ∖ { 0 }))))⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
5545, 53, 54syl2anc 584 . . . . . . . 8 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (𝐹𝑓):(1...(♯‘(𝐹 “ (V ∖ { 0 }))))⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
5655ffvelcdmda 7104 . . . . . . 7 (((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈ (1...(♯‘(𝐹 “ (V ∖ { 0 }))))) → ((𝐹𝑓)‘𝑥) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
5742mrccl 17654 . . . . . . . . . 10 (((SubMnd‘𝐺) ∈ (Moore‘𝐵) ∧ ran 𝐹𝐵) → ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺))
5841, 43, 57syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺))
592oppgsubm 19381 . . . . . . . . 9 (SubMnd‘𝐺) = (SubMnd‘𝑂)
6058, 59eleqtrdi 2851 . . . . . . . 8 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝑂))
61 eqid 2737 . . . . . . . . . 10 (+g𝑂) = (+g𝑂)
6261submcl 18825 . . . . . . . . 9 ((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝑂) ∧ 𝑥 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g𝑂)𝑦) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
63623expb 1121 . . . . . . . 8 ((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝑂) ∧ (𝑥 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) → (𝑥(+g𝑂)𝑦) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
6460, 63sylan 580 . . . . . . 7 (((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) ∧ (𝑥 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) → (𝑥(+g𝑂)𝑦) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
65 eqid 2737 . . . . . . . . . 10 (+g𝐺) = (+g𝐺)
6665, 2, 61oppgplus 19367 . . . . . . . . 9 (𝑥(+g𝑂)𝑦) = (𝑦(+g𝐺)𝑥)
67 gsumzoppg.c . . . . . . . . . . . . . 14 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
6867adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
69 gsumzoppg.z . . . . . . . . . . . . . 14 𝑍 = (Cntz‘𝐺)
70 eqid 2737 . . . . . . . . . . . . . 14 (𝐺s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) = (𝐺s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
7169, 42, 70cntzspan 19862 . . . . . . . . . . . . 13 ((𝐺 ∈ Mnd ∧ ran 𝐹 ⊆ (𝑍‘ran 𝐹)) → (𝐺s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd)
7237, 68, 71syl2anc 584 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (𝐺s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd)
7370, 69submcmn2 19857 . . . . . . . . . . . . 13 (((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺) → ((𝐺s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd ↔ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))))
7458, 73syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → ((𝐺s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd ↔ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))))
7572, 74mpbid 232 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)))
7675sselda 3983 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → 𝑥 ∈ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)))
7765, 69cntzi 19347 . . . . . . . . . 10 ((𝑥 ∈ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g𝐺)𝑦) = (𝑦(+g𝐺)𝑥))
7876, 77sylan 580 . . . . . . . . 9 ((((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g𝐺)𝑦) = (𝑦(+g𝐺)𝑥))
7966, 78eqtr4id 2796 . . . . . . . 8 ((((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g𝑂)𝑦) = (𝑥(+g𝐺)𝑦))
8079anasss 466 . . . . . . 7 (((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) ∧ (𝑥 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) → (𝑥(+g𝑂)𝑦) = (𝑥(+g𝐺)𝑦))
8130, 56, 64, 80seqfeq4 14092 . . . . . 6 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (seq1((+g𝑂), (𝐹𝑓))‘(♯‘(𝐹 “ (V ∖ { 0 })))) = (seq1((+g𝐺), (𝐹𝑓))‘(♯‘(𝐹 “ (V ∖ { 0 })))))
822, 38oppgbas 19370 . . . . . . 7 𝐵 = (Base‘𝑂)
83 eqid 2737 . . . . . . 7 (Cntz‘𝑂) = (Cntz‘𝑂)
8437, 3syl 17 . . . . . . 7 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → 𝑂 ∈ Mnd)
855adantr 480 . . . . . . 7 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → 𝐴𝑉)
862, 69oppgcntz 19383 . . . . . . . 8 (𝑍‘ran 𝐹) = ((Cntz‘𝑂)‘ran 𝐹)
8768, 86sseqtrdi 4024 . . . . . . 7 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆ ((Cntz‘𝑂)‘ran 𝐹))
88 suppssdm 8202 . . . . . . . . . . 11 (𝐹 supp 0 ) ⊆ dom 𝐹
8920, 88eqsstrrdi 4029 . . . . . . . . . 10 (𝜑 → (𝐹 “ (V ∖ { 0 })) ⊆ dom 𝐹)
9014, 89fssdmd 6754 . . . . . . . . 9 (𝜑 → (𝐹 “ (V ∖ { 0 })) ⊆ 𝐴)
9190adantr 480 . . . . . . . 8 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (𝐹 “ (V ∖ { 0 })) ⊆ 𝐴)
9247, 91, 50syl2anc 584 . . . . . . 7 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1𝐴)
9321adantr 480 . . . . . . . . 9 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → ((𝐹 supp 0 ) ⊆ (𝐹 “ (V ∖ { 0 })) ↔ (𝐹 “ (V ∖ { 0 })) ⊆ (𝐹 “ (V ∖ { 0 }))))
9417, 93mpbiri 258 . . . . . . . 8 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ (𝐹 “ (V ∖ { 0 })))
95 f1ofo 6855 . . . . . . . . . . 11 (𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })) → 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–onto→(𝐹 “ (V ∖ { 0 })))
96 forn 6823 . . . . . . . . . . 11 (𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–onto→(𝐹 “ (V ∖ { 0 })) → ran 𝑓 = (𝐹 “ (V ∖ { 0 })))
9795, 96syl 17 . . . . . . . . . 10 (𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })) → ran 𝑓 = (𝐹 “ (V ∖ { 0 })))
9897sseq2d 4016 . . . . . . . . 9 (𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ (𝐹 “ (V ∖ { 0 }))))
9998ad2antll 729 . . . . . . . 8 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ (𝐹 “ (V ∖ { 0 }))))
10094, 99mpbird 257 . . . . . . 7 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ ran 𝑓)
101 eqid 2737 . . . . . . 7 ((𝐹𝑓) supp 0 ) = ((𝐹𝑓) supp 0 )
10282, 7, 61, 83, 84, 85, 31, 87, 28, 92, 100, 101gsumval3 19925 . . . . . 6 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (𝑂 Σg 𝐹) = (seq1((+g𝑂), (𝐹𝑓))‘(♯‘(𝐹 “ (V ∖ { 0 })))))
10322adantr 480 . . . . . . . 8 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ (𝐹 “ (V ∖ { 0 })))
104103, 99mpbird 257 . . . . . . 7 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ ran 𝑓)
10538, 6, 65, 69, 37, 85, 31, 68, 28, 92, 104, 101gsumval3 19925 . . . . . 6 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (𝐺 Σg 𝐹) = (seq1((+g𝐺), (𝐹𝑓))‘(♯‘(𝐹 “ (V ∖ { 0 })))))
10681, 102, 1053eqtr4d 2787 . . . . 5 ((𝜑 ∧ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))) → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹))
107106expr 456 . . . 4 ((𝜑 ∧ (♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ) → (𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })) → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹)))
108107exlimdv 1933 . . 3 ((𝜑 ∧ (♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })) → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹)))
109108expimpd 453 . 2 (𝜑 → (((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 }))) → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹)))
110 gsumzoppg.n . . . . 5 (𝜑𝐹 finSupp 0 )
111110fsuppimpd 9409 . . . 4 (𝜑 → (𝐹 supp 0 ) ∈ Fin)
11220, 111eqeltrrd 2842 . . 3 (𝜑 → (𝐹 “ (V ∖ { 0 })) ∈ Fin)
113 fz1f1o 15746 . . 3 ((𝐹 “ (V ∖ { 0 })) ∈ Fin → ((𝐹 “ (V ∖ { 0 })) = ∅ ∨ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))))
114112, 113syl 17 . 2 (𝜑 → ((𝐹 “ (V ∖ { 0 })) = ∅ ∨ ((♯‘(𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘(𝐹 “ (V ∖ { 0 }))))–1-1-onto→(𝐹 “ (V ∖ { 0 })))))
11527, 109, 114mpjaod 861 1 (𝜑 → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wex 1779  wcel 2108  Vcvv 3480  cdif 3948  wss 3951  c0 4333  {csn 4626   class class class wbr 5143  cmpt 5225  ccnv 5684  dom cdm 5685  ran crn 5686  cima 5688  ccom 5689   Fn wfn 6556  wf 6557  1-1wf1 6558  ontowfo 6559  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431   supp csupp 8185  Fincfn 8985   finSupp cfsupp 9401  1c1 11156  cn 12266  cuz 12878  ...cfz 13547  seqcseq 14042  chash 14369  Basecbs 17247  s cress 17274  +gcplusg 17297  0gc0g 17484   Σg cgsu 17485  Moorecmre 17625  mrClscmrc 17626  ACScacs 17628  Mndcmnd 18747  SubMndcsubmnd 18795  Cntzccntz 19333  oppgcoppg 19363  CMndccmn 19798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-tpos 8251  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-fzo 13695  df-seq 14043  df-hash 14370  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-0g 17486  df-gsum 17487  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-cntz 19335  df-oppg 19364  df-cmn 19800
This theorem is referenced by:  gsumzinv  19963
  Copyright terms: Public domain W3C validator