Step | Hyp | Ref
| Expression |
1 | | gsumzoppg.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Mnd) |
2 | | gsumzoppg.o |
. . . . . . . . 9
⊢ 𝑂 =
(oppg‘𝐺) |
3 | 2 | oppgmnd 19135 |
. . . . . . . 8
⊢ (𝐺 ∈ Mnd → 𝑂 ∈ Mnd) |
4 | 1, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑂 ∈ Mnd) |
5 | | gsumzoppg.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
6 | | gsumzoppg.0 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐺) |
7 | 2, 6 | oppgid 19137 |
. . . . . . . 8
⊢ 0 =
(0g‘𝑂) |
8 | 7 | gsumz 18646 |
. . . . . . 7
⊢ ((𝑂 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝑂 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
9 | 4, 5, 8 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑂 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
10 | 6 | gsumz 18646 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
11 | 1, 5, 10 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
12 | 9, 11 | eqtr4d 2779 |
. . . . 5
⊢ (𝜑 → (𝑂 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
13 | 12 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
(𝑂
Σg (𝑘 ∈ 𝐴 ↦ 0 )) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
14 | | gsumzoppg.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
15 | 6 | fvexi 6856 |
. . . . . . 7
⊢ 0 ∈
V |
16 | 15 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈ V) |
17 | | ssid 3966 |
. . . . . . 7
⊢ (◡𝐹 “ (V ∖ { 0 })) ⊆ (◡𝐹 “ (V ∖ { 0 })) |
18 | 14, 5 | fexd 7177 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ V) |
19 | | suppimacnv 8105 |
. . . . . . . . 9
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ (𝐹 supp 0 ) = (◡𝐹 “ (V ∖ { 0 }))) |
20 | 18, 15, 19 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 supp 0 ) = (◡𝐹 “ (V ∖ { 0 }))) |
21 | 20 | sseq1d 3975 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 })) ↔ (◡𝐹 “ (V ∖ { 0 })) ⊆ (◡𝐹 “ (V ∖ { 0 })))) |
22 | 17, 21 | mpbiri 257 |
. . . . . 6
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 }))) |
23 | 14, 5, 16, 22 | gsumcllem 19685 |
. . . . 5
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
𝐹 = (𝑘 ∈ 𝐴 ↦ 0 )) |
24 | 23 | oveq2d 7373 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
(𝑂
Σg 𝐹) = (𝑂 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
25 | 23 | oveq2d 7373 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
(𝐺
Σg 𝐹) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
26 | 13, 24, 25 | 3eqtr4d 2786 |
. . 3
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
(𝑂
Σg 𝐹) = (𝐺 Σg 𝐹)) |
27 | 26 | ex 413 |
. 2
⊢ (𝜑 → ((◡𝐹 “ (V ∖ { 0 })) = ∅ →
(𝑂
Σg 𝐹) = (𝐺 Σg 𝐹))) |
28 | | simprl 769 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
(♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈
ℕ) |
29 | | nnuz 12806 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
30 | 28, 29 | eleqtrdi 2848 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
(♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈
(ℤ≥‘1)) |
31 | 14 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐹:𝐴⟶𝐵) |
32 | | ffn 6668 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
33 | | dffn4 6762 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
34 | 32, 33 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→ran 𝐹) |
35 | | fof 6756 |
. . . . . . . . . . 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 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐺 ∈ Mnd) |
38 | | gsumzoppg.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝐺) |
39 | 38 | submacs 18637 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ Mnd →
(SubMnd‘𝐺) ∈
(ACS‘𝐵)) |
40 | | acsmre 17532 |
. . . . . . . . . . . 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 2736 |
. . . . . . . . . . 11
⊢
(mrCls‘(SubMnd‘𝐺)) = (mrCls‘(SubMnd‘𝐺)) |
43 | 31 | frnd 6676 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆ 𝐵) |
44 | 41, 42, 43 | mrcssidd 17505 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
45 | 36, 44 | fssd 6686 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
46 | | f1of1 6783 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → 𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1→(◡𝐹 “ (V ∖ { 0
}))) |
47 | 46 | ad2antll 727 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1→(◡𝐹 “ (V ∖ { 0
}))) |
48 | | cnvimass 6033 |
. . . . . . . . . . . 12
⊢ (◡𝐹 “ (V ∖ { 0 })) ⊆ dom 𝐹 |
49 | 48, 31 | fssdm 6688 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (◡𝐹 “ (V ∖ { 0 })) ⊆ 𝐴) |
50 | | f1ss 6744 |
. . . . . . . . . . 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 6738 |
. . . . . . . . . 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 6692 |
. . . . . . . . 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 7035 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈
(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))) → ((𝐹 ∘ 𝑓)‘𝑥) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
57 | 42 | mrccl 17491 |
. . . . . . . . . 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 19143 |
. . . . . . . . 9
⊢
(SubMnd‘𝐺) =
(SubMnd‘𝑂) |
60 | 58, 59 | eleqtrdi 2848 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝑂)) |
61 | | eqid 2736 |
. . . . . . . . . 10
⊢
(+g‘𝑂) = (+g‘𝑂) |
62 | 61 | submcl 18623 |
. . . . . . . . 9
⊢
((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝑂) ∧ 𝑥 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g‘𝑂)𝑦) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
63 | 62 | 3expb 1120 |
. . . . . . . 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 2736 |
. . . . . . . . . 10
⊢
(+g‘𝐺) = (+g‘𝐺) |
66 | 65, 2, 61 | oppgplus 19127 |
. . . . . . . . 9
⊢ (𝑥(+g‘𝑂)𝑦) = (𝑦(+g‘𝐺)𝑥) |
67 | | gsumzoppg.c |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
68 | 67 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
69 | | gsumzoppg.z |
. . . . . . . . . . . . . 14
⊢ 𝑍 = (Cntz‘𝐺) |
70 | | eqid 2736 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) = (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
71 | 69, 42, 70 | cntzspan 19622 |
. . . . . . . . . . . . 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 19617 |
. . . . . . . . . . . . 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 231 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) |
76 | 75 | sselda 3944 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → 𝑥 ∈ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) |
77 | 65, 69 | cntzi 19109 |
. . . . . . . . . 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 2795 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g‘𝑂)𝑦) = (𝑥(+g‘𝐺)𝑦)) |
80 | 79 | anasss 467 |
. . . . . . 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 13957 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
(seq1((+g‘𝑂), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 })))) =
(seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))) |
82 | 2, 38 | oppgbas 19130 |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑂) |
83 | | eqid 2736 |
. . . . . . 7
⊢
(Cntz‘𝑂) =
(Cntz‘𝑂) |
84 | 37, 3 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝑂 ∈ Mnd) |
85 | 5 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐴 ∈ 𝑉) |
86 | 2, 69 | oppgcntz 19145 |
. . . . . . . 8
⊢ (𝑍‘ran 𝐹) = ((Cntz‘𝑂)‘ran 𝐹) |
87 | 68, 86 | sseqtrdi 3994 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆ ((Cntz‘𝑂)‘ran 𝐹)) |
88 | | suppssdm 8108 |
. . . . . . . . . . 11
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
89 | 20, 88 | eqsstrrdi 3999 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) ⊆ dom 𝐹) |
90 | 14, 89 | fssdmd 6687 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) ⊆ 𝐴) |
91 | 90 | adantr 481 |
. . . . . . . 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 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ((𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 })) ↔ (◡𝐹 “ (V ∖ { 0 })) ⊆ (◡𝐹 “ (V ∖ { 0 })))) |
94 | 17, 93 | mpbiri 257 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 }))) |
95 | | f1ofo 6791 |
. . . . . . . . . . 11
⊢ (𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → 𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–onto→(◡𝐹 “ (V ∖ { 0 }))) |
96 | | forn 6759 |
. . . . . . . . . . 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 3976 |
. . . . . . . . 9
⊢ (𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 })))) |
99 | 98 | ad2antll 727 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 })))) |
100 | 94, 99 | mpbird 256 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ ran 𝑓) |
101 | | eqid 2736 |
. . . . . . 7
⊢ ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 ) |
102 | 82, 7, 61, 83, 84, 85, 31, 87, 28, 92, 100, 101 | gsumval3 19684 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝑂 Σg
𝐹) =
(seq1((+g‘𝑂), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))) |
103 | 22 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 }))) |
104 | 103, 99 | mpbird 256 |
. . . . . . 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 19684 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐺 Σg
𝐹) =
(seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))) |
106 | 81, 102, 105 | 3eqtr4d 2786 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝑂 Σg
𝐹) = (𝐺 Σg 𝐹)) |
107 | 106 | expr 457 |
. . . 4
⊢ ((𝜑 ∧ (♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ)
→ (𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → (𝑂 Σg
𝐹) = (𝐺 Σg 𝐹))) |
108 | 107 | exlimdv 1936 |
. . 3
⊢ ((𝜑 ∧ (♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ)
→ (∃𝑓 𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → (𝑂 Σg
𝐹) = (𝐺 Σg 𝐹))) |
109 | 108 | expimpd 454 |
. 2
⊢ (𝜑 → (((♯‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 }))) → (𝑂 Σg
𝐹) = (𝐺 Σg 𝐹))) |
110 | | gsumzoppg.n |
. . . . 5
⊢ (𝜑 → 𝐹 finSupp 0 ) |
111 | 110 | fsuppimpd 9312 |
. . . 4
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
112 | 20, 111 | eqeltrrd 2839 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) ∈
Fin) |
113 | | fz1f1o 15595 |
. . 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 858 |
1
⊢ (𝜑 → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹)) |