Step | Hyp | Ref
| Expression |
1 | | monmat2matmon.b |
. . 3
⊢ 𝐵 = (Base‘𝐶) |
2 | | eqid 2738 |
. . 3
⊢
(0g‘𝐶) = (0g‘𝐶) |
3 | | crngring 19428 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
4 | 3 | anim2i 620 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
5 | | monmat2matmon.p |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) |
6 | | monmat2matmon.c |
. . . . . 6
⊢ 𝐶 = (𝑁 Mat 𝑃) |
7 | 5, 6 | pmatring 21443 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
8 | | ringcmn 19453 |
. . . . 5
⊢ (𝐶 ∈ Ring → 𝐶 ∈ CMnd) |
9 | 4, 7, 8 | 3syl 18 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ CMnd) |
10 | 9 | adantr 484 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ 𝐶 ∈
CMnd) |
11 | | monmat2matmon.a |
. . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) |
12 | 11 | matring 21194 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
13 | 3, 12 | sylan2 596 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring) |
14 | | monmat2matmon.q |
. . . . . 6
⊢ 𝑄 = (Poly1‘𝐴) |
15 | 14 | ply1ring 21023 |
. . . . 5
⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring) |
16 | | ringmnd 19426 |
. . . . 5
⊢ (𝑄 ∈ Ring → 𝑄 ∈ Mnd) |
17 | 13, 15, 16 | 3syl 18 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑄 ∈ Mnd) |
18 | 17 | adantr 484 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ 𝑄 ∈
Mnd) |
19 | | nn0ex 11982 |
. . . 4
⊢
ℕ0 ∈ V |
20 | 19 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ ℕ0 ∈ V) |
21 | | monmat2matmon.m1 |
. . . . . . 7
⊢ ∗ = (
·𝑠 ‘𝑄) |
22 | | monmat2matmon.e1 |
. . . . . . 7
⊢ ↑ =
(.g‘(mulGrp‘𝑄)) |
23 | | monmat2matmon.x |
. . . . . . 7
⊢ 𝑋 = (var1‘𝐴) |
24 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝑄) =
(Base‘𝑄) |
25 | | monmat2matmon.i |
. . . . . . 7
⊢ 𝐼 = (𝑁 pMatToMatPoly 𝑅) |
26 | 5, 6, 1, 21, 22, 23, 11, 14, 24, 25 | pm2mpghm 21567 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐼 ∈ (𝐶 GrpHom 𝑄)) |
27 | 3, 26 | sylan2 596 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐼 ∈ (𝐶 GrpHom 𝑄)) |
28 | 27 | adantr 484 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ 𝐼 ∈ (𝐶 GrpHom 𝑄)) |
29 | | ghmmhm 18486 |
. . . 4
⊢ (𝐼 ∈ (𝐶 GrpHom 𝑄) → 𝐼 ∈ (𝐶 MndHom 𝑄)) |
30 | 28, 29 | syl 17 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ 𝐼 ∈ (𝐶 MndHom 𝑄)) |
31 | 4 | adantr 484 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (𝑁 ∈ Fin ∧
𝑅 ∈
Ring)) |
32 | 31 | adantr 484 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
33 | | elmapi 8459 |
. . . . . . 7
⊢ (𝑀 ∈ (𝐾 ↑m ℕ0)
→ 𝑀:ℕ0⟶𝐾) |
34 | 33 | adantr 484 |
. . . . . 6
⊢ ((𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴))
→ 𝑀:ℕ0⟶𝐾) |
35 | 34 | adantl 485 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ 𝑀:ℕ0⟶𝐾) |
36 | 35 | ffvelrnda 6861 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → (𝑀‘𝑛) ∈ 𝐾) |
37 | | simpr 488 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℕ0) |
38 | | monmat2matmon.k |
. . . . 5
⊢ 𝐾 = (Base‘𝐴) |
39 | | monmat2matmon.t |
. . . . 5
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
40 | | monmat2matmon.m2 |
. . . . 5
⊢ · = (
·𝑠 ‘𝐶) |
41 | | monmat2matmon.e2 |
. . . . 5
⊢ 𝐸 =
(.g‘(mulGrp‘𝑃)) |
42 | | monmat2matmon.y |
. . . . 5
⊢ 𝑌 = (var1‘𝑅) |
43 | 11, 38, 39, 5, 6, 1,
40, 41, 42 | mat2pmatscmxcl 21491 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑀‘𝑛) ∈ 𝐾 ∧ 𝑛 ∈ ℕ0)) → ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) ∈ 𝐵) |
44 | 32, 36, 37, 43 | syl12anc 836 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) ∈ 𝐵) |
45 | | fvexd 6689 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (0g‘𝐶) ∈ V) |
46 | | ovexd 7205 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) ∈ V) |
47 | | simpr 488 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑m ℕ0))
→ 𝑀 ∈ (𝐾 ↑m
ℕ0)) |
48 | | fvex 6687 |
. . . . . . 7
⊢
(0g‘𝐴) ∈ V |
49 | | fsuppmapnn0ub 13454 |
. . . . . . 7
⊢ ((𝑀 ∈ (𝐾 ↑m ℕ0)
∧ (0g‘𝐴) ∈ V) → (𝑀 finSupp (0g‘𝐴) → ∃𝑦 ∈ ℕ0
∀𝑥 ∈
ℕ0 (𝑦 <
𝑥 → (𝑀‘𝑥) = (0g‘𝐴)))) |
50 | 47, 48, 49 | sylancl 589 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑m ℕ0))
→ (𝑀 finSupp
(0g‘𝐴)
→ ∃𝑦 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → (𝑀‘𝑥) = (0g‘𝐴)))) |
51 | | csbov12g 7214 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (⦋𝑥 / 𝑛⦌(𝑛𝐸𝑌) ·
⦋𝑥 / 𝑛⦌(𝑇‘(𝑀‘𝑛)))) |
52 | | csbov1g 7215 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑛𝐸𝑌) = (⦋𝑥 / 𝑛⦌𝑛𝐸𝑌)) |
53 | | csbvarg 4321 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌𝑛 = 𝑥) |
54 | 53 | oveq1d 7185 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ (⦋𝑥 /
𝑛⦌𝑛𝐸𝑌) = (𝑥𝐸𝑌)) |
55 | 52, 54 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑛𝐸𝑌) = (𝑥𝐸𝑌)) |
56 | | csbfv2g 6718 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑇‘(𝑀‘𝑛)) = (𝑇‘⦋𝑥 / 𝑛⦌(𝑀‘𝑛))) |
57 | | csbfv2g 6718 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑀‘𝑛) = (𝑀‘⦋𝑥 / 𝑛⦌𝑛)) |
58 | 53 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℕ0
→ (𝑀‘⦋𝑥 / 𝑛⦌𝑛) = (𝑀‘𝑥)) |
59 | 57, 58 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑀‘𝑛) = (𝑀‘𝑥)) |
60 | 59 | fveq2d 6678 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ (𝑇‘⦋𝑥 / 𝑛⦌(𝑀‘𝑛)) = (𝑇‘(𝑀‘𝑥))) |
61 | 56, 60 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑇‘(𝑀‘𝑛)) = (𝑇‘(𝑀‘𝑥))) |
62 | 55, 61 | oveq12d 7188 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℕ0
→ (⦋𝑥 /
𝑛⦌(𝑛𝐸𝑌) ·
⦋𝑥 / 𝑛⦌(𝑇‘(𝑀‘𝑛))) = ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥)))) |
63 | 51, 62 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥)))) |
64 | 63 | adantl 485 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) →
⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥)))) |
65 | 64 | adantr 484 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑀‘𝑥) = (0g‘𝐴)) → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥)))) |
66 | | fveq2 6674 |
. . . . . . . . . . . . 13
⊢ ((𝑀‘𝑥) = (0g‘𝐴) → (𝑇‘(𝑀‘𝑥)) = (𝑇‘(0g‘𝐴))) |
67 | 66 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ ((𝑀‘𝑥) = (0g‘𝐴) → ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥))) = ((𝑥𝐸𝑌) · (𝑇‘(0g‘𝐴)))) |
68 | 39, 11, 38, 5, 6, 1 | mat2pmatghm 21481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐴 GrpHom 𝐶)) |
69 | 3, 68 | sylan2 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑇 ∈ (𝐴 GrpHom 𝐶)) |
70 | 69 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑇 ∈ (𝐴 GrpHom 𝐶)) |
71 | | ghmmhm 18486 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ (𝐴 GrpHom 𝐶) → 𝑇 ∈ (𝐴 MndHom 𝐶)) |
72 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐴) = (0g‘𝐴) |
73 | 72, 2 | mhm0 18080 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ (𝐴 MndHom 𝐶) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
74 | 70, 71, 73 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
75 | 74 | oveq2d 7186 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑥𝐸𝑌) · (𝑇‘(0g‘𝐴))) = ((𝑥𝐸𝑌) ·
(0g‘𝐶))) |
76 | 5 | ply1ring 21023 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
77 | 3, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Ring) |
78 | 6 | matlmod 21180 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) → 𝐶 ∈ LMod) |
79 | 77, 78 | sylan2 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ LMod) |
80 | 79 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝐶 ∈ LMod) |
81 | 77 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ Ring) |
82 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
83 | 82 | ringmgp 19422 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
84 | 81, 83 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(mulGrp‘𝑃) ∈
Mnd) |
85 | 84 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) →
(mulGrp‘𝑃) ∈
Mnd) |
86 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈
ℕ0) |
87 | 3 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring) |
88 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝑃) =
(Base‘𝑃) |
89 | 42, 5, 88 | vr1cl 20992 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ Ring → 𝑌 ∈ (Base‘𝑃)) |
90 | 87, 89 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ (Base‘𝑃)) |
91 | 90 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑌 ∈ (Base‘𝑃)) |
92 | 82, 88 | mgpbas 19364 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
93 | 92, 41 | mulgnn0cl 18362 |
. . . . . . . . . . . . . . . 16
⊢
(((mulGrp‘𝑃)
∈ Mnd ∧ 𝑥 ∈
ℕ0 ∧ 𝑌
∈ (Base‘𝑃))
→ (𝑥𝐸𝑌) ∈ (Base‘𝑃)) |
94 | 85, 86, 91, 93 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → (𝑥𝐸𝑌) ∈ (Base‘𝑃)) |
95 | 5 | ply1crng 20973 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
96 | 6 | matsca2 21171 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝐶)) |
97 | 95, 96 | sylan2 596 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 = (Scalar‘𝐶)) |
98 | 97 | eqcomd 2744 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(Scalar‘𝐶) = 𝑃) |
99 | 98 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) →
(Scalar‘𝐶) = 𝑃) |
100 | 99 | fveq2d 6678 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) →
(Base‘(Scalar‘𝐶)) = (Base‘𝑃)) |
101 | 94, 100 | eleqtrrd 2836 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → (𝑥𝐸𝑌) ∈ (Base‘(Scalar‘𝐶))) |
102 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(Scalar‘𝐶) =
(Scalar‘𝐶) |
103 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶)) |
104 | 102, 40, 103, 2 | lmodvs0 19787 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ LMod ∧ (𝑥𝐸𝑌) ∈ (Base‘(Scalar‘𝐶))) → ((𝑥𝐸𝑌) ·
(0g‘𝐶)) =
(0g‘𝐶)) |
105 | 80, 101, 104 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑥𝐸𝑌) ·
(0g‘𝐶)) =
(0g‘𝐶)) |
106 | 75, 105 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑥𝐸𝑌) · (𝑇‘(0g‘𝐴))) = (0g‘𝐶)) |
107 | 67, 106 | sylan9eqr 2795 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑀‘𝑥) = (0g‘𝐴)) → ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥))) = (0g‘𝐶)) |
108 | 65, 107 | eqtrd 2773 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑀‘𝑥) = (0g‘𝐴)) → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)) |
109 | 108 | ex 416 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑀‘𝑥) = (0g‘𝐴) → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶))) |
110 | 109 | imim2d 57 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑦 < 𝑥 → (𝑀‘𝑥) = (0g‘𝐴)) → (𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)))) |
111 | 110 | ralimdva 3091 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) → (∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → (𝑀‘𝑥) = (0g‘𝐴)) → ∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)))) |
112 | 111 | reximdva 3184 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑m ℕ0))
→ (∃𝑦 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → (𝑀‘𝑥) = (0g‘𝐴)) → ∃𝑦 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)))) |
113 | 50, 112 | syld 47 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑m ℕ0))
→ (𝑀 finSupp
(0g‘𝐴)
→ ∃𝑦 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)))) |
114 | 113 | impr 458 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ ∃𝑦 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶))) |
115 | 45, 46, 114 | mptnn0fsupp 13456 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (𝑛 ∈
ℕ0 ↦ ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))) finSupp (0g‘𝐶)) |
116 | 1, 2, 10, 18, 20, 30, 44, 115 | gsummptmhm 19179 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (𝑄
Σg (𝑛 ∈ ℕ0 ↦ (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))))) = (𝐼‘(𝐶 Σg (𝑛 ∈ ℕ0
↦ ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))))))) |
117 | | simpll 767 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) |
118 | 5, 6, 1, 21, 22, 23, 11, 38, 14, 25, 41, 42, 40, 39 | monmat2matmon 21575 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ ((𝑀‘𝑛) ∈ 𝐾 ∧ 𝑛 ∈ ℕ0)) → (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))) = ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))) |
119 | 117, 36, 37, 118 | syl12anc 836 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))) = ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))) |
120 | 119 | mpteq2dva 5125 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (𝑛 ∈
ℕ0 ↦ (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))))) = (𝑛 ∈ ℕ0 ↦ ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋)))) |
121 | 120 | oveq2d 7186 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (𝑄
Σg (𝑛 ∈ ℕ0 ↦ (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))))) = (𝑄 Σg (𝑛 ∈ ℕ0
↦ ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))))) |
122 | 116, 121 | eqtr3d 2775 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (𝐼‘(𝐶 Σg
(𝑛 ∈
ℕ0 ↦ ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))))) = (𝑄 Σg (𝑛 ∈ ℕ0
↦ ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))))) |