Proof of Theorem pmatcollpw3fi1lem1
Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) |
2 | | pmatcollpw.p |
. . . . . . . . . . 11
⊢ 𝑃 = (Poly1‘𝑅) |
3 | | pmatcollpw.c |
. . . . . . . . . . 11
⊢ 𝐶 = (𝑁 Mat 𝑃) |
4 | 2, 3 | pmatring 20498 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
5 | | ringmnd 18556 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Ring → 𝐶 ∈ Mnd) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Mnd) |
7 | 6 | adantr 481 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
𝐶 ∈
Mnd) |
8 | | pmatcollpw.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐶) |
9 | | ringcmn 18581 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ Ring → 𝐶 ∈ CMnd) |
10 | 4, 9 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ CMnd) |
11 | 10 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
𝐶 ∈
CMnd) |
12 | | snfi 8038 |
. . . . . . . . . 10
⊢ {0}
∈ Fin |
13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) → {0}
∈ Fin) |
14 | | simplll 798 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → 𝑁 ∈ Fin) |
15 | | simpllr 799 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → 𝑅 ∈ Ring) |
16 | | elmapi 7879 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ (𝐷 ↑𝑚 {0}) →
𝐺:{0}⟶𝐷) |
17 | 16 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
𝐺:{0}⟶𝐷) |
18 | 17 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → (𝐺‘𝑛) ∈ 𝐷) |
19 | | elsni 4194 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {0} → 𝑛 = 0) |
20 | | 0nn0 11307 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
21 | 19, 20 | syl6eqel 2709 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ {0} → 𝑛 ∈
ℕ0) |
22 | 21 | adantl 482 |
. . . . . . . . . . 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 20545 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝐺‘𝑛) ∈ 𝐷 ∧ 𝑛 ∈ ℕ0)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))) ∈ 𝐵) |
30 | 14, 15, 18, 22, 29 | syl22anc 1327 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) →
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))) ∈ 𝐵) |
31 | 30 | ralrimiva 2966 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
∀𝑛 ∈ {0}
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))) ∈ 𝐵) |
32 | 8, 11, 13, 31 | gsummptcl 18366 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝐶
Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) ∈ 𝐵) |
33 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘𝐶) = (+g‘𝐶) |
34 | | eqid 2622 |
. . . . . . . . 9
⊢
(0g‘𝐶) = (0g‘𝐶) |
35 | 8, 33, 34 | mndrid 17312 |
. . . . . . . 8
⊢ ((𝐶 ∈ Mnd ∧ (𝐶 Σg
(𝑛 ∈ {0} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) ∈ 𝐵) → ((𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))(+g‘𝐶)(0g‘𝐶)) = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) |
36 | 7, 32, 35 | syl2anc 693 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
((𝐶
Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))(+g‘𝐶)(0g‘𝐶)) = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) |
37 | | 0z 11388 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℤ |
38 | | fzsn 12383 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℤ → (0...0) = {0}) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (0...0) =
{0} |
40 | 39 | eqcomi 2631 |
. . . . . . . . . . 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 477 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → 𝑙 = 𝑛) |
45 | 19 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → 𝑛 = 0) |
46 | 44, 45 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → 𝑙 = 0) |
47 | 46 | iftrued 4094 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = (𝐺‘0)) |
48 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 0 → (𝐺‘𝑛) = (𝐺‘0)) |
49 | 48 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 → (𝐺‘0) = (𝐺‘𝑛)) |
50 | 19, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ {0} → (𝐺‘0) = (𝐺‘𝑛)) |
51 | 50 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → (𝐺‘0) = (𝐺‘𝑛)) |
52 | 47, 51 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = (𝐺‘𝑛)) |
53 | | 1nn0 11308 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℕ0 |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 0 → 1 ∈
ℕ0) |
55 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 = (ℤ≥‘0) |
56 | 54, 55 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 0 → 1 ∈
(ℤ≥‘0)) |
57 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
(ℤ≥‘0) → 0 ∈ (0...1)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 → 0 ∈
(0...1)) |
59 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 → (𝑛 ∈ (0...1) ↔ 0 ∈
(0...1))) |
60 | 58, 59 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 0 → 𝑛 ∈ (0...1)) |
61 | 19, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ {0} → 𝑛 ∈
(0...1)) |
62 | 61 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → 𝑛 ∈
(0...1)) |
63 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺:{0}⟶𝐷 ∧ 𝑛 ∈ {0}) → (𝐺‘𝑛) ∈ 𝐷) |
64 | 63 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺:{0}⟶𝐷 → (𝑛 ∈ {0} → (𝐺‘𝑛) ∈ 𝐷)) |
65 | 16, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ (𝐷 ↑𝑚 {0}) →
(𝑛 ∈ {0} → (𝐺‘𝑛) ∈ 𝐷)) |
66 | 65 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝑛 ∈ {0} → (𝐺‘𝑛) ∈ 𝐷)) |
67 | 66 | imp 445 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → (𝐺‘𝑛) ∈ 𝐷) |
68 | 43, 52, 62, 67 | fvmptd 6288 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → (𝐻‘𝑛) = (𝐺‘𝑛)) |
69 | 68 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → (𝐺‘𝑛) = (𝐻‘𝑛)) |
70 | 69 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) → (𝑇‘(𝐺‘𝑛)) = (𝑇‘(𝐻‘𝑛))) |
71 | 70 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ {0}) →
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))) = ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))) |
72 | 41, 71 | mpteq12dva 4732 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝑛 ∈ {0} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))) = (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) |
73 | 72 | oveq2d 6666 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝐶
Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) = (𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) |
74 | | ovexd 6680 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) → (0
+ 1) ∈ V) |
75 | 8, 34 | mndidcl 17308 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ Mnd →
(0g‘𝐶)
∈ 𝐵) |
76 | 6, 75 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝐶)
∈ 𝐵) |
77 | 76 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(0g‘𝐶)
∈ 𝐵) |
78 | 42 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → 𝐻 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝐺‘0), 0 ))) |
79 | | 0p1e1 11132 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 + 1) =
1 |
80 | 79 | eqeq2i 2634 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (0 + 1) ↔ 𝑛 = 1) |
81 | | ax-1ne0 10005 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ≠
0 |
82 | 81 | neii 2796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ¬ 1
= 0 |
83 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 1 → (𝑛 = 0 ↔ 1 = 0)) |
84 | 82, 83 | mtbiri 317 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → ¬ 𝑛 = 0) |
85 | 80, 84 | sylbi 207 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = (0 + 1) → ¬ 𝑛 = 0) |
86 | 85 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → ¬ 𝑛 = 0) |
87 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑛 → (𝑙 = 0 ↔ 𝑛 = 0)) |
88 | 87 | notbid 308 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑛 → (¬ 𝑙 = 0 ↔ ¬ 𝑛 = 0)) |
89 | 88 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → (¬ 𝑙 = 0 ↔ ¬ 𝑛 = 0)) |
90 | 86, 89 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → ¬ 𝑙 = 0) |
91 | 90 | iffalsed 4097 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = 0 ) |
92 | | pmatcollpw3fi1lem1.0 |
. . . . . . . . . . . . . . . 16
⊢ 0 =
(0g‘𝐴) |
93 | 91, 92 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) =
(0g‘𝐴)) |
94 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → 1 ∈
ℕ0) |
95 | 94, 55 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → 1 ∈
(ℤ≥‘0)) |
96 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
(ℤ≥‘0) → 1 ∈ (0...1)) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → 1 ∈
(0...1)) |
98 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → (𝑛 ∈ (0...1) ↔ 1 ∈
(0...1))) |
99 | 97, 98 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → 𝑛 ∈ (0...1)) |
100 | 80, 99 | sylbi 207 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (0 + 1) → 𝑛 ∈
(0...1)) |
101 | 100 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → 𝑛 ∈
(0...1)) |
102 | | fvexd 6203 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) →
(0g‘𝐴)
∈ V) |
103 | 78, 93, 101, 102 | fvmptd 6288 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → (𝐻‘𝑛) = (0g‘𝐴)) |
104 | 103 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → (𝑇‘(𝐻‘𝑛)) = (𝑇‘(0g‘𝐴))) |
105 | 23 | fveq2i 6194 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐴) = (0g‘(𝑁 Mat 𝑅)) |
106 | 3 | fveq2i 6194 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐶) = (0g‘(𝑁 Mat 𝑃)) |
107 | 25, 2, 105, 106 | 0mat2pmat 20541 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
108 | 107 | ancoms 469 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
109 | 108 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
110 | 104, 109 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → (𝑇‘(𝐻‘𝑛)) = (0g‘𝐶)) |
111 | 110 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))) = ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶))) |
112 | 2, 3 | pmatlmod 20499 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ LMod) |
113 | 112 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → 𝐶 ∈ LMod) |
114 | | simpllr 799 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → 𝑅 ∈ Ring) |
115 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → (𝑛 ∈ ℕ0 ↔ 1 ∈
ℕ0)) |
116 | 94, 115 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 1 → 𝑛 ∈ ℕ0) |
117 | 80, 116 | sylbi 207 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (0 + 1) → 𝑛 ∈
ℕ0) |
118 | 117 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → 𝑛 ∈
ℕ0) |
119 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
120 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑃) =
(Base‘𝑃) |
121 | 2, 28, 119, 27, 120 | ply1moncl 19641 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃)) |
122 | 114, 118,
121 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → (𝑛 ↑ 𝑋) ∈ (Base‘𝑃)) |
123 | 2 | ply1ring 19618 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
124 | 3 | matsca2 20226 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) → 𝑃 = (Scalar‘𝐶)) |
125 | 123, 124 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑃 = (Scalar‘𝐶)) |
126 | 125 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Scalar‘𝐶) = 𝑃) |
127 | 126 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘(Scalar‘𝐶)) = (Base‘𝑃)) |
128 | 127 | eleq2d 2687 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶)) ↔ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃))) |
129 | 128 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → ((𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶)) ↔ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃))) |
130 | 122, 129 | mpbird 247 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → (𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶))) |
131 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(Scalar‘𝐶) =
(Scalar‘𝐶) |
132 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶)) |
133 | 131, 26, 132, 34 | lmodvs0 18897 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ LMod ∧ (𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶))) → ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶)) =
(0g‘𝐶)) |
134 | 113, 130,
133 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶)) =
(0g‘𝐶)) |
135 | 111, 134 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 = (0 + 1)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))) = (0g‘𝐶)) |
136 | 8, 7, 74, 77, 135 | gsumsnd 18352 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝐶
Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) = (0g‘𝐶)) |
137 | 136 | eqcomd 2628 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(0g‘𝐶) =
(𝐶
Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) |
138 | 73, 137 | oveq12d 6668 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
((𝐶
Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))(+g‘𝐶)(0g‘𝐶)) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
139 | 36, 138 | eqtr3d 2658 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝐶
Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
140 | 139 | adantr 481 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
141 | 1, 140 | eqtrd 2656 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
142 | 141 | 3impa 1259 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
143 | 20 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) → 0
∈ ℕ0) |
144 | | simplll 798 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ (0...(0 + 1)))
→ 𝑁 ∈
Fin) |
145 | | simpllr 799 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ (0...(0 + 1)))
→ 𝑅 ∈
Ring) |
146 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝐺:{0}⟶𝐷 → 𝐺:{0}⟶𝐷) |
147 | | c0ex 10034 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
148 | 147 | snid 4208 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
{0} |
149 | 148 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐺:{0}⟶𝐷 → 0 ∈ {0}) |
150 | 146, 149 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ (𝐺:{0}⟶𝐷 → (𝐺‘0) ∈ 𝐷) |
151 | 16, 150 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ (𝐷 ↑𝑚 {0}) →
(𝐺‘0) ∈ 𝐷) |
152 | 151 | ad2antlr 763 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑙 ∈ (0...1)) →
(𝐺‘0) ∈ 𝐷) |
153 | 23 | matring 20249 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
154 | 24, 92 | ring0cl 18569 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Ring → 0 ∈ 𝐷) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 0 ∈ 𝐷) |
156 | 155 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑙 ∈ (0...1)) →
0 ∈
𝐷) |
157 | 152, 156 | ifcld 4131 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑙 ∈ (0...1)) →
if(𝑙 = 0, (𝐺‘0), 0 ) ∈ 𝐷) |
158 | 157, 42 | fmptd 6385 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
𝐻:(0...1)⟶𝐷) |
159 | 79 | oveq2i 6661 |
. . . . . . . . 9
⊢ (0...(0 +
1)) = (0...1) |
160 | 159 | feq2i 6037 |
. . . . . . . 8
⊢ (𝐻:(0...(0 + 1))⟶𝐷 ↔ 𝐻:(0...1)⟶𝐷) |
161 | 158, 160 | sylibr 224 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
𝐻:(0...(0 +
1))⟶𝐷) |
162 | 161 | ffvelrnda 6359 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ (0...(0 + 1)))
→ (𝐻‘𝑛) ∈ 𝐷) |
163 | | elfznn0 12433 |
. . . . . . 7
⊢ (𝑛 ∈ (0...(0 + 1)) →
𝑛 ∈
ℕ0) |
164 | 163 | adantl 482 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ (0...(0 + 1)))
→ 𝑛 ∈
ℕ0) |
165 | 23, 24, 25, 2, 3, 8,
26, 27, 28 | mat2pmatscmxcl 20545 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝐻‘𝑛) ∈ 𝐷 ∧ 𝑛 ∈ ℕ0)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))) ∈ 𝐵) |
166 | 144, 145,
162, 164, 165 | syl22anc 1327 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑛 ∈ (0...(0 + 1)))
→ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))) ∈ 𝐵) |
167 | 8, 33, 11, 143, 166 | gsummptfzsplit 18332 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0})) →
(𝐶
Σg (𝑛 ∈ (0...(0 + 1)) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
168 | 167 | 3adant3 1081 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → (𝐶 Σg (𝑛 ∈ (0...(0 + 1)) ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
169 | 142, 168 | eqtr4d 2659 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...(0 + 1)) ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) |
170 | | mpteq1 4737 |
. . . 4
⊢ ((0...(0
+ 1)) = (0...1) → (𝑛
∈ (0...(0 + 1)) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))) = (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) |
171 | 159, 170 | ax-mp 5 |
. . 3
⊢ (𝑛 ∈ (0...(0 + 1)) ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))) = (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))) |
172 | 171 | oveq2i 6661 |
. 2
⊢ (𝐶 Σg
(𝑛 ∈ (0...(0 + 1))
↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) |
173 | 169, 172 | syl6eq 2672 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) |