Step | Hyp | Ref
| Expression |
1 | | monmat2matmon.b |
. . 3
⊢ 𝐵 = (Base‘𝐶) |
2 | | eqid 2610 |
. . 3
⊢
(0g‘𝐶) = (0g‘𝐶) |
3 | | crngring 18381 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
4 | 3 | anim2i 591 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
5 | | monmat2matmon.p |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) |
6 | | monmat2matmon.c |
. . . . . 6
⊢ 𝐶 = (𝑁 Mat 𝑃) |
7 | 5, 6 | pmatring 20317 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
8 | | ringcmn 18404 |
. . . . 5
⊢ (𝐶 ∈ Ring → 𝐶 ∈ CMnd) |
9 | 4, 7, 8 | 3syl 18 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ CMnd) |
10 | 9 | adantr 480 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → 𝐶 ∈ CMnd) |
11 | | monmat2matmon.a |
. . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) |
12 | 11 | matring 20068 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
13 | 3, 12 | sylan2 490 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring) |
14 | | monmat2matmon.q |
. . . . . 6
⊢ 𝑄 = (Poly1‘𝐴) |
15 | 14 | ply1ring 19439 |
. . . . 5
⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring) |
16 | | ringmnd 18379 |
. . . . 5
⊢ (𝑄 ∈ Ring → 𝑄 ∈ Mnd) |
17 | 13, 15, 16 | 3syl 18 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑄 ∈ Mnd) |
18 | 17 | adantr 480 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → 𝑄 ∈ Mnd) |
19 | | nn0ex 11175 |
. . . 4
⊢
ℕ0 ∈ V |
20 | 19 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → ℕ0
∈ V) |
21 | | monmat2matmon.m1 |
. . . . . . 7
⊢ ∗ = (
·𝑠 ‘𝑄) |
22 | | monmat2matmon.e1 |
. . . . . . 7
⊢ ↑ =
(.g‘(mulGrp‘𝑄)) |
23 | | monmat2matmon.x |
. . . . . . 7
⊢ 𝑋 = (var1‘𝐴) |
24 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑄) =
(Base‘𝑄) |
25 | | monmat2matmon.i |
. . . . . . 7
⊢ 𝐼 = (𝑁 pMatToMatPoly 𝑅) |
26 | 5, 6, 1, 21, 22, 23, 11, 14, 24, 25 | pm2mpghm 20440 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐼 ∈ (𝐶 GrpHom 𝑄)) |
27 | 3, 26 | sylan2 490 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐼 ∈ (𝐶 GrpHom 𝑄)) |
28 | 27 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → 𝐼 ∈ (𝐶 GrpHom 𝑄)) |
29 | | ghmmhm 17493 |
. . . 4
⊢ (𝐼 ∈ (𝐶 GrpHom 𝑄) → 𝐼 ∈ (𝐶 MndHom 𝑄)) |
30 | 28, 29 | syl 17 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → 𝐼 ∈ (𝐶 MndHom 𝑄)) |
31 | 4 | adantr 480 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
32 | 31 | adantr 480 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
33 | | elmapi 7765 |
. . . . . . 7
⊢ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) → 𝑀:ℕ0⟶𝐾) |
34 | 33 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴)) → 𝑀:ℕ0⟶𝐾) |
35 | 34 | adantl 481 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → 𝑀:ℕ0⟶𝐾) |
36 | 35 | ffvelrnda 6267 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) ∧ 𝑛 ∈ ℕ0) → (𝑀‘𝑛) ∈ 𝐾) |
37 | | simpr 476 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ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 20364 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑀‘𝑛) ∈ 𝐾 ∧ 𝑛 ∈ ℕ0)) → ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) ∈ 𝐵) |
44 | 32, 36, 37, 43 | syl12anc 1316 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) ∧ 𝑛 ∈ ℕ0) → ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) ∈ 𝐵) |
45 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝐶) ∈ V |
46 | 45 | a1i 11 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) →
(0g‘𝐶)
∈ V) |
47 | | ovex 6577 |
. . . . 5
⊢ ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) ∈ V |
48 | 47 | a1i 11 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) ∧ 𝑛 ∈ ℕ0) → ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) ∈ V) |
49 | | simpr 476 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) → 𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) |
50 | | fvex 6113 |
. . . . . . 7
⊢
(0g‘𝐴) ∈ V |
51 | | fsuppmapnn0ub 12657 |
. . . . . . 7
⊢ ((𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ (0g‘𝐴) ∈ V) → (𝑀 finSupp (0g‘𝐴) → ∃𝑦 ∈ ℕ0
∀𝑥 ∈
ℕ0 (𝑦 <
𝑥 → (𝑀‘𝑥) = (0g‘𝐴)))) |
52 | 49, 50, 51 | sylancl 693 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) → (𝑀 finSupp (0g‘𝐴) → ∃𝑦 ∈ ℕ0
∀𝑥 ∈
ℕ0 (𝑦 <
𝑥 → (𝑀‘𝑥) = (0g‘𝐴)))) |
53 | | csbov12g 6587 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (⦋𝑥 / 𝑛⦌(𝑛𝐸𝑌) ·
⦋𝑥 / 𝑛⦌(𝑇‘(𝑀‘𝑛)))) |
54 | | csbov1g 6588 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑛𝐸𝑌) = (⦋𝑥 / 𝑛⦌𝑛𝐸𝑌)) |
55 | | csbvarg 3955 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌𝑛 = 𝑥) |
56 | 55 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ (⦋𝑥 /
𝑛⦌𝑛𝐸𝑌) = (𝑥𝐸𝑌)) |
57 | 54, 56 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑛𝐸𝑌) = (𝑥𝐸𝑌)) |
58 | | csbfv2g 6142 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑇‘(𝑀‘𝑛)) = (𝑇‘⦋𝑥 / 𝑛⦌(𝑀‘𝑛))) |
59 | | csbfv2g 6142 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑀‘𝑛) = (𝑀‘⦋𝑥 / 𝑛⦌𝑛)) |
60 | 55 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℕ0
→ (𝑀‘⦋𝑥 / 𝑛⦌𝑛) = (𝑀‘𝑥)) |
61 | 59, 60 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑀‘𝑛) = (𝑀‘𝑥)) |
62 | 61 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ (𝑇‘⦋𝑥 / 𝑛⦌(𝑀‘𝑛)) = (𝑇‘(𝑀‘𝑥))) |
63 | 58, 62 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑇‘(𝑀‘𝑛)) = (𝑇‘(𝑀‘𝑥))) |
64 | 57, 63 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℕ0
→ (⦋𝑥 /
𝑛⦌(𝑛𝐸𝑌) ·
⦋𝑥 / 𝑛⦌(𝑇‘(𝑀‘𝑛))) = ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥)))) |
65 | 53, 64 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥)))) |
66 | 65 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ⦋𝑥 /
𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥)))) |
67 | 66 | adantr 480 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
∧ (𝑀‘𝑥) = (0g‘𝐴)) → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥)))) |
68 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ ((𝑀‘𝑥) = (0g‘𝐴) → (𝑇‘(𝑀‘𝑥)) = (𝑇‘(0g‘𝐴))) |
69 | 68 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝑀‘𝑥) = (0g‘𝐴) → ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥))) = ((𝑥𝐸𝑌) · (𝑇‘(0g‘𝐴)))) |
70 | 39, 11, 38, 5, 6, 1 | mat2pmatghm 20354 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐴 GrpHom 𝐶)) |
71 | 3, 70 | sylan2 490 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑇 ∈ (𝐴 GrpHom 𝐶)) |
72 | 71 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ 𝑇 ∈ (𝐴 GrpHom 𝐶)) |
73 | | ghmmhm 17493 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ (𝐴 GrpHom 𝐶) → 𝑇 ∈ (𝐴 MndHom 𝐶)) |
74 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐴) = (0g‘𝐴) |
75 | 74, 2 | mhm0 17166 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ (𝐴 MndHom 𝐶) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
76 | 72, 73, 75 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
77 | 76 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑥𝐸𝑌) · (𝑇‘(0g‘𝐴))) = ((𝑥𝐸𝑌) ·
(0g‘𝐶))) |
78 | 5 | ply1ring 19439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
79 | 3, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Ring) |
80 | 6 | matlmod 20054 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) → 𝐶 ∈ LMod) |
81 | 79, 80 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ LMod) |
82 | 81 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ 𝐶 ∈
LMod) |
83 | 79 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ Ring) |
84 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
85 | 84 | ringmgp 18376 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
86 | 83, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(mulGrp‘𝑃) ∈
Mnd) |
87 | 86 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (mulGrp‘𝑃)
∈ Mnd) |
88 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ 𝑥 ∈
ℕ0) |
89 | 3 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring) |
90 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝑃) =
(Base‘𝑃) |
91 | 42, 5, 90 | vr1cl 19408 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ Ring → 𝑌 ∈ (Base‘𝑃)) |
92 | 89, 91 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ (Base‘𝑃)) |
93 | 92 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ 𝑌 ∈
(Base‘𝑃)) |
94 | 84, 90 | mgpbas 18318 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
95 | 94, 41 | mulgnn0cl 17381 |
. . . . . . . . . . . . . . . 16
⊢
(((mulGrp‘𝑃)
∈ Mnd ∧ 𝑥 ∈
ℕ0 ∧ 𝑌
∈ (Base‘𝑃))
→ (𝑥𝐸𝑌) ∈ (Base‘𝑃)) |
96 | 87, 88, 93, 95 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (𝑥𝐸𝑌) ∈ (Base‘𝑃)) |
97 | 5 | ply1crng 19389 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
98 | 6 | matsca2 20045 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝐶)) |
99 | 97, 98 | sylan2 490 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 = (Scalar‘𝐶)) |
100 | 99 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(Scalar‘𝐶) = 𝑃) |
101 | 100 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (Scalar‘𝐶) =
𝑃) |
102 | 101 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (Base‘(Scalar‘𝐶)) = (Base‘𝑃)) |
103 | 96, 102 | eleqtrrd 2691 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (𝑥𝐸𝑌) ∈ (Base‘(Scalar‘𝐶))) |
104 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Scalar‘𝐶) =
(Scalar‘𝐶) |
105 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶)) |
106 | 104, 40, 105, 2 | lmodvs0 18720 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ LMod ∧ (𝑥𝐸𝑌) ∈ (Base‘(Scalar‘𝐶))) → ((𝑥𝐸𝑌) ·
(0g‘𝐶)) =
(0g‘𝐶)) |
107 | 82, 103, 106 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑥𝐸𝑌) ·
(0g‘𝐶)) =
(0g‘𝐶)) |
108 | 77, 107 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑥𝐸𝑌) · (𝑇‘(0g‘𝐴))) = (0g‘𝐶)) |
109 | 69, 108 | sylan9eqr 2666 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
∧ (𝑀‘𝑥) = (0g‘𝐴)) → ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥))) = (0g‘𝐶)) |
110 | 67, 109 | eqtrd 2644 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
∧ (𝑀‘𝑥) = (0g‘𝐴)) → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)) |
111 | 110 | ex 449 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑀‘𝑥) = (0g‘𝐴) → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶))) |
112 | 111 | imim2d 55 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑦 < 𝑥 → (𝑀‘𝑥) = (0g‘𝐴)) → (𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)))) |
113 | 112 | ralimdva 2945 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) ∧ 𝑦 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑦 <
𝑥 → (𝑀‘𝑥) = (0g‘𝐴)) → ∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)))) |
114 | 113 | reximdva 3000 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) → (∃𝑦 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑦 < 𝑥 → (𝑀‘𝑥) = (0g‘𝐴)) → ∃𝑦 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)))) |
115 | 52, 114 | syld 46 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑𝑚
ℕ0)) → (𝑀 finSupp (0g‘𝐴) → ∃𝑦 ∈ ℕ0
∀𝑥 ∈
ℕ0 (𝑦 <
𝑥 →
⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)))) |
116 | 115 | impr 647 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → ∃𝑦 ∈ ℕ0
∀𝑥 ∈
ℕ0 (𝑦 <
𝑥 →
⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶))) |
117 | 46, 48, 116 | mptnn0fsupp 12659 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))) finSupp (0g‘𝐶)) |
118 | 1, 2, 10, 18, 20, 30, 44, 117 | gsummptmhm 18163 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → (𝑄 Σg (𝑛 ∈ ℕ0
↦ (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))))) = (𝐼‘(𝐶 Σg (𝑛 ∈ ℕ0
↦ ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))))))) |
119 | | simpll 786 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) |
120 | 5, 6, 1, 21, 22, 23, 11, 38, 14, 25, 41, 42, 40, 39 | monmat2matmon 20448 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ ((𝑀‘𝑛) ∈ 𝐾 ∧ 𝑛 ∈ ℕ0)) → (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))) = ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))) |
121 | 119, 36, 37, 120 | syl12anc 1316 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) ∧ 𝑛 ∈ ℕ0) → (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))) = ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))) |
122 | 121 | mpteq2dva 4672 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → (𝑛 ∈ ℕ0 ↦ (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))))) = (𝑛 ∈ ℕ0 ↦ ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋)))) |
123 | 122 | oveq2d 6565 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → (𝑄 Σg (𝑛 ∈ ℕ0
↦ (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))))) = (𝑄 Σg (𝑛 ∈ ℕ0
↦ ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))))) |
124 | 118, 123 | eqtr3d 2646 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚
ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → (𝐼‘(𝐶 Σg (𝑛 ∈ ℕ0
↦ ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))))) = (𝑄 Σg (𝑛 ∈ ℕ0
↦ ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))))) |