Step | Hyp | Ref
| Expression |
1 | | eqid 2740 |
. . . . 5
⊢
(Poly1‘𝐴) = (Poly1‘𝐴) |
2 | | eqid 2740 |
. . . . 5
⊢
(var1‘𝐴) = (var1‘𝐴) |
3 | | eqid 2740 |
. . . . 5
⊢
(.g‘(mulGrp‘(Poly1‘𝐴))) =
(.g‘(mulGrp‘(Poly1‘𝐴))) |
4 | | crngring 19806 |
. . . . . . . 8
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
5 | | chcoeffeq.a |
. . . . . . . . 9
⊢ 𝐴 = (𝑁 Mat 𝑅) |
6 | 5 | matring 21603 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
7 | 4, 6 | sylan2 593 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring) |
8 | 7 | 3adant3 1131 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ Ring) |
9 | 8 | adantr 481 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐴 ∈ Ring) |
10 | | chcoeffeq.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐴) |
11 | | eqid 2740 |
. . . . 5
⊢ (
·𝑠 ‘(Poly1‘𝐴)) = (
·𝑠 ‘(Poly1‘𝐴)) |
12 | | eqid 2740 |
. . . . 5
⊢
(0g‘𝐴) = (0g‘𝐴) |
13 | | chcoeffeq.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
14 | | chcoeffeq.y |
. . . . . . . 8
⊢ 𝑌 = (𝑁 Mat 𝑃) |
15 | | chcoeffeq.t |
. . . . . . . 8
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
16 | | chcoeffeq.r |
. . . . . . . 8
⊢ × =
(.r‘𝑌) |
17 | | chcoeffeq.s |
. . . . . . . 8
⊢ − =
(-g‘𝑌) |
18 | | chcoeffeq.0 |
. . . . . . . 8
⊢ 0 =
(0g‘𝑌) |
19 | | chcoeffeq.g |
. . . . . . . 8
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) |
20 | | eqid 2740 |
. . . . . . . 8
⊢ (𝑁 ConstPolyMat 𝑅) = (𝑁 ConstPolyMat 𝑅) |
21 | | eqid 2740 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌) |
22 | | eqid 2740 |
. . . . . . . 8
⊢
(1r‘𝑌) = (1r‘𝑌) |
23 | | eqid 2740 |
. . . . . . . 8
⊢
(var1‘𝑅) = (var1‘𝑅) |
24 | | eqid 2740 |
. . . . . . . 8
⊢
(((var1‘𝑅)( ·𝑠
‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) = (((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) |
25 | | eqid 2740 |
. . . . . . . 8
⊢ (𝑁 maAdju 𝑃) = (𝑁 maAdju 𝑃) |
26 | | chcoeffeq.w |
. . . . . . . 8
⊢ 𝑊 = (Base‘𝑌) |
27 | | chcoeffeq.u |
. . . . . . . 8
⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) |
28 | 5, 10, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 1, 2, 11, 3, 27 | cpmadumatpolylem1 22041 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑈 ∘ 𝐺) ∈ (𝐵 ↑m
ℕ0)) |
29 | 28 | anasss 467 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑈 ∘ 𝐺) ∈ (𝐵 ↑m
ℕ0)) |
30 | 5, 10, 13, 14, 16, 17, 18, 15, 19, 20 | chfacfisfcpmat 22015 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)) |
31 | 4, 30 | syl3anl2 1412 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)) |
32 | 31 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ (𝑈 ∘ 𝐺) ∈ (𝐵 ↑m ℕ0))
→ 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)) |
33 | | fvco3 6864 |
. . . . . . . . . 10
⊢ ((𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅) ∧ 𝑙 ∈ ℕ0) → ((𝑈 ∘ 𝐺)‘𝑙) = (𝑈‘(𝐺‘𝑙))) |
34 | 33 | eqcomd 2746 |
. . . . . . . . 9
⊢ ((𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅) ∧ 𝑙 ∈ ℕ0) → (𝑈‘(𝐺‘𝑙)) = ((𝑈 ∘ 𝐺)‘𝑙)) |
35 | 32, 34 | sylan 580 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ (𝑈 ∘ 𝐺) ∈ (𝐵 ↑m ℕ0))
∧ 𝑙 ∈
ℕ0) → (𝑈‘(𝐺‘𝑙)) = ((𝑈 ∘ 𝐺)‘𝑙)) |
36 | | elmapi 8629 |
. . . . . . . . . 10
⊢ ((𝑈 ∘ 𝐺) ∈ (𝐵 ↑m ℕ0)
→ (𝑈 ∘ 𝐺):ℕ0⟶𝐵) |
37 | 36 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ (𝑈 ∘ 𝐺) ∈ (𝐵 ↑m ℕ0))
→ (𝑈 ∘ 𝐺):ℕ0⟶𝐵) |
38 | 37 | ffvelrnda 6958 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ (𝑈 ∘ 𝐺) ∈ (𝐵 ↑m ℕ0))
∧ 𝑙 ∈
ℕ0) → ((𝑈 ∘ 𝐺)‘𝑙) ∈ 𝐵) |
39 | 35, 38 | eqeltrd 2841 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ (𝑈 ∘ 𝐺) ∈ (𝐵 ↑m ℕ0))
∧ 𝑙 ∈
ℕ0) → (𝑈‘(𝐺‘𝑙)) ∈ 𝐵) |
40 | 39 | ralrimiva 3110 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ (𝑈 ∘ 𝐺) ∈ (𝐵 ↑m ℕ0))
→ ∀𝑙 ∈
ℕ0 (𝑈‘(𝐺‘𝑙)) ∈ 𝐵) |
41 | 29, 40 | mpdan 684 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ∀𝑙 ∈ ℕ0 (𝑈‘(𝐺‘𝑙)) ∈ 𝐵) |
42 | 4 | anim2i 617 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
43 | 42 | 3adant3 1131 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
44 | 43 | adantr 481 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
45 | 5, 10, 20, 27 | cpm2mf 21912 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵) |
47 | | fcompt 7002 |
. . . . . . 7
⊢ ((𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵 ∧ 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)) → (𝑈 ∘ 𝐺) = (𝑙 ∈ ℕ0 ↦ (𝑈‘(𝐺‘𝑙)))) |
48 | 46, 31, 47 | syl2anc 584 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑈 ∘ 𝐺) = (𝑙 ∈ ℕ0 ↦ (𝑈‘(𝐺‘𝑙)))) |
49 | 5, 10, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 1, 2, 11, 3, 27 | cpmadumatpolylem2 22042 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑈 ∘ 𝐺) finSupp (0g‘𝐴)) |
50 | 49 | anasss 467 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑈 ∘ 𝐺) finSupp (0g‘𝐴)) |
51 | 48, 50 | eqbrtrrd 5103 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑙 ∈ ℕ0 ↦ (𝑈‘(𝐺‘𝑙))) finSupp (0g‘𝐴)) |
52 | | simpll1 1211 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑙 ∈ ℕ0) → 𝑁 ∈ Fin) |
53 | 4 | 3ad2ant2 1133 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
54 | 53 | ad2antrr 723 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑙 ∈ ℕ0) → 𝑅 ∈ Ring) |
55 | | chcoeffeq.k |
. . . . . . . . . 10
⊢ 𝐾 = (𝐶‘𝑀) |
56 | | chcoeffeq.c |
. . . . . . . . . . 11
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
57 | | eqid 2740 |
. . . . . . . . . . 11
⊢
(Base‘𝑃) =
(Base‘𝑃) |
58 | 56, 5, 10, 13, 57 | chpmatply1 21992 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) ∈ (Base‘𝑃)) |
59 | 55, 58 | eqeltrid 2845 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐾 ∈ (Base‘𝑃)) |
60 | | eqid 2740 |
. . . . . . . . . 10
⊢
(coe1‘𝐾) = (coe1‘𝐾) |
61 | | eqid 2740 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
62 | 60, 57, 13, 61 | coe1fvalcl 21394 |
. . . . . . . . 9
⊢ ((𝐾 ∈ (Base‘𝑃) ∧ 𝑙 ∈ ℕ0) →
((coe1‘𝐾)‘𝑙) ∈ (Base‘𝑅)) |
63 | 59, 62 | sylan 580 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) →
((coe1‘𝐾)‘𝑙) ∈ (Base‘𝑅)) |
64 | 63 | adantlr 712 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑙 ∈ ℕ0) →
((coe1‘𝐾)‘𝑙) ∈ (Base‘𝑅)) |
65 | | chcoeffeq.1 |
. . . . . . . . . 10
⊢ 1 =
(1r‘𝐴) |
66 | 10, 65 | ringidcl 19818 |
. . . . . . . . 9
⊢ (𝐴 ∈ Ring → 1 ∈ 𝐵) |
67 | 8, 66 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 1 ∈ 𝐵) |
68 | 67 | ad2antrr 723 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑙 ∈ ℕ0) → 1 ∈ 𝐵) |
69 | | chcoeffeq.m |
. . . . . . . 8
⊢ ∗ = (
·𝑠 ‘𝐴) |
70 | 61, 5, 10, 69 | matvscl 21591 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧
(((coe1‘𝐾)‘𝑙) ∈ (Base‘𝑅) ∧ 1 ∈ 𝐵)) → (((coe1‘𝐾)‘𝑙) ∗ 1 ) ∈ 𝐵) |
71 | 52, 54, 64, 68, 70 | syl22anc 836 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑙 ∈ ℕ0) →
(((coe1‘𝐾)‘𝑙) ∗ 1 ) ∈ 𝐵) |
72 | 71 | ralrimiva 3110 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ∀𝑙 ∈ ℕ0
(((coe1‘𝐾)‘𝑙) ∗ 1 ) ∈ 𝐵) |
73 | | nn0ex 12250 |
. . . . . . 7
⊢
ℕ0 ∈ V |
74 | 73 | a1i 11 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ℕ0 ∈
V) |
75 | 5 | matlmod 21589 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) |
76 | 4, 75 | sylan2 593 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ LMod) |
77 | 76 | 3adant3 1131 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ LMod) |
78 | 77 | adantr 481 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐴 ∈ LMod) |
79 | | eqidd 2741 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (Scalar‘𝐴) = (Scalar‘𝐴)) |
80 | | fvexd 6786 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑙 ∈ ℕ0) →
((coe1‘𝐾)‘𝑙) ∈ V) |
81 | | eqid 2740 |
. . . . . 6
⊢
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐴)) |
82 | 5 | matsca2 21580 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 = (Scalar‘𝐴)) |
83 | 82 | 3adant3 1131 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 = (Scalar‘𝐴)) |
84 | 83, 53 | eqeltrrd 2842 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝐴) ∈ Ring) |
85 | 83 | eqcomd 2746 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝐴) = 𝑅) |
86 | 85 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) →
(Poly1‘(Scalar‘𝐴)) = (Poly1‘𝑅)) |
87 | 86, 13 | eqtr4di 2798 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) →
(Poly1‘(Scalar‘𝐴)) = 𝑃) |
88 | 87 | fveq2d 6775 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) →
(Base‘(Poly1‘(Scalar‘𝐴))) = (Base‘𝑃)) |
89 | 59, 88 | eleqtrrd 2844 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐾 ∈
(Base‘(Poly1‘(Scalar‘𝐴)))) |
90 | | eqid 2740 |
. . . . . . . . 9
⊢
(Poly1‘(Scalar‘𝐴)) =
(Poly1‘(Scalar‘𝐴)) |
91 | | eqid 2740 |
. . . . . . . . 9
⊢
(Base‘(Poly1‘(Scalar‘𝐴))) =
(Base‘(Poly1‘(Scalar‘𝐴))) |
92 | 90, 91, 81 | mptcoe1fsupp 21397 |
. . . . . . . 8
⊢
(((Scalar‘𝐴)
∈ Ring ∧ 𝐾 ∈
(Base‘(Poly1‘(Scalar‘𝐴)))) → (𝑙 ∈ ℕ0 ↦
((coe1‘𝐾)‘𝑙)) finSupp
(0g‘(Scalar‘𝐴))) |
93 | 84, 89, 92 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑙 ∈ ℕ0 ↦
((coe1‘𝐾)‘𝑙)) finSupp
(0g‘(Scalar‘𝐴))) |
94 | 93 | adantr 481 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑙 ∈ ℕ0 ↦
((coe1‘𝐾)‘𝑙)) finSupp
(0g‘(Scalar‘𝐴))) |
95 | 74, 78, 79, 10, 80, 68, 12, 81, 69, 94 | mptscmfsupp0 20199 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑙 ∈ ℕ0 ↦
(((coe1‘𝐾)‘𝑙) ∗ 1 )) finSupp
(0g‘𝐴)) |
96 | | 2fveq3 6776 |
. . . . . . . . 9
⊢ (𝑛 = 𝑙 → (𝑈‘(𝐺‘𝑛)) = (𝑈‘(𝐺‘𝑙))) |
97 | | oveq1 7279 |
. . . . . . . . 9
⊢ (𝑛 = 𝑙 → (𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)) = (𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))) |
98 | 96, 97 | oveq12d 7290 |
. . . . . . . 8
⊢ (𝑛 = 𝑙 → ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))) = ((𝑈‘(𝐺‘𝑙))(
·𝑠 ‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))) |
99 | 98 | cbvmptv 5192 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))) = (𝑙
∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑙))(
·𝑠 ‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))) |
100 | 99 | oveq2i 7283 |
. . . . . 6
⊢
((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0
↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑙 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑙))(
·𝑠 ‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) |
101 | 100 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑙 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑙))(
·𝑠 ‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) |
102 | | fveq2 6771 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑙 → ((coe1‘𝐾)‘𝑛) = ((coe1‘𝐾)‘𝑙)) |
103 | 102 | oveq1d 7287 |
. . . . . . . . 9
⊢ (𝑛 = 𝑙 → (((coe1‘𝐾)‘𝑛) ∗ 1 ) =
(((coe1‘𝐾)‘𝑙) ∗ 1 )) |
104 | 103, 97 | oveq12d 7290 |
. . . . . . . 8
⊢ (𝑛 = 𝑙 → ((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))) = ((((coe1‘𝐾)‘𝑙)
∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))) |
105 | 104 | cbvmptv 5192 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ ((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))) = (𝑙
∈ ℕ0 ↦ ((((coe1‘𝐾)‘𝑙)
∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))) |
106 | 105 | oveq2i 7283 |
. . . . . 6
⊢
((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0
↦ ((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑙 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑙) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) |
107 | 106 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑙 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑙) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) |
108 | 1, 2, 3, 9, 10, 11, 12, 41, 51, 72, 95, 101, 107 | gsumply1eq 21487 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) ↔ ∀𝑙 ∈ ℕ0 (𝑈‘(𝐺‘𝑙))
= (((coe1‘𝐾)‘𝑙) ∗ 1 ))) |
109 | 108 | biimpa 477 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) → ∀𝑙 ∈ ℕ0 (𝑈‘(𝐺‘𝑙))
= (((coe1‘𝐾)‘𝑙) ∗ 1 )) |
110 | 96, 103 | eqeq12d 2756 |
. . . 4
⊢ (𝑛 = 𝑙 → ((𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) ↔ (𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 ))) |
111 | 110 | cbvralvw 3381 |
. . 3
⊢
(∀𝑛 ∈
ℕ0 (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) ↔ ∀𝑙 ∈ ℕ0
(𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 )) |
112 | 109, 111 | sylibr 233 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 )) |
113 | 112 | ex 413 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 ))) |