Step | Hyp | Ref
| Expression |
1 | | gsumzoppg.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Mnd) |
2 | | gsumzoppg.o |
. . . . . . . . 9
⊢ 𝑂 =
(oppg‘𝐺) |
3 | 2 | oppgmnd 17607 |
. . . . . . . 8
⊢ (𝐺 ∈ Mnd → 𝑂 ∈ Mnd) |
4 | 1, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑂 ∈ Mnd) |
5 | | gsumzoppg.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
6 | | gsumzoppg.0 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐺) |
7 | 2, 6 | oppgid 17609 |
. . . . . . . 8
⊢ 0 =
(0g‘𝑂) |
8 | 7 | gsumz 17197 |
. . . . . . 7
⊢ ((𝑂 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝑂 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
9 | 4, 5, 8 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝑂 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
10 | 6 | gsumz 17197 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
11 | 1, 5, 10 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
12 | 9, 11 | eqtr4d 2647 |
. . . . 5
⊢ (𝜑 → (𝑂 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
13 | 12 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
(𝑂
Σg (𝑘 ∈ 𝐴 ↦ 0 )) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
14 | | gsumzoppg.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
15 | | fvex 6113 |
. . . . . . . 8
⊢
(0g‘𝐺) ∈ V |
16 | 6, 15 | eqeltri 2684 |
. . . . . . 7
⊢ 0 ∈
V |
17 | 16 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈ V) |
18 | | ssid 3587 |
. . . . . . 7
⊢ (◡𝐹 “ (V ∖ { 0 })) ⊆ (◡𝐹 “ (V ∖ { 0 })) |
19 | | fex 6394 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
20 | 14, 5, 19 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ V) |
21 | | suppimacnv 7193 |
. . . . . . . . 9
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ (𝐹 supp 0 ) = (◡𝐹 “ (V ∖ { 0 }))) |
22 | 20, 16, 21 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 supp 0 ) = (◡𝐹 “ (V ∖ { 0 }))) |
23 | 22 | sseq1d 3595 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 })) ↔ (◡𝐹 “ (V ∖ { 0 })) ⊆ (◡𝐹 “ (V ∖ { 0 })))) |
24 | 18, 23 | mpbiri 247 |
. . . . . 6
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 }))) |
25 | 14, 5, 17, 24 | gsumcllem 18132 |
. . . . 5
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
𝐹 = (𝑘 ∈ 𝐴 ↦ 0 )) |
26 | 25 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
(𝑂
Σg 𝐹) = (𝑂 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
27 | 25 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
(𝐺
Σg 𝐹) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
28 | 13, 26, 27 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ (◡𝐹 “ (V ∖ { 0 })) = ∅) →
(𝑂
Σg 𝐹) = (𝐺 Σg 𝐹)) |
29 | 28 | ex 449 |
. 2
⊢ (𝜑 → ((◡𝐹 “ (V ∖ { 0 })) = ∅ →
(𝑂
Σg 𝐹) = (𝐺 Σg 𝐹))) |
30 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
(#‘(◡𝐹 “ (V ∖ { 0 }))) ∈
ℕ) |
31 | | nnuz 11599 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
32 | 30, 31 | syl6eleq 2698 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
(#‘(◡𝐹 “ (V ∖ { 0 }))) ∈
(ℤ≥‘1)) |
33 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐹:𝐴⟶𝐵) |
34 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
35 | | dffn4 6034 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
36 | 34, 35 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→ran 𝐹) |
37 | | fof 6028 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴–onto→ran 𝐹 → 𝐹:𝐴⟶ran 𝐹) |
38 | 33, 36, 37 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐹:𝐴⟶ran 𝐹) |
39 | 1 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐺 ∈ Mnd) |
40 | | gsumzoppg.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝐺) |
41 | 40 | submacs 17188 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ Mnd →
(SubMnd‘𝐺) ∈
(ACS‘𝐵)) |
42 | | acsmre 16136 |
. . . . . . . . . . . 12
⊢
((SubMnd‘𝐺)
∈ (ACS‘𝐵) →
(SubMnd‘𝐺) ∈
(Moore‘𝐵)) |
43 | 39, 41, 42 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
(SubMnd‘𝐺) ∈
(Moore‘𝐵)) |
44 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(mrCls‘(SubMnd‘𝐺)) = (mrCls‘(SubMnd‘𝐺)) |
45 | | frn 5966 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) |
46 | 33, 45 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆ 𝐵) |
47 | 43, 44, 46 | mrcssidd 16108 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
48 | 38, 47 | fssd 5970 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
49 | | f1of1 6049 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1→(◡𝐹 “ (V ∖ { 0
}))) |
50 | 49 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1→(◡𝐹 “ (V ∖ { 0
}))) |
51 | | cnvimass 5404 |
. . . . . . . . . . . 12
⊢ (◡𝐹 “ (V ∖ { 0 })) ⊆ dom 𝐹 |
52 | | fdm 5964 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
53 | 33, 52 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → dom 𝐹 = 𝐴) |
54 | 51, 53 | syl5sseq 3616 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (◡𝐹 “ (V ∖ { 0 })) ⊆ 𝐴) |
55 | | f1ss 6019 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1→(◡𝐹 “ (V ∖ { 0 })) ∧
(◡𝐹 “ (V ∖ { 0 })) ⊆ 𝐴) → 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1→𝐴) |
56 | 50, 54, 55 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1→𝐴) |
57 | | f1f 6014 |
. . . . . . . . . 10
⊢ (𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1→𝐴 → 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))⟶𝐴) |
58 | 56, 57 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))⟶𝐴) |
59 | | fco 5971 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))⟶𝐴) → (𝐹 ∘ 𝑓):(1...(#‘(◡𝐹 “ (V ∖ { 0
}))))⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
60 | 48, 58, 59 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐹 ∘ 𝑓):(1...(#‘(◡𝐹 “ (V ∖ { 0
}))))⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
61 | 60 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈ (1...(#‘(◡𝐹 “ (V ∖ { 0 }))))) → ((𝐹 ∘ 𝑓)‘𝑥) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
62 | 44 | mrccl 16094 |
. . . . . . . . . 10
⊢
(((SubMnd‘𝐺)
∈ (Moore‘𝐵)
∧ ran 𝐹 ⊆ 𝐵) →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺)) |
63 | 43, 46, 62 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺)) |
64 | 2 | oppgsubm 17615 |
. . . . . . . . 9
⊢
(SubMnd‘𝐺) =
(SubMnd‘𝑂) |
65 | 63, 64 | syl6eleq 2698 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝑂)) |
66 | | eqid 2610 |
. . . . . . . . . 10
⊢
(+g‘𝑂) = (+g‘𝑂) |
67 | 66 | submcl 17176 |
. . . . . . . . 9
⊢
((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝑂) ∧ 𝑥 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g‘𝑂)𝑦) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
68 | 67 | 3expb 1258 |
. . . . . . . 8
⊢
((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝑂) ∧ (𝑥 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) → (𝑥(+g‘𝑂)𝑦) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
69 | 65, 68 | sylan 487 |
. . . . . . 7
⊢ (((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ (𝑥 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) → (𝑥(+g‘𝑂)𝑦) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
70 | | gsumzoppg.c |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
72 | | gsumzoppg.z |
. . . . . . . . . . . . . 14
⊢ 𝑍 = (Cntz‘𝐺) |
73 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) = (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
74 | 72, 44, 73 | cntzspan 18070 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Mnd ∧ ran 𝐹 ⊆ (𝑍‘ran 𝐹)) → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd) |
75 | 39, 71, 74 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd) |
76 | 73, 72 | submcmn2 18067 |
. . . . . . . . . . . . 13
⊢
(((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺) → ((𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd ↔
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)))) |
77 | 63, 76 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ((𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd ↔
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)))) |
78 | 75, 77 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) |
79 | 78 | sselda 3568 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → 𝑥 ∈ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) |
80 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(+g‘𝐺) = (+g‘𝐺) |
81 | 80, 72 | cntzi 17585 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
82 | 79, 81 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
83 | 80, 2, 66 | oppgplus 17602 |
. . . . . . . . 9
⊢ (𝑥(+g‘𝑂)𝑦) = (𝑦(+g‘𝐺)𝑥) |
84 | 82, 83 | syl6reqr 2663 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ 𝑥 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → (𝑥(+g‘𝑂)𝑦) = (𝑥(+g‘𝐺)𝑦)) |
85 | 84 | anasss 677 |
. . . . . . 7
⊢ (((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) ∧ (𝑥 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∧ 𝑦 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) → (𝑥(+g‘𝑂)𝑦) = (𝑥(+g‘𝐺)𝑦)) |
86 | 32, 61, 69, 85 | seqfeq4 12712 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) →
(seq1((+g‘𝑂), (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 })))) =
(seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 }))))) |
87 | 2, 40 | oppgbas 17604 |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑂) |
88 | | eqid 2610 |
. . . . . . 7
⊢
(Cntz‘𝑂) =
(Cntz‘𝑂) |
89 | 39, 3 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝑂 ∈ Mnd) |
90 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝐴 ∈ 𝑉) |
91 | 2, 72 | oppgcntz 17617 |
. . . . . . . 8
⊢ (𝑍‘ran 𝐹) = ((Cntz‘𝑂)‘ran 𝐹) |
92 | 71, 91 | syl6sseq 3614 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ran 𝐹 ⊆ ((Cntz‘𝑂)‘ran 𝐹)) |
93 | | suppssdm 7195 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
94 | 22, 93 | syl6eqssr 3619 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) ⊆ dom 𝐹) |
95 | 94 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐹 = 𝐴 ∧ 𝜑) → (◡𝐹 “ (V ∖ { 0 })) ⊆ dom 𝐹) |
96 | | eqcom 2617 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝐹 = 𝐴 ↔ 𝐴 = dom 𝐹) |
97 | 96 | biimpi 205 |
. . . . . . . . . . . . . 14
⊢ (dom
𝐹 = 𝐴 → 𝐴 = dom 𝐹) |
98 | 97 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐹 = 𝐴 ∧ 𝜑) → 𝐴 = dom 𝐹) |
99 | 95, 98 | sseqtr4d 3605 |
. . . . . . . . . . . 12
⊢ ((dom
𝐹 = 𝐴 ∧ 𝜑) → (◡𝐹 “ (V ∖ { 0 })) ⊆ 𝐴) |
100 | 99 | ex 449 |
. . . . . . . . . . 11
⊢ (dom
𝐹 = 𝐴 → (𝜑 → (◡𝐹 “ (V ∖ { 0 })) ⊆ 𝐴)) |
101 | 52, 100 | syl 17 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶𝐵 → (𝜑 → (◡𝐹 “ (V ∖ { 0 })) ⊆ 𝐴)) |
102 | 14, 101 | mpcom 37 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) ⊆ 𝐴) |
103 | 102 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (◡𝐹 “ (V ∖ { 0 })) ⊆ 𝐴) |
104 | 50, 103, 55 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1→𝐴) |
105 | 23 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ((𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 })) ↔ (◡𝐹 “ (V ∖ { 0 })) ⊆ (◡𝐹 “ (V ∖ { 0 })))) |
106 | 18, 105 | mpbiri 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 }))) |
107 | | f1ofo 6057 |
. . . . . . . . . . 11
⊢ (𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–onto→(◡𝐹 “ (V ∖ { 0 }))) |
108 | | forn 6031 |
. . . . . . . . . . 11
⊢ (𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–onto→(◡𝐹 “ (V ∖ { 0 })) → ran 𝑓 = (◡𝐹 “ (V ∖ { 0 }))) |
109 | 107, 108 | syl 17 |
. . . . . . . . . 10
⊢ (𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → ran 𝑓 = (◡𝐹 “ (V ∖ { 0 }))) |
110 | 109 | sseq2d 3596 |
. . . . . . . . 9
⊢ (𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 })))) |
111 | 110 | ad2antll 761 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 })))) |
112 | 106, 111 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ ran 𝑓) |
113 | | eqid 2610 |
. . . . . . 7
⊢ ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 ) |
114 | 87, 7, 66, 88, 89, 90, 33, 92, 30, 104, 112, 113 | gsumval3 18131 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝑂 Σg
𝐹) =
(seq1((+g‘𝑂), (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 }))))) |
115 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ (◡𝐹 “ (V ∖ { 0 }))) |
116 | 115, 111 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐹 supp 0 ) ⊆ ran 𝑓) |
117 | 40, 6, 80, 72, 39, 90, 33, 71, 30, 104, 116, 113 | gsumval3 18131 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝐺 Σg
𝐹) =
(seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 }))))) |
118 | 86, 114, 117 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ ((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })))) → (𝑂 Σg
𝐹) = (𝐺 Σg 𝐹)) |
119 | 118 | expr 641 |
. . . 4
⊢ ((𝜑 ∧ (#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ)
→ (𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → (𝑂 Σg
𝐹) = (𝐺 Σg 𝐹))) |
120 | 119 | exlimdv 1848 |
. . 3
⊢ ((𝜑 ∧ (#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ)
→ (∃𝑓 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) → (𝑂 Σg
𝐹) = (𝐺 Σg 𝐹))) |
121 | 120 | expimpd 627 |
. 2
⊢ (𝜑 → (((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 }))) → (𝑂 Σg
𝐹) = (𝐺 Σg 𝐹))) |
122 | | gsumzoppg.n |
. . . . 5
⊢ (𝜑 → 𝐹 finSupp 0 ) |
123 | 122 | fsuppimpd 8165 |
. . . 4
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
124 | 22, 123 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) ∈
Fin) |
125 | | fz1f1o 14288 |
. . 3
⊢ ((◡𝐹 “ (V ∖ { 0 })) ∈ Fin →
((◡𝐹 “ (V ∖ { 0 })) = ∅ ∨
((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 }))))) |
126 | 124, 125 | syl 17 |
. 2
⊢ (𝜑 → ((◡𝐹 “ (V ∖ { 0 })) = ∅ ∨
((#‘(◡𝐹 “ (V ∖ { 0 }))) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 }))))) |
127 | 29, 121, 126 | mpjaod 395 |
1
⊢ (𝜑 → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹)) |