| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | monmat2matmon.b | . . 3
⊢ 𝐵 = (Base‘𝐶) | 
| 2 |  | eqid 2737 | . . 3
⊢
(0g‘𝐶) = (0g‘𝐶) | 
| 3 |  | crngring 20242 | . . . . . 6
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | 
| 4 | 3 | anim2i 617 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) | 
| 5 |  | monmat2matmon.p | . . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) | 
| 6 |  | monmat2matmon.c | . . . . . 6
⊢ 𝐶 = (𝑁 Mat 𝑃) | 
| 7 | 5, 6 | pmatring 22698 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) | 
| 8 |  | ringcmn 20279 | . . . . 5
⊢ (𝐶 ∈ Ring → 𝐶 ∈ CMnd) | 
| 9 | 4, 7, 8 | 3syl 18 | . . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ CMnd) | 
| 10 | 9 | adantr 480 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ 𝐶 ∈
CMnd) | 
| 11 |  | monmat2matmon.a | . . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) | 
| 12 | 11 | matring 22449 | . . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) | 
| 13 | 3, 12 | sylan2 593 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring) | 
| 14 |  | monmat2matmon.q | . . . . . 6
⊢ 𝑄 = (Poly1‘𝐴) | 
| 15 | 14 | ply1ring 22249 | . . . . 5
⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring) | 
| 16 |  | ringmnd 20240 | . . . . 5
⊢ (𝑄 ∈ Ring → 𝑄 ∈ Mnd) | 
| 17 | 13, 15, 16 | 3syl 18 | . . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑄 ∈ Mnd) | 
| 18 | 17 | adantr 480 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ 𝑄 ∈
Mnd) | 
| 19 |  | nn0ex 12532 | . . . 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 2737 | . . . . . . 7
⊢
(Base‘𝑄) =
(Base‘𝑄) | 
| 25 |  | monmat2matmon.i | . . . . . . 7
⊢ 𝐼 = (𝑁 pMatToMatPoly 𝑅) | 
| 26 | 5, 6, 1, 21, 22, 23, 11, 14, 24, 25 | pm2mpghm 22822 | . . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐼 ∈ (𝐶 GrpHom 𝑄)) | 
| 27 | 3, 26 | sylan2 593 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐼 ∈ (𝐶 GrpHom 𝑄)) | 
| 28 | 27 | adantr 480 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ 𝐼 ∈ (𝐶 GrpHom 𝑄)) | 
| 29 |  | ghmmhm 19244 | . . . 4
⊢ (𝐼 ∈ (𝐶 GrpHom 𝑄) → 𝐼 ∈ (𝐶 MndHom 𝑄)) | 
| 30 | 28, 29 | syl 17 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ 𝐼 ∈ (𝐶 MndHom 𝑄)) | 
| 31 | 4 | adantr 480 | . . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (𝑁 ∈ Fin ∧
𝑅 ∈
Ring)) | 
| 32 | 31 | adantr 480 | . . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) | 
| 33 |  | elmapi 8889 | . . . . . . 7
⊢ (𝑀 ∈ (𝐾 ↑m ℕ0)
→ 𝑀:ℕ0⟶𝐾) | 
| 34 | 33 | adantr 480 | . . . . . 6
⊢ ((𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴))
→ 𝑀:ℕ0⟶𝐾) | 
| 35 | 34 | adantl 481 | . . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ 𝑀:ℕ0⟶𝐾) | 
| 36 | 35 | ffvelcdmda 7104 | . . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → (𝑀‘𝑛) ∈ 𝐾) | 
| 37 |  | simpr 484 | . . . 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 22746 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑀‘𝑛) ∈ 𝐾 ∧ 𝑛 ∈ ℕ0)) → ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) ∈ 𝐵) | 
| 44 | 32, 36, 37, 43 | syl12anc 837 | . . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) ∈ 𝐵) | 
| 45 |  | fvexd 6921 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (0g‘𝐶) ∈ V) | 
| 46 |  | ovexd 7466 | . . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) ∈ V) | 
| 47 |  | simpr 484 | . . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑m ℕ0))
→ 𝑀 ∈ (𝐾 ↑m
ℕ0)) | 
| 48 |  | fvex 6919 | . . . . . . 7
⊢
(0g‘𝐴) ∈ V | 
| 49 |  | fsuppmapnn0ub 14036 | . . . . . . 7
⊢ ((𝑀 ∈ (𝐾 ↑m ℕ0)
∧ (0g‘𝐴) ∈ V) → (𝑀 finSupp (0g‘𝐴) → ∃𝑦 ∈ ℕ0
∀𝑥 ∈
ℕ0 (𝑦 <
𝑥 → (𝑀‘𝑥) = (0g‘𝐴)))) | 
| 50 | 47, 48, 49 | sylancl 586 | . . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑m ℕ0))
→ (𝑀 finSupp
(0g‘𝐴)
→ ∃𝑦 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → (𝑀‘𝑥) = (0g‘𝐴)))) | 
| 51 |  | csbov12g 7477 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (⦋𝑥 / 𝑛⦌(𝑛𝐸𝑌) ·
⦋𝑥 / 𝑛⦌(𝑇‘(𝑀‘𝑛)))) | 
| 52 |  | csbov1g 7478 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑛𝐸𝑌) = (⦋𝑥 / 𝑛⦌𝑛𝐸𝑌)) | 
| 53 |  | csbvarg 4434 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌𝑛 = 𝑥) | 
| 54 | 53 | oveq1d 7446 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ (⦋𝑥 /
𝑛⦌𝑛𝐸𝑌) = (𝑥𝐸𝑌)) | 
| 55 | 52, 54 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑛𝐸𝑌) = (𝑥𝐸𝑌)) | 
| 56 |  | csbfv2g 6955 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑇‘(𝑀‘𝑛)) = (𝑇‘⦋𝑥 / 𝑛⦌(𝑀‘𝑛))) | 
| 57 |  | csbfv2g 6955 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑀‘𝑛) = (𝑀‘⦋𝑥 / 𝑛⦌𝑛)) | 
| 58 | 53 | fveq2d 6910 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℕ0
→ (𝑀‘⦋𝑥 / 𝑛⦌𝑛) = (𝑀‘𝑥)) | 
| 59 | 57, 58 | eqtrd 2777 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑀‘𝑛) = (𝑀‘𝑥)) | 
| 60 | 59 | fveq2d 6910 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ (𝑇‘⦋𝑥 / 𝑛⦌(𝑀‘𝑛)) = (𝑇‘(𝑀‘𝑥))) | 
| 61 | 56, 60 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌(𝑇‘(𝑀‘𝑛)) = (𝑇‘(𝑀‘𝑥))) | 
| 62 | 55, 61 | oveq12d 7449 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℕ0
→ (⦋𝑥 /
𝑛⦌(𝑛𝐸𝑌) ·
⦋𝑥 / 𝑛⦌(𝑇‘(𝑀‘𝑛))) = ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥)))) | 
| 63 | 51, 62 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ0
→ ⦋𝑥 /
𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥)))) | 
| 64 | 63 | adantl 481 | . . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) →
⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥)))) | 
| 65 | 64 | adantr 480 | . . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑀‘𝑥) = (0g‘𝐴)) → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥)))) | 
| 66 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ ((𝑀‘𝑥) = (0g‘𝐴) → (𝑇‘(𝑀‘𝑥)) = (𝑇‘(0g‘𝐴))) | 
| 67 | 66 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((𝑀‘𝑥) = (0g‘𝐴) → ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥))) = ((𝑥𝐸𝑌) · (𝑇‘(0g‘𝐴)))) | 
| 68 | 39, 11, 38, 5, 6, 1 | mat2pmatghm 22736 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐴 GrpHom 𝐶)) | 
| 69 | 3, 68 | sylan2 593 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑇 ∈ (𝐴 GrpHom 𝐶)) | 
| 70 | 69 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑇 ∈ (𝐴 GrpHom 𝐶)) | 
| 71 |  | ghmmhm 19244 | . . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ (𝐴 GrpHom 𝐶) → 𝑇 ∈ (𝐴 MndHom 𝐶)) | 
| 72 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢
(0g‘𝐴) = (0g‘𝐴) | 
| 73 | 72, 2 | mhm0 18807 | . . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ (𝐴 MndHom 𝐶) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) | 
| 74 | 70, 71, 73 | 3syl 18 | . . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) | 
| 75 | 74 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑥𝐸𝑌) · (𝑇‘(0g‘𝐴))) = ((𝑥𝐸𝑌) ·
(0g‘𝐶))) | 
| 76 | 5 | ply1ring 22249 | . . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) | 
| 77 | 3, 76 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Ring) | 
| 78 | 6 | matlmod 22435 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) → 𝐶 ∈ LMod) | 
| 79 | 77, 78 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ LMod) | 
| 80 | 79 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝐶 ∈ LMod) | 
| 81 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) | 
| 82 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑃) =
(Base‘𝑃) | 
| 83 | 81, 82 | mgpbas 20142 | . . . . . . . . . . . . . . . 16
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) | 
| 84 | 77 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ Ring) | 
| 85 | 81 | ringmgp 20236 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) | 
| 86 | 84, 85 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(mulGrp‘𝑃) ∈
Mnd) | 
| 87 | 86 | ad3antrrr 730 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) →
(mulGrp‘𝑃) ∈
Mnd) | 
| 88 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈
ℕ0) | 
| 89 | 3 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring) | 
| 90 | 42, 5, 82 | vr1cl 22219 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ Ring → 𝑌 ∈ (Base‘𝑃)) | 
| 91 | 89, 90 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ (Base‘𝑃)) | 
| 92 | 91 | ad3antrrr 730 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑌 ∈ (Base‘𝑃)) | 
| 93 | 83, 41, 87, 88, 92 | mulgnn0cld 19113 | . . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → (𝑥𝐸𝑌) ∈ (Base‘𝑃)) | 
| 94 | 5 | ply1crng 22200 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) | 
| 95 | 6 | matsca2 22426 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝐶)) | 
| 96 | 94, 95 | sylan2 593 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 = (Scalar‘𝐶)) | 
| 97 | 96 | eqcomd 2743 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(Scalar‘𝐶) = 𝑃) | 
| 98 | 97 | ad3antrrr 730 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) →
(Scalar‘𝐶) = 𝑃) | 
| 99 | 98 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) →
(Base‘(Scalar‘𝐶)) = (Base‘𝑃)) | 
| 100 | 93, 99 | eleqtrrd 2844 | . . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → (𝑥𝐸𝑌) ∈ (Base‘(Scalar‘𝐶))) | 
| 101 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢
(Scalar‘𝐶) =
(Scalar‘𝐶) | 
| 102 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶)) | 
| 103 | 101, 40, 102, 2 | lmodvs0 20894 | . . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ LMod ∧ (𝑥𝐸𝑌) ∈ (Base‘(Scalar‘𝐶))) → ((𝑥𝐸𝑌) ·
(0g‘𝐶)) =
(0g‘𝐶)) | 
| 104 | 80, 100, 103 | syl2anc 584 | . . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑥𝐸𝑌) ·
(0g‘𝐶)) =
(0g‘𝐶)) | 
| 105 | 75, 104 | eqtrd 2777 | . . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑥𝐸𝑌) · (𝑇‘(0g‘𝐴))) = (0g‘𝐶)) | 
| 106 | 67, 105 | sylan9eqr 2799 | . . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑀‘𝑥) = (0g‘𝐴)) → ((𝑥𝐸𝑌) · (𝑇‘(𝑀‘𝑥))) = (0g‘𝐶)) | 
| 107 | 65, 106 | eqtrd 2777 | . . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑀‘𝑥) = (0g‘𝐴)) → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)) | 
| 108 | 107 | ex 412 | . . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑀‘𝑥) = (0g‘𝐴) → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶))) | 
| 109 | 108 | imim2d 57 | . . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑦 < 𝑥 → (𝑀‘𝑥) = (0g‘𝐴)) → (𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)))) | 
| 110 | 109 | ralimdva 3167 | . . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑m ℕ0))
∧ 𝑦 ∈
ℕ0) → (∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → (𝑀‘𝑥) = (0g‘𝐴)) → ∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)))) | 
| 111 | 110 | reximdva 3168 | . . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑m ℕ0))
→ (∃𝑦 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → (𝑀‘𝑥) = (0g‘𝐴)) → ∃𝑦 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)))) | 
| 112 | 50, 111 | syld 47 | . . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑀 ∈ (𝐾 ↑m ℕ0))
→ (𝑀 finSupp
(0g‘𝐴)
→ ∃𝑦 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶)))) | 
| 113 | 112 | impr 454 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ ∃𝑦 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑦 < 𝑥 → ⦋𝑥 / 𝑛⦌((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))) = (0g‘𝐶))) | 
| 114 | 45, 46, 113 | mptnn0fsupp 14038 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (𝑛 ∈
ℕ0 ↦ ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))) finSupp (0g‘𝐶)) | 
| 115 | 1, 2, 10, 18, 20, 30, 44, 114 | gsummptmhm 19958 | . 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (𝑄
Σg (𝑛 ∈ ℕ0 ↦ (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))))) = (𝐼‘(𝐶 Σg (𝑛 ∈ ℕ0
↦ ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))))))) | 
| 116 |  | simpll 767 | . . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) | 
| 117 | 5, 6, 1, 21, 22, 23, 11, 38, 14, 25, 41, 42, 40, 39 | monmat2matmon 22830 | . . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ ((𝑀‘𝑛) ∈ 𝐾 ∧ 𝑛 ∈ ℕ0)) → (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))) = ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))) | 
| 118 | 116, 36, 37, 117 | syl12anc 837 | . . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
∧ 𝑛 ∈
ℕ0) → (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))) = ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))) | 
| 119 | 118 | mpteq2dva 5242 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (𝑛 ∈
ℕ0 ↦ (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛))))) = (𝑛 ∈ ℕ0 ↦ ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋)))) | 
| 120 | 119 | oveq2d 7447 | . 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (𝑄
Σg (𝑛 ∈ ℕ0 ↦ (𝐼‘((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))))) = (𝑄 Σg (𝑛 ∈ ℕ0
↦ ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))))) | 
| 121 | 115, 120 | eqtr3d 2779 | 1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0)
∧ 𝑀 finSupp
(0g‘𝐴)))
→ (𝐼‘(𝐶 Σg
(𝑛 ∈
ℕ0 ↦ ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))))) = (𝑄 Σg (𝑛 ∈ ℕ0
↦ ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))))) |