Proof of Theorem cpmadugsumlemC
Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. . 3
⊢
(Base‘𝑌) =
(Base‘𝑌) |
2 | | eqid 2736 |
. . 3
⊢
(0g‘𝑌) = (0g‘𝑌) |
3 | | eqid 2736 |
. . 3
⊢
(+g‘𝑌) = (+g‘𝑌) |
4 | | cpmadugsum.r |
. . 3
⊢ × =
(.r‘𝑌) |
5 | | crngring 19976 |
. . . . . . . 8
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
6 | | cpmadugsum.p |
. . . . . . . . 9
⊢ 𝑃 = (Poly1‘𝑅) |
7 | 6 | ply1ring 21619 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
8 | 5, 7 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Ring) |
9 | 8 | anim2i 617 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑃 ∈ Ring)) |
10 | | cpmadugsum.y |
. . . . . . 7
⊢ 𝑌 = (𝑁 Mat 𝑃) |
11 | 10 | matring 21792 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) → 𝑌 ∈ Ring) |
12 | 9, 11 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ Ring) |
13 | 12 | 3adant3 1132 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Ring) |
14 | 13 | adantr 481 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑌 ∈ Ring) |
15 | | ovexd 7392 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (0...𝑠) ∈ V) |
16 | | cpmadugsum.t |
. . . . . 6
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
17 | | cpmadugsum.a |
. . . . . 6
⊢ 𝐴 = (𝑁 Mat 𝑅) |
18 | | cpmadugsum.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐴) |
19 | 16, 17, 18, 6, 10 | mat2pmatbas 22075 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
20 | 5, 19 | syl3an2 1164 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
21 | 20 | adantr 481 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
22 | 9 | 3adant3 1132 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑃 ∈ Ring)) |
23 | 10 | matlmod 21778 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) → 𝑌 ∈ LMod) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ LMod) |
25 | 24 | ad2antrr 724 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑌 ∈ LMod) |
26 | | eqid 2736 |
. . . . . . 7
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
27 | | eqid 2736 |
. . . . . . 7
⊢
(Base‘𝑃) =
(Base‘𝑃) |
28 | 26, 27 | mgpbas 19902 |
. . . . . 6
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
29 | | cpmadugsum.e |
. . . . . 6
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
30 | 8 | 3ad2ant2 1134 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ Ring) |
31 | 26 | ringmgp 19970 |
. . . . . . . 8
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (mulGrp‘𝑃) ∈ Mnd) |
33 | 32 | ad2antrr 724 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (mulGrp‘𝑃) ∈ Mnd) |
34 | | elfznn0 13534 |
. . . . . . 7
⊢ (𝑖 ∈ (0...𝑠) → 𝑖 ∈ ℕ0) |
35 | 34 | adantl 482 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑖 ∈ ℕ0) |
36 | 5 | 3ad2ant2 1134 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
37 | | cpmadugsum.x |
. . . . . . . . 9
⊢ 𝑋 = (var1‘𝑅) |
38 | 37, 6, 27 | vr1cl 21588 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃)) |
39 | 36, 38 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑋 ∈ (Base‘𝑃)) |
40 | 39 | ad2antrr 724 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑋 ∈ (Base‘𝑃)) |
41 | 28, 29, 33, 35, 40 | mulgnn0cld 18897 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑖 ↑ 𝑋) ∈ (Base‘𝑃)) |
42 | 6 | ply1crng 21569 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
43 | 42 | anim2i 617 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing)) |
44 | 43 | 3adant3 1132 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing)) |
45 | 10 | matsca2 21769 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝑌)) |
46 | 44, 45 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑃 = (Scalar‘𝑌)) |
47 | 46 | eqcomd 2742 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝑌) = 𝑃) |
48 | 47 | fveq2d 6846 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Base‘(Scalar‘𝑌)) = (Base‘𝑃)) |
49 | 48 | eleq2d 2823 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑖 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌)) ↔ (𝑖 ↑ 𝑋) ∈ (Base‘𝑃))) |
50 | 49 | ad2antrr 724 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑖 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌)) ↔ (𝑖 ↑ 𝑋) ∈ (Base‘𝑃))) |
51 | 41, 50 | mpbird 256 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑖 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌))) |
52 | | simpll1 1212 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑁 ∈ Fin) |
53 | 36 | ad2antrr 724 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑅 ∈ Ring) |
54 | | simplrl 775 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑠 ∈ ℕ0) |
55 | | simprr 771 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑏 ∈ (𝐵 ↑m (0...𝑠))) |
56 | 55 | anim1i 615 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑏 ∈ (𝐵 ↑m (0...𝑠)) ∧ 𝑖 ∈ (0...𝑠))) |
57 | 17, 18, 6, 10, 16 | m2pmfzmap 22096 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0)
∧ (𝑏 ∈ (𝐵 ↑m (0...𝑠)) ∧ 𝑖 ∈ (0...𝑠))) → (𝑇‘(𝑏‘𝑖)) ∈ (Base‘𝑌)) |
58 | 52, 53, 54, 56, 57 | syl31anc 1373 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑇‘(𝑏‘𝑖)) ∈ (Base‘𝑌)) |
59 | | eqid 2736 |
. . . . 5
⊢
(Scalar‘𝑌) =
(Scalar‘𝑌) |
60 | | cpmadugsum.m |
. . . . 5
⊢ · = (
·𝑠 ‘𝑌) |
61 | | eqid 2736 |
. . . . 5
⊢
(Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌)) |
62 | 1, 59, 60, 61 | lmodvscl 20339 |
. . . 4
⊢ ((𝑌 ∈ LMod ∧ (𝑖 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌)) ∧ (𝑇‘(𝑏‘𝑖)) ∈ (Base‘𝑌)) → ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖))) ∈ (Base‘𝑌)) |
63 | 25, 51, 58, 62 | syl3anc 1371 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖))) ∈ (Base‘𝑌)) |
64 | | simpl1 1191 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑁 ∈ Fin) |
65 | 36 | adantr 481 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑅 ∈ Ring) |
66 | | simprl 769 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑠 ∈ ℕ0) |
67 | | eqid 2736 |
. . . . 5
⊢ (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))) = (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))) |
68 | | fzfid 13878 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0)
∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (0...𝑠) ∈ Fin) |
69 | | ovexd 7392 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0)
∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖))) ∈ V) |
70 | | fvexd 6857 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0)
∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) →
(0g‘𝑌)
∈ V) |
71 | 67, 68, 69, 70 | fsuppmptdm 9316 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0)
∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))) finSupp (0g‘𝑌)) |
72 | 64, 65, 66, 55, 71 | syl31anc 1373 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))) finSupp (0g‘𝑌)) |
73 | 1, 2, 3, 4, 14, 15, 21, 63, 72 | gsummulc2 20031 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑇‘𝑀) × ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))))) = ((𝑇‘𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖))))))) |
74 | 10 | matassa 21793 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑌 ∈ AssAlg) |
75 | 43, 74 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ AssAlg) |
76 | 75 | 3adant3 1132 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ AssAlg) |
77 | 76 | ad2antrr 724 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → 𝑌 ∈ AssAlg) |
78 | 8 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ Ring) |
79 | 78, 31 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(mulGrp‘𝑃) ∈
Mnd) |
80 | 79 | 3adant3 1132 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (mulGrp‘𝑃) ∈ Mnd) |
81 | 80 | ad2antrr 724 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (mulGrp‘𝑃) ∈ Mnd) |
82 | 28, 29, 81, 35, 40 | mulgnn0cld 18897 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑖 ↑ 𝑋) ∈ (Base‘𝑃)) |
83 | 48 | ad2antrr 724 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (Base‘(Scalar‘𝑌)) = (Base‘𝑃)) |
84 | 82, 83 | eleqtrrd 2841 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑖 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌))) |
85 | 20 | ad2antrr 724 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
86 | 1, 59, 61, 60, 4 | assaassr 21265 |
. . . . 5
⊢ ((𝑌 ∈ AssAlg ∧ ((𝑖 ↑ 𝑋) ∈ (Base‘(Scalar‘𝑌)) ∧ (𝑇‘𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘𝑖)) ∈ (Base‘𝑌))) → ((𝑇‘𝑀) × ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))) = ((𝑖 ↑ 𝑋) · ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
87 | 77, 84, 85, 58, 86 | syl13anc 1372 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑇‘𝑀) × ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))) = ((𝑖 ↑ 𝑋) · ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
88 | 87 | mpteq2dva 5205 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ (0...𝑠) ↦ ((𝑇‘𝑀) × ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖))))) = (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))))) |
89 | 88 | oveq2d 7373 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑇‘𝑀) × ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) |
90 | 73, 89 | eqtr3d 2778 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑇‘𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) |