Proof of Theorem pmatcollpw3fi1lem1
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) |
2 | | pmatcollpw.p |
. . . . . . . . . . 11
⊢ 𝑃 = (Poly1‘𝑅) |
3 | | pmatcollpw.c |
. . . . . . . . . . 11
⊢ 𝐶 = (𝑁 Mat 𝑃) |
4 | 2, 3 | pmatring 20317 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
5 | | ringmnd 18379 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Ring → 𝐶 ∈ Mnd) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Mnd) |
7 | 6 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
𝐶 ∈
Mnd) |
8 | | pmatcollpw.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐶) |
9 | | ringcmn 18404 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ Ring → 𝐶 ∈ CMnd) |
10 | 4, 9 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ CMnd) |
11 | 10 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
𝐶 ∈
CMnd) |
12 | | snfi 7923 |
. . . . . . . . . 10
⊢ {0}
∈ Fin |
13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) → {0}
∈ Fin) |
14 | | simplll 794 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → 𝑁 ∈ Fin) |
15 | | simpllr 795 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → 𝑅 ∈ Ring) |
16 | | elmapi 7765 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ (𝐷 ↑𝑚 {0}) →
𝐺:{0}⟶𝐷) |
17 | 16 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
𝐺:{0}⟶𝐷) |
18 | 17 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → (𝐺‘𝑛) ∈ 𝐷) |
19 | | elsni 4142 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {0} → 𝑛 = 0) |
20 | | 0nn0 11184 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
21 | 19, 20 | syl6eqel 2696 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ {0} → 𝑛 ∈
ℕ0) |
22 | 21 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → 𝑛 ∈
ℕ0) |
23 | | pmatcollpw3.a |
. . . . . . . . . . . 12
⊢ 𝐴 = (𝑁 Mat 𝑅) |
24 | | pmatcollpw3.d |
. . . . . . . . . . . 12
⊢ 𝐷 = (Base‘𝐴) |
25 | | pmatcollpw.t |
. . . . . . . . . . . 12
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
26 | | pmatcollpw.m |
. . . . . . . . . . . 12
⊢ ∗ = (
·𝑠 ‘𝐶) |
27 | | pmatcollpw.e |
. . . . . . . . . . . 12
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
28 | | pmatcollpw.x |
. . . . . . . . . . . 12
⊢ 𝑋 = (var1‘𝑅) |
29 | 23, 24, 25, 2, 3, 8,
26, 27, 28 | mat2pmatscmxcl 20364 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝐺‘𝑛) ∈ 𝐷 ∧ 𝑛 ∈ ℕ0)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))) ∈ 𝐵) |
30 | 14, 15, 18, 22, 29 | syl22anc 1319 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) →
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))) ∈ 𝐵) |
31 | 30 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
∀𝑛 ∈ {0}
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))) ∈ 𝐵) |
32 | 8, 11, 13, 31 | gsummptcl 18189 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝐶
Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) ∈ 𝐵) |
33 | | eqid 2610 |
. . . . . . . . 9
⊢
(+g‘𝐶) = (+g‘𝐶) |
34 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝐶) = (0g‘𝐶) |
35 | 8, 33, 34 | mndrid 17135 |
. . . . . . . 8
⊢ ((𝐶 ∈ Mnd ∧ (𝐶 Σg
(𝑛 ∈ {0} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) ∈ 𝐵) → ((𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))(+g‘𝐶)(0g‘𝐶)) = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) |
36 | 7, 32, 35 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
((𝐶
Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))(+g‘𝐶)(0g‘𝐶)) = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) |
37 | | 0z 11265 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℤ |
38 | | fzsn 12254 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℤ → (0...0) = {0}) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (0...0) =
{0} |
40 | 39 | eqcomi 2619 |
. . . . . . . . . . 11
⊢ {0} =
(0...0) |
41 | 40 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) → {0}
= (0...0)) |
42 | | pmatcollpw3fi1lem1.h |
. . . . . . . . . . . . . . 15
⊢ 𝐻 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝐺‘0), 0 )) |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → 𝐻 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝐺‘0), 0 ))) |
44 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → 𝑙 = 𝑛) |
45 | 19 | ad2antlr 759 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → 𝑛 = 0) |
46 | 44, 45 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → 𝑙 = 0) |
47 | 46 | iftrued 4044 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = (𝐺‘0)) |
48 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 0 → (𝐺‘𝑛) = (𝐺‘0)) |
49 | 48 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 → (𝐺‘0) = (𝐺‘𝑛)) |
50 | 19, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ {0} → (𝐺‘0) = (𝐺‘𝑛)) |
51 | 50 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → (𝐺‘0) = (𝐺‘𝑛)) |
52 | 47, 51 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = (𝐺‘𝑛)) |
53 | | 1nn0 11185 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℕ0 |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 0 → 1 ∈
ℕ0) |
55 | | nn0uz 11598 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 = (ℤ≥‘0) |
56 | 54, 55 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 0 → 1 ∈
(ℤ≥‘0)) |
57 | | eluzfz1 12219 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
(ℤ≥‘0) → 0 ∈ (0...1)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 → 0 ∈
(0...1)) |
59 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 → (𝑛 ∈ (0...1) ↔ 0 ∈
(0...1))) |
60 | 58, 59 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 0 → 𝑛 ∈ (0...1)) |
61 | 19, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ {0} → 𝑛 ∈
(0...1)) |
62 | 61 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → 𝑛 ∈
(0...1)) |
63 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺:{0}⟶𝐷 ∧ 𝑛 ∈ {0}) → (𝐺‘𝑛) ∈ 𝐷) |
64 | 63 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺:{0}⟶𝐷 → (𝑛 ∈ {0} → (𝐺‘𝑛) ∈ 𝐷)) |
65 | 16, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ (𝐷 ↑𝑚 {0}) →
(𝑛 ∈ {0} → (𝐺‘𝑛) ∈ 𝐷)) |
66 | 65 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝑛 ∈ {0} → (𝐺‘𝑛) ∈ 𝐷)) |
67 | 66 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → (𝐺‘𝑛) ∈ 𝐷) |
68 | 43, 52, 62, 67 | fvmptd 6197 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → (𝐻‘𝑛) = (𝐺‘𝑛)) |
69 | 68 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → (𝐺‘𝑛) = (𝐻‘𝑛)) |
70 | 69 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → (𝑇‘(𝐺‘𝑛)) = (𝑇‘(𝐻‘𝑛))) |
71 | 70 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) →
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))) = ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))) |
72 | 41, 71 | mpteq12dva 4662 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝑛 ∈ {0} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))) = (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) |
73 | 72 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝐶
Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) = (𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) |
74 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (0 + 1)
∈ V |
75 | 74 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) → (0
+ 1) ∈ V) |
76 | 8, 34 | mndidcl 17131 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ Mnd →
(0g‘𝐶)
∈ 𝐵) |
77 | 6, 76 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝐶)
∈ 𝐵) |
78 | 77 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(0g‘𝐶)
∈ 𝐵) |
79 | 42 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → 𝐻 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝐺‘0), 0 ))) |
80 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 + 1) =
1 |
81 | 80 | eqeq2i 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (0 + 1) ↔ 𝑛 = 1) |
82 | | ax-1ne0 9884 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ≠
0 |
83 | 82 | neii 2784 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ¬ 1
= 0 |
84 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 1 → (𝑛 = 0 ↔ 1 = 0)) |
85 | 83, 84 | mtbiri 316 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → ¬ 𝑛 = 0) |
86 | 81, 85 | sylbi 206 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = (0 + 1) → ¬ 𝑛 = 0) |
87 | 86 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → ¬ 𝑛 = 0) |
88 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑛 → (𝑙 = 0 ↔ 𝑛 = 0)) |
89 | 88 | notbid 307 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑛 → (¬ 𝑙 = 0 ↔ ¬ 𝑛 = 0)) |
90 | 89 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → (¬ 𝑙 = 0 ↔ ¬ 𝑛 = 0)) |
91 | 87, 90 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → ¬ 𝑙 = 0) |
92 | 91 | iffalsed 4047 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = 0 ) |
93 | | pmatcollpw3fi1lem1.0 |
. . . . . . . . . . . . . . . 16
⊢ 0 =
(0g‘𝐴) |
94 | 92, 93 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) =
(0g‘𝐴)) |
95 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → 1 ∈
ℕ0) |
96 | 95, 55 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → 1 ∈
(ℤ≥‘0)) |
97 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
(ℤ≥‘0) → 1 ∈ (0...1)) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → 1 ∈
(0...1)) |
99 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → (𝑛 ∈ (0...1) ↔ 1 ∈
(0...1))) |
100 | 98, 99 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → 𝑛 ∈ (0...1)) |
101 | 81, 100 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (0 + 1) → 𝑛 ∈
(0...1)) |
102 | 101 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → 𝑛 ∈
(0...1)) |
103 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐴) ∈ V |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) →
(0g‘𝐴)
∈ V) |
105 | 79, 94, 102, 104 | fvmptd 6197 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → (𝐻‘𝑛) = (0g‘𝐴)) |
106 | 105 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → (𝑇‘(𝐻‘𝑛)) = (𝑇‘(0g‘𝐴))) |
107 | 23 | fveq2i 6106 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐴) = (0g‘(𝑁 Mat 𝑅)) |
108 | 3 | fveq2i 6106 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐶) = (0g‘(𝑁 Mat 𝑃)) |
109 | 25, 2, 107, 108 | 0mat2pmat 20360 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
110 | 109 | ancoms 468 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
111 | 110 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
112 | 106, 111 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → (𝑇‘(𝐻‘𝑛)) = (0g‘𝐶)) |
113 | 112 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))) = ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶))) |
114 | 2, 3 | pmatlmod 20318 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ LMod) |
115 | 114 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → 𝐶 ∈ LMod) |
116 | | simpllr 795 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → 𝑅 ∈ Ring) |
117 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → (𝑛 ∈ ℕ0 ↔ 1 ∈
ℕ0)) |
118 | 95, 117 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 1 → 𝑛 ∈ ℕ0) |
119 | 81, 118 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (0 + 1) → 𝑛 ∈
ℕ0) |
120 | 119 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → 𝑛 ∈
ℕ0) |
121 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
122 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑃) =
(Base‘𝑃) |
123 | 2, 28, 121, 27, 122 | ply1moncl 19462 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃)) |
124 | 116, 120,
123 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → (𝑛 ↑ 𝑋) ∈ (Base‘𝑃)) |
125 | 2 | ply1ring 19439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
126 | 3 | matsca2 20045 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) → 𝑃 = (Scalar‘𝐶)) |
127 | 125, 126 | sylan2 490 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑃 = (Scalar‘𝐶)) |
128 | 127 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Scalar‘𝐶) = 𝑃) |
129 | 128 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘(Scalar‘𝐶)) = (Base‘𝑃)) |
130 | 129 | eleq2d 2673 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶)) ↔ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃))) |
131 | 130 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → ((𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶)) ↔ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃))) |
132 | 124, 131 | mpbird 246 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → (𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶))) |
133 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Scalar‘𝐶) =
(Scalar‘𝐶) |
134 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶)) |
135 | 133, 26, 134, 34 | lmodvs0 18720 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ LMod ∧ (𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶))) → ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶)) =
(0g‘𝐶)) |
136 | 115, 132,
135 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶)) =
(0g‘𝐶)) |
137 | 113, 136 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))) = (0g‘𝐶)) |
138 | 8, 7, 75, 78, 137 | gsumsnd 18175 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝐶
Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) = (0g‘𝐶)) |
139 | 138 | eqcomd 2616 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(0g‘𝐶) =
(𝐶
Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) |
140 | 73, 139 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
((𝐶
Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))(+g‘𝐶)(0g‘𝐶)) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
141 | 36, 140 | eqtr3d 2646 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝐶
Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
142 | 141 | adantr 480 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
143 | 1, 142 | eqtrd 2644 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
144 | 143 | 3impa 1251 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
145 | 20 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) → 0
∈ ℕ0) |
146 | | simplll 794 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ (0...(0 + 1)))
→ 𝑁 ∈
Fin) |
147 | | simpllr 795 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ (0...(0 + 1)))
→ 𝑅 ∈
Ring) |
148 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝐺:{0}⟶𝐷 → 𝐺:{0}⟶𝐷) |
149 | | c0ex 9913 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
150 | 149 | snid 4155 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
{0} |
151 | 150 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐺:{0}⟶𝐷 → 0 ∈ {0}) |
152 | 148, 151 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (𝐺:{0}⟶𝐷 → (𝐺‘0) ∈ 𝐷) |
153 | 16, 152 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ (𝐷 ↑𝑚 {0}) →
(𝐺‘0) ∈ 𝐷) |
154 | 153 | ad2antlr 759 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑙 ∈ (0...1)) →
(𝐺‘0) ∈ 𝐷) |
155 | 23 | matring 20068 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
156 | 24, 93 | ring0cl 18392 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Ring → 0 ∈ 𝐷) |
157 | 155, 156 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 0 ∈ 𝐷) |
158 | 157 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑙 ∈ (0...1)) →
0 ∈
𝐷) |
159 | 154, 158 | ifcld 4081 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑙 ∈ (0...1)) →
if(𝑙 = 0, (𝐺‘0), 0 ) ∈ 𝐷) |
160 | 159, 42 | fmptd 6292 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
𝐻:(0...1)⟶𝐷) |
161 | 80 | oveq2i 6560 |
. . . . . . . . 9
⊢ (0...(0 +
1)) = (0...1) |
162 | 161 | feq2i 5950 |
. . . . . . . 8
⊢ (𝐻:(0...(0 + 1))⟶𝐷 ↔ 𝐻:(0...1)⟶𝐷) |
163 | 160, 162 | sylibr 223 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
𝐻:(0...(0 +
1))⟶𝐷) |
164 | 163 | ffvelrnda 6267 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ (0...(0 + 1)))
→ (𝐻‘𝑛) ∈ 𝐷) |
165 | | elfznn0 12302 |
. . . . . . 7
⊢ (𝑛 ∈ (0...(0 + 1)) →
𝑛 ∈
ℕ0) |
166 | 165 | adantl 481 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ (0...(0 + 1)))
→ 𝑛 ∈
ℕ0) |
167 | 23, 24, 25, 2, 3, 8,
26, 27, 28 | mat2pmatscmxcl 20364 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝐻‘𝑛) ∈ 𝐷 ∧ 𝑛 ∈ ℕ0)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))) ∈ 𝐵) |
168 | 146, 147,
164, 166, 167 | syl22anc 1319 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ (0...(0 + 1)))
→ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))) ∈ 𝐵) |
169 | 8, 33, 11, 145, 168 | gsummptfzsplit 18155 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝐶
Σg (𝑛 ∈ (0...(0 + 1)) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
170 | 169 | 3adant3 1074 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → (𝐶 Σg (𝑛 ∈ (0...(0 + 1)) ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
171 | 144, 170 | eqtr4d 2647 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...(0 + 1)) ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) |
172 | | mpteq1 4665 |
. . . 4
⊢ ((0...(0
+ 1)) = (0...1) → (𝑛
∈ (0...(0 + 1)) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))) = (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) |
173 | 161, 172 | ax-mp 5 |
. . 3
⊢ (𝑛 ∈ (0...(0 + 1)) ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))) = (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))) |
174 | 173 | oveq2i 6560 |
. 2
⊢ (𝐶 Σg
(𝑛 ∈ (0...(0 + 1))
↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) |
175 | 171, 174 | syl6eq 2660 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) |