Proof of Theorem pmatcollpw3fi1lem1
| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) |
| 2 | | pmatcollpw.p |
. . . . . . . . . . 11
⊢ 𝑃 = (Poly1‘𝑅) |
| 3 | | pmatcollpw.c |
. . . . . . . . . . 11
⊢ 𝐶 = (𝑁 Mat 𝑃) |
| 4 | 2, 3 | pmatring 22698 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
| 5 | | ringmnd 20240 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Ring → 𝐶 ∈ Mnd) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Mnd) |
| 7 | 6 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → 𝐶 ∈ Mnd) |
| 8 | | pmatcollpw.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐶) |
| 9 | | ringcmn 20279 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ Ring → 𝐶 ∈ CMnd) |
| 10 | 4, 9 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ CMnd) |
| 11 | 10 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → 𝐶 ∈ CMnd) |
| 12 | | snfi 9083 |
. . . . . . . . . 10
⊢ {0}
∈ Fin |
| 13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → {0} ∈
Fin) |
| 14 | | simplll 775 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) → 𝑁 ∈ Fin) |
| 15 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) → 𝑅 ∈ Ring) |
| 16 | | elmapi 8889 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ (𝐷 ↑m {0}) → 𝐺:{0}⟶𝐷) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → 𝐺:{0}⟶𝐷) |
| 18 | 17 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) → (𝐺‘𝑛) ∈ 𝐷) |
| 19 | | elsni 4643 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {0} → 𝑛 = 0) |
| 20 | | 0nn0 12541 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
| 21 | 19, 20 | eqeltrdi 2849 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ {0} → 𝑛 ∈
ℕ0) |
| 22 | 21 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {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 22746 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝐺‘𝑛) ∈ 𝐷 ∧ 𝑛 ∈ ℕ0)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))) ∈ 𝐵) |
| 30 | 14, 15, 18, 22, 29 | syl22anc 839 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))) ∈ 𝐵) |
| 31 | 30 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) →
∀𝑛 ∈ {0}
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))) ∈ 𝐵) |
| 32 | 8, 11, 13, 31 | gsummptcl 19985 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → (𝐶 Σg
(𝑛 ∈ {0} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) ∈ 𝐵) |
| 33 | | eqid 2737 |
. . . . . . . . 9
⊢
(+g‘𝐶) = (+g‘𝐶) |
| 34 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝐶) = (0g‘𝐶) |
| 35 | 8, 33, 34 | mndrid 18768 |
. . . . . . . 8
⊢ ((𝐶 ∈ Mnd ∧ (𝐶 Σg
(𝑛 ∈ {0} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) ∈ 𝐵) → ((𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))(+g‘𝐶)(0g‘𝐶)) = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) |
| 36 | 7, 32, 35 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → ((𝐶 Σg
(𝑛 ∈ {0} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))(+g‘𝐶)(0g‘𝐶)) = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) |
| 37 | | fz0sn 13667 |
. . . . . . . . . . . 12
⊢ (0...0) =
{0} |
| 38 | 37 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ {0} =
(0...0) |
| 39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → {0} =
(0...0)) |
| 40 | | pmatcollpw3fi1lem1.h |
. . . . . . . . . . . . . 14
⊢ 𝐻 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝐺‘0), 0 )) |
| 41 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → 𝑙 = 𝑛) |
| 42 | 19 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → 𝑛 = 0) |
| 43 | 41, 42 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → 𝑙 = 0) |
| 44 | 43 | iftrued 4533 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = (𝐺‘0)) |
| 45 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 0 → (𝐺‘𝑛) = (𝐺‘0)) |
| 46 | 45 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 → (𝐺‘0) = (𝐺‘𝑛)) |
| 47 | 19, 46 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ {0} → (𝐺‘0) = (𝐺‘𝑛)) |
| 48 | 47 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → (𝐺‘0) = (𝐺‘𝑛)) |
| 49 | 44, 48 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = (𝐺‘𝑛)) |
| 50 | | 1nn0 12542 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℕ0 |
| 51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 0 → 1 ∈
ℕ0) |
| 52 | | nn0uz 12920 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 = (ℤ≥‘0) |
| 53 | 51, 52 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 0 → 1 ∈
(ℤ≥‘0)) |
| 54 | | eluzfz1 13571 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
(ℤ≥‘0) → 0 ∈ (0...1)) |
| 55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 → 0 ∈
(0...1)) |
| 56 | | eleq1 2829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 → (𝑛 ∈ (0...1) ↔ 0 ∈
(0...1))) |
| 57 | 55, 56 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 0 → 𝑛 ∈ (0...1)) |
| 58 | 19, 57 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ {0} → 𝑛 ∈
(0...1)) |
| 59 | 58 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) → 𝑛 ∈
(0...1)) |
| 60 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺:{0}⟶𝐷 ∧ 𝑛 ∈ {0}) → (𝐺‘𝑛) ∈ 𝐷) |
| 61 | 60 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺:{0}⟶𝐷 → (𝑛 ∈ {0} → (𝐺‘𝑛) ∈ 𝐷)) |
| 62 | 16, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ (𝐷 ↑m {0}) → (𝑛 ∈ {0} → (𝐺‘𝑛) ∈ 𝐷)) |
| 63 | 62 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → (𝑛 ∈ {0} → (𝐺‘𝑛) ∈ 𝐷)) |
| 64 | 63 | imp 406 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) → (𝐺‘𝑛) ∈ 𝐷) |
| 65 | 40, 49, 59, 64 | fvmptd2 7024 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) → (𝐻‘𝑛) = (𝐺‘𝑛)) |
| 66 | 65 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) → (𝐺‘𝑛) = (𝐻‘𝑛)) |
| 67 | 66 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) → (𝑇‘(𝐺‘𝑛)) = (𝑇‘(𝐻‘𝑛))) |
| 68 | 67 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ {0}) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))) = ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))) |
| 69 | 39, 68 | mpteq12dva 5231 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))) = (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) |
| 70 | 69 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → (𝐶 Σg
(𝑛 ∈ {0} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) = (𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) |
| 71 | | ovexd 7466 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → (0 + 1)
∈ V) |
| 72 | 8, 34 | mndidcl 18762 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ Mnd →
(0g‘𝐶)
∈ 𝐵) |
| 73 | 6, 72 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝐶)
∈ 𝐵) |
| 74 | 73 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) →
(0g‘𝐶)
∈ 𝐵) |
| 75 | | 0p1e1 12388 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 + 1) =
1 |
| 76 | 75 | eqeq2i 2750 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (0 + 1) ↔ 𝑛 = 1) |
| 77 | | ax-1ne0 11224 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ≠
0 |
| 78 | 77 | neii 2942 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ¬ 1
= 0 |
| 79 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 1 → (𝑛 = 0 ↔ 1 = 0)) |
| 80 | 78, 79 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → ¬ 𝑛 = 0) |
| 81 | 76, 80 | sylbi 217 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = (0 + 1) → ¬ 𝑛 = 0) |
| 82 | 81 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → ¬ 𝑛 = 0) |
| 83 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑛 → (𝑙 = 0 ↔ 𝑛 = 0)) |
| 84 | 83 | notbid 318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑛 → (¬ 𝑙 = 0 ↔ ¬ 𝑛 = 0)) |
| 85 | 84 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → (¬ 𝑙 = 0 ↔ ¬ 𝑛 = 0)) |
| 86 | 82, 85 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → ¬ 𝑙 = 0) |
| 87 | 86 | iffalsed 4536 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) = 0 ) |
| 88 | | pmatcollpw3fi1lem1.0 |
. . . . . . . . . . . . . . . 16
⊢ 0 =
(0g‘𝐴) |
| 89 | 87, 88 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, (𝐺‘0), 0 ) =
(0g‘𝐴)) |
| 90 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → 1 ∈
ℕ0) |
| 91 | 90, 52 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → 1 ∈
(ℤ≥‘0)) |
| 92 | | eluzfz2 13572 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
(ℤ≥‘0) → 1 ∈ (0...1)) |
| 93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → 1 ∈
(0...1)) |
| 94 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → (𝑛 ∈ (0...1) ↔ 1 ∈
(0...1))) |
| 95 | 93, 94 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → 𝑛 ∈ (0...1)) |
| 96 | 76, 95 | sylbi 217 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (0 + 1) → 𝑛 ∈
(0...1)) |
| 97 | 96 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → 𝑛 ∈
(0...1)) |
| 98 | | fvexd 6921 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) →
(0g‘𝐴)
∈ V) |
| 99 | 40, 89, 97, 98 | fvmptd2 7024 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → (𝐻‘𝑛) = (0g‘𝐴)) |
| 100 | 99 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → (𝑇‘(𝐻‘𝑛)) = (𝑇‘(0g‘𝐴))) |
| 101 | 23 | fveq2i 6909 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐴) = (0g‘(𝑁 Mat 𝑅)) |
| 102 | 3 | fveq2i 6909 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐶) = (0g‘(𝑁 Mat 𝑃)) |
| 103 | 25, 2, 101, 102 | 0mat2pmat 22742 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
| 104 | 103 | ancoms 458 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
| 105 | 104 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → (𝑇‘(0g‘𝐴)) = (0g‘𝐶)) |
| 106 | 100, 105 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → (𝑇‘(𝐻‘𝑛)) = (0g‘𝐶)) |
| 107 | 106 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))) = ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶))) |
| 108 | 2, 3 | pmatlmod 22699 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ LMod) |
| 109 | 108 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → 𝐶 ∈ LMod) |
| 110 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → 𝑅 ∈ Ring) |
| 111 | | eleq1 2829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → (𝑛 ∈ ℕ0 ↔ 1 ∈
ℕ0)) |
| 112 | 90, 111 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 1 → 𝑛 ∈ ℕ0) |
| 113 | 76, 112 | sylbi 217 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (0 + 1) → 𝑛 ∈
ℕ0) |
| 114 | 113 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → 𝑛 ∈
ℕ0) |
| 115 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
| 116 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑃) =
(Base‘𝑃) |
| 117 | 2, 28, 115, 27, 116 | ply1moncl 22274 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃)) |
| 118 | 110, 114,
117 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → (𝑛 ↑ 𝑋) ∈ (Base‘𝑃)) |
| 119 | 2 | ply1ring 22249 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
| 120 | 3 | matsca2 22426 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) → 𝑃 = (Scalar‘𝐶)) |
| 121 | 119, 120 | sylan2 593 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑃 = (Scalar‘𝐶)) |
| 122 | 121 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Scalar‘𝐶) = 𝑃) |
| 123 | 122 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘(Scalar‘𝐶)) = (Base‘𝑃)) |
| 124 | 123 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶)) ↔ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃))) |
| 125 | 124 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → ((𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶)) ↔ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃))) |
| 126 | 118, 125 | mpbird 257 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → (𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶))) |
| 127 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Scalar‘𝐶) =
(Scalar‘𝐶) |
| 128 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶)) |
| 129 | 127, 26, 128, 34 | lmodvs0 20894 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ LMod ∧ (𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶))) → ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶)) =
(0g‘𝐶)) |
| 130 | 109, 126,
129 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶)) =
(0g‘𝐶)) |
| 131 | 107, 130 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 = (0 + 1)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))) = (0g‘𝐶)) |
| 132 | 8, 7, 71, 74, 131 | gsumsnd 19970 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → (𝐶 Σg
(𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) = (0g‘𝐶)) |
| 133 | 132 | eqcomd 2743 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) →
(0g‘𝐶) =
(𝐶
Σg (𝑛 ∈ {(0 + 1)} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) |
| 134 | 70, 133 | oveq12d 7449 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → ((𝐶 Σg
(𝑛 ∈ {0} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))(+g‘𝐶)(0g‘𝐶)) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
| 135 | 36, 134 | eqtr3d 2779 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → (𝐶 Σg
(𝑛 ∈ {0} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
| 136 | 135 | adantr 480 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
| 137 | 1, 136 | eqtrd 2777 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
| 138 | 137 | 3impa 1110 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
| 139 | 20 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → 0 ∈
ℕ0) |
| 140 | | simplll 775 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ (0...(0 + 1))) →
𝑁 ∈
Fin) |
| 141 | | simpllr 776 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ (0...(0 + 1))) →
𝑅 ∈
Ring) |
| 142 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝐺:{0}⟶𝐷 → 𝐺:{0}⟶𝐷) |
| 143 | | c0ex 11255 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
| 144 | 143 | snid 4662 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
{0} |
| 145 | 144 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐺:{0}⟶𝐷 → 0 ∈ {0}) |
| 146 | 142, 145 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (𝐺:{0}⟶𝐷 → (𝐺‘0) ∈ 𝐷) |
| 147 | 16, 146 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ (𝐷 ↑m {0}) → (𝐺‘0) ∈ 𝐷) |
| 148 | 147 | ad2antlr 727 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑙 ∈ (0...1)) → (𝐺‘0) ∈ 𝐷) |
| 149 | 23 | matring 22449 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
| 150 | 24, 88 | ring0cl 20264 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Ring → 0 ∈ 𝐷) |
| 151 | 149, 150 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 0 ∈ 𝐷) |
| 152 | 151 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑙 ∈ (0...1)) → 0 ∈ 𝐷) |
| 153 | 148, 152 | ifcld 4572 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑙 ∈ (0...1)) → if(𝑙 = 0, (𝐺‘0), 0 ) ∈ 𝐷) |
| 154 | 153, 40 | fmptd 7134 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → 𝐻:(0...1)⟶𝐷) |
| 155 | 75 | oveq2i 7442 |
. . . . . . . . 9
⊢ (0...(0 +
1)) = (0...1) |
| 156 | 155 | feq2i 6728 |
. . . . . . . 8
⊢ (𝐻:(0...(0 + 1))⟶𝐷 ↔ 𝐻:(0...1)⟶𝐷) |
| 157 | 154, 156 | sylibr 234 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → 𝐻:(0...(0 + 1))⟶𝐷) |
| 158 | 157 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ (0...(0 + 1))) →
(𝐻‘𝑛) ∈ 𝐷) |
| 159 | | elfznn0 13660 |
. . . . . . 7
⊢ (𝑛 ∈ (0...(0 + 1)) →
𝑛 ∈
ℕ0) |
| 160 | 159 | adantl 481 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ (0...(0 + 1))) →
𝑛 ∈
ℕ0) |
| 161 | 23, 24, 25, 2, 3, 8,
26, 27, 28 | mat2pmatscmxcl 22746 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝐻‘𝑛) ∈ 𝐷 ∧ 𝑛 ∈ ℕ0)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))) ∈ 𝐵) |
| 162 | 140, 141,
158, 160, 161 | syl22anc 839 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) ∧ 𝑛 ∈ (0...(0 + 1))) →
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))) ∈ 𝐵) |
| 163 | 8, 33, 11, 139, 162 | gsummptfzsplit 19950 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0})) → (𝐶 Σg
(𝑛 ∈ (0...(0 + 1))
↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
| 164 | 163 | 3adant3 1133 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → (𝐶 Σg (𝑛 ∈ (0...(0 + 1)) ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) = ((𝐶 Σg (𝑛 ∈ (0...0) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))(+g‘𝐶)(𝐶 Σg (𝑛 ∈ {(0 + 1)} ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))) |
| 165 | 138, 164 | eqtr4d 2780 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...(0 + 1)) ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) |
| 166 | 155 | mpteq1i 5238 |
. . 3
⊢ (𝑛 ∈ (0...(0 + 1)) ↦
((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))) = (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))) |
| 167 | 166 | oveq2i 7442 |
. 2
⊢ (𝐶 Σg
(𝑛 ∈ (0...(0 + 1))
↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))) |
| 168 | 165, 167 | eqtrdi 2793 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑m {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) |