| Step | Hyp | Ref
| Expression |
| 1 | | gsumzoppg.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Mnd) |
| 2 | | gsumzoppg.o |
. . . . . . . . 9
⊢ 𝑂 =
(oppg‘𝐺) |
| 3 | 2 | oppgmnd 19373 |
. . . . . . . 8
⊢ (𝐺 ∈ Mnd → 𝑂 ∈ Mnd) |
| 4 | 1, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑂 ∈ Mnd) |
| 5 | | gsumzoppg.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 6 | | gsumzoppg.0 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐺) |
| 7 | 2, 6 | oppgid 19375 |
. . . . . . . 8
⊢ 0 =
(0g‘𝑂) |
| 8 | 7 | gsumz 18849 |
. . . . . . 7
⊢ ((𝑂 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝑂 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
| 9 | 4, 5, 8 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑂 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
| 10 | 6 | gsumz 18849 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
| 11 | 1, 5, 10 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
| 12 | 9, 11 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → (𝑂 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
| 13 | 12 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
(𝑂
Σg (𝑘 ∈ 𝐴 ↦ 0 )) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
| 14 | | gsumzoppg.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 15 | 6 | fvexi 6920 |
. . . . . . 7
⊢ 0 ∈
V |
| 16 | 15 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈ V) |
| 17 | | ssid 4006 |
. . . . . . 7
⊢ (◡𝐹 “ (V ∖ { 0 })) ⊆ (◡𝐹 “ (V ∖ { 0 })) |
| 18 | 14, 5 | fexd 7247 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ V) |
| 19 | | suppimacnv 8199 |
. . . . . . . . 9
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ (𝐹 supp 0 ) = (◡𝐹 “ (V ∖ { 0 }))) |
| 20 | 18, 15, 19 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 supp 0 ) = (◡𝐹 “ (V ∖ { 0 }))) |
| 21 | 20 | sseq1d 4015 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 })) ↔ (◡𝐹 “ (V ∖ { 0 })) ⊆ (◡𝐹 “ (V ∖ { 0 })))) |
| 22 | 17, 21 | mpbiri 258 |
. . . . . 6
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 }))) |
| 23 | 14, 5, 16, 22 | gsumcllem 19926 |
. . . . 5
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
𝐹 = (𝑘 ∈ 𝐴 ↦ 0 )) |
| 24 | 23 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
(𝑂
Σg 𝐹) = (𝑂 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
| 25 | 23 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
(𝐺
Σg 𝐹) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
| 26 | 13, 24, 25 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
(𝑂
Σg 𝐹) = (𝐺 Σg 𝐹)) |
| 27 | 26 | ex 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) |
| 30 | 28, 29 | eleqtrdi 2851 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
(♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈
(ℤ≥‘1)) |
| 31 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐹:𝐴⟶𝐵) |
| 32 | | ffn 6736 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
| 33 | | dffn4 6826 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
| 34 | 32, 33 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→ran 𝐹) |
| 35 | | fof 6820 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴–onto→ran 𝐹 → 𝐹:𝐴⟶ran 𝐹) |
| 36 | 31, 34, 35 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐹:𝐴⟶ran 𝐹) |
| 37 | 1 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐺 ∈ Mnd) |
| 38 | | gsumzoppg.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝐺) |
| 39 | 38 | submacs 18840 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ Mnd →
(SubMnd‘𝐺) ∈
(ACS‘𝐵)) |
| 40 | | acsmre 17695 |
. . . . . . . . . . . 12
⊢
((SubMnd‘𝐺)
∈ (ACS‘𝐵) →
(SubMnd‘𝐺) ∈
(Moore‘𝐵)) |
| 41 | 37, 39, 40 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
(SubMnd‘𝐺) ∈
(Moore‘𝐵)) |
| 42 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(mrCls‘(SubMnd‘𝐺)) = (mrCls‘(SubMnd‘𝐺)) |
| 43 | 31 | frnd 6744 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆ 𝐵) |
| 44 | 41, 42, 43 | mrcssidd 17668 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 45 | 36, 44 | fssd 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
}))) |
| 47 | 46 | ad2antll 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 𝐹 |
| 49 | 48, 31 | fssdm 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→𝐴) |
| 51 | 47, 49, 50 | syl2anc 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 }))))⟶𝐴) |
| 53 | 51, 52 | syl 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 𝐹)) |
| 55 | 45, 53, 54 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐹 ∘ 𝑓):(1...(♯‘(◡𝐹 “ (V ∖ { 0
}))))⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 56 | 55 | ffvelcdmda 7104 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈
(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))) → ((𝐹 ∘ 𝑓)‘𝑥) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 57 | 42 | mrccl 17654 |
. . . . . . . . . 10
⊢
(((SubMnd‘𝐺)
∈ (Moore‘𝐵)
∧ ran 𝐹 ⊆ 𝐵) →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺)) |
| 58 | 41, 43, 57 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺)) |
| 59 | 2 | oppgsubm 19381 |
. . . . . . . . 9
⊢
(SubMnd‘𝐺) =
(SubMnd‘𝑂) |
| 60 | 58, 59 | eleqtrdi 2851 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝑂)) |
| 61 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝑂) = (+g‘𝑂) |
| 62 | 61 | submcl 18825 |
. . . . . . . . 9
⊢
((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝑂) ∧ 𝑥 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g‘𝑂)𝑦) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 63 | 62 | 3expb 1121 |
. . . . . . . 8
⊢
((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝑂) ∧ (𝑥 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) → (𝑥(+g‘𝑂)𝑦) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 64 | 60, 63 | sylan 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‘𝐺) |
| 66 | 65, 2, 61 | oppgplus 19367 |
. . . . . . . . 9
⊢ (𝑥(+g‘𝑂)𝑦) = (𝑦(+g‘𝐺)𝑥) |
| 67 | | gsumzoppg.c |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
| 68 | 67 | adantr 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 𝐹)) |
| 71 | 69, 42, 70 | cntzspan 19862 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Mnd ∧ ran 𝐹 ⊆ (𝑍‘ran 𝐹)) → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd) |
| 72 | 37, 68, 71 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd) |
| 73 | 70, 69 | submcmn2 19857 |
. . . . . . . . . . . . 13
⊢
(((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺) → ((𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd ↔
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)))) |
| 74 | 58, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ((𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd ↔
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)))) |
| 75 | 72, 74 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) |
| 76 | 75 | sselda 3983 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → 𝑥 ∈ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) |
| 77 | 65, 69 | cntzi 19347 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
| 78 | 76, 77 | sylan 580 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
| 79 | 66, 78 | eqtr4id 2796 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g‘𝑂)𝑦) = (𝑥(+g‘𝐺)𝑦)) |
| 80 | 79 | anasss 466 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ (𝑥 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) → (𝑥(+g‘𝑂)𝑦) = (𝑥(+g‘𝐺)𝑦)) |
| 81 | 30, 56, 64, 80 | seqfeq4 14092 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
(seq1((+g‘𝑂), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 })))) =
(seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))) |
| 82 | 2, 38 | oppgbas 19370 |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑂) |
| 83 | | eqid 2737 |
. . . . . . 7
⊢
(Cntz‘𝑂) =
(Cntz‘𝑂) |
| 84 | 37, 3 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝑂 ∈ Mnd) |
| 85 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐴 ∈ 𝑉) |
| 86 | 2, 69 | oppgcntz 19383 |
. . . . . . . 8
⊢ (𝑍‘ran 𝐹) = ((Cntz‘𝑂)‘ran 𝐹) |
| 87 | 68, 86 | sseqtrdi 4024 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆ ((Cntz‘𝑂)‘ran 𝐹)) |
| 88 | | suppssdm 8202 |
. . . . . . . . . . 11
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
| 89 | 20, 88 | eqsstrrdi 4029 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) ⊆ dom 𝐹) |
| 90 | 14, 89 | fssdmd 6754 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) ⊆ 𝐴) |
| 91 | 90 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (◡𝐹 “ (V ∖ { 0 })) ⊆ 𝐴) |
| 92 | 47, 91, 50 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1→𝐴) |
| 93 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ((𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 })) ↔ (◡𝐹 “ (V ∖ { 0 })) ⊆ (◡𝐹 “ (V ∖ { 0 })))) |
| 94 | 17, 93 | mpbiri 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 }))) |
| 97 | 95, 96 | syl 17 |
. . . . . . . . . 10
⊢ (𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → ran 𝑓 = (◡𝐹 “ (V ∖ { 0 }))) |
| 98 | 97 | sseq2d 4016 |
. . . . . . . . 9
⊢ (𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 })))) |
| 99 | 98 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 })))) |
| 100 | 94, 99 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ ran 𝑓) |
| 101 | | eqid 2737 |
. . . . . . 7
⊢ ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 ) |
| 102 | 82, 7, 61, 83, 84, 85, 31, 87, 28, 92, 100, 101 | gsumval3 19925 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝑂 Σg
𝐹) =
(seq1((+g‘𝑂), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))) |
| 103 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 }))) |
| 104 | 103, 99 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ ran 𝑓) |
| 105 | 38, 6, 65, 69, 37, 85, 31, 68, 28, 92, 104, 101 | gsumval3 19925 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐺 Σg
𝐹) =
(seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))) |
| 106 | 81, 102, 105 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝑂 Σg
𝐹) = (𝐺 Σg 𝐹)) |
| 107 | 106 | expr 456 |
. . . 4
⊢ ((𝜑 ∧ (♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ)
→ (𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → (𝑂 Σg
𝐹) = (𝐺 Σg 𝐹))) |
| 108 | 107 | exlimdv 1933 |
. . 3
⊢ ((𝜑 ∧ (♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ)
→ (∃𝑓 𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → (𝑂 Σg
𝐹) = (𝐺 Σg 𝐹))) |
| 109 | 108 | expimpd 453 |
. 2
⊢ (𝜑 → (((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 }))) → (𝑂 Σg
𝐹) = (𝐺 Σg 𝐹))) |
| 110 | | gsumzoppg.n |
. . . . 5
⊢ (𝜑 → 𝐹 finSupp 0 ) |
| 111 | 110 | fsuppimpd 9409 |
. . . 4
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
| 112 | 20, 111 | eqeltrrd 2842 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) ∈
Fin) |
| 113 | | fz1f1o 15746 |
. . 3
⊢ ((◡𝐹 “ (V ∖ { 0 })) ∈ Fin →
((◡𝐹 “ (V ∖ { 0 })) = ∅ ∨
((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 }))))) |
| 114 | 112, 113 | syl 17 |
. 2
⊢ (𝜑 → ((◡𝐹 “ (V ∖ { 0 })) = ∅ ∨
((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 }))))) |
| 115 | 27, 109, 114 | mpjaod 861 |
1
⊢ (𝜑 → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹)) |