Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
(Poly1‘𝐴) = (Poly1‘𝐴) |
2 | | eqid 2610 |
. . . . 5
⊢
(var1‘𝐴) = (var1‘𝐴) |
3 | | eqid 2610 |
. . . . 5
⊢
(.g‘(mulGrp‘(Poly1‘𝐴))) =
(.g‘(mulGrp‘(Poly1‘𝐴))) |
4 | | crngring 18381 |
. . . . . . . 8
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
5 | | chcoeffeq.a |
. . . . . . . . 9
⊢ 𝐴 = (𝑁 Mat 𝑅) |
6 | 5 | matring 20068 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
7 | 4, 6 | sylan2 490 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring) |
8 | 7 | 3adant3 1074 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ Ring) |
9 | 8 | adantr 480 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝐴 ∈ Ring) |
10 | | chcoeffeq.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐴) |
11 | | eqid 2610 |
. . . . 5
⊢ (
·𝑠 ‘(Poly1‘𝐴)) = (
·𝑠 ‘(Poly1‘𝐴)) |
12 | | eqid 2610 |
. . . . 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 2610 |
. . . . . . . 8
⊢ (𝑁 ConstPolyMat 𝑅) = (𝑁 ConstPolyMat 𝑅) |
21 | | eqid 2610 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌) |
22 | | eqid 2610 |
. . . . . . . 8
⊢
(1r‘𝑌) = (1r‘𝑌) |
23 | | eqid 2610 |
. . . . . . . 8
⊢
(var1‘𝑅) = (var1‘𝑅) |
24 | | eqid 2610 |
. . . . . . . 8
⊢
(((var1‘𝑅)( ·𝑠
‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) = (((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) |
25 | | eqid 2610 |
. . . . . . . 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 20505 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → (𝑈 ∘ 𝐺) ∈ (𝐵 ↑𝑚
ℕ0)) |
29 | 28 | anasss 677 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑈 ∘ 𝐺) ∈ (𝐵 ↑𝑚
ℕ0)) |
30 | 5, 10, 13, 14, 16, 17, 18, 15, 19, 20 | chfacfisfcpmat 20479 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)) |
31 | 4, 30 | syl3anl2 1367 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)) |
32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ (𝑈 ∘ 𝐺) ∈ (𝐵 ↑𝑚
ℕ0)) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)) |
33 | | fvco3 6185 |
. . . . . . . . . 10
⊢ ((𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅) ∧ 𝑙 ∈ ℕ0) → ((𝑈 ∘ 𝐺)‘𝑙) = (𝑈‘(𝐺‘𝑙))) |
34 | 33 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅) ∧ 𝑙 ∈ ℕ0) → (𝑈‘(𝐺‘𝑙)) = ((𝑈 ∘ 𝐺)‘𝑙)) |
35 | 32, 34 | sylan 487 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ (𝑈 ∘ 𝐺) ∈ (𝐵 ↑𝑚
ℕ0)) ∧ 𝑙 ∈ ℕ0) → (𝑈‘(𝐺‘𝑙)) = ((𝑈 ∘ 𝐺)‘𝑙)) |
36 | | elmapi 7765 |
. . . . . . . . . 10
⊢ ((𝑈 ∘ 𝐺) ∈ (𝐵 ↑𝑚
ℕ0) → (𝑈 ∘ 𝐺):ℕ0⟶𝐵) |
37 | 36 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ (𝑈 ∘ 𝐺) ∈ (𝐵 ↑𝑚
ℕ0)) → (𝑈 ∘ 𝐺):ℕ0⟶𝐵) |
38 | 37 | ffvelrnda 6267 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ (𝑈 ∘ 𝐺) ∈ (𝐵 ↑𝑚
ℕ0)) ∧ 𝑙 ∈ ℕ0) → ((𝑈 ∘ 𝐺)‘𝑙) ∈ 𝐵) |
39 | 35, 38 | eqeltrd 2688 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ (𝑈 ∘ 𝐺) ∈ (𝐵 ↑𝑚
ℕ0)) ∧ 𝑙 ∈ ℕ0) → (𝑈‘(𝐺‘𝑙)) ∈ 𝐵) |
40 | 39 | ralrimiva 2949 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ (𝑈 ∘ 𝐺) ∈ (𝐵 ↑𝑚
ℕ0)) → ∀𝑙 ∈ ℕ0 (𝑈‘(𝐺‘𝑙)) ∈ 𝐵) |
41 | 29, 40 | mpdan 699 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ∀𝑙 ∈ ℕ0
(𝑈‘(𝐺‘𝑙)) ∈ 𝐵) |
42 | 4 | anim2i 591 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
43 | 42 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
44 | 43 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
45 | 5, 10, 20, 27 | cpm2mf 20376 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵) |
47 | | fcompt 6306 |
. . . . . . 7
⊢ ((𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵 ∧ 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)) → (𝑈 ∘ 𝐺) = (𝑙 ∈ ℕ0 ↦ (𝑈‘(𝐺‘𝑙)))) |
48 | 46, 31, 47 | syl2anc 691 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (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 20506 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → (𝑈 ∘ 𝐺) finSupp (0g‘𝐴)) |
50 | 49 | anasss 677 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑈 ∘ 𝐺) finSupp (0g‘𝐴)) |
51 | 48, 50 | eqbrtrrd 4607 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑙 ∈ ℕ0 ↦ (𝑈‘(𝐺‘𝑙))) finSupp (0g‘𝐴)) |
52 | | simpll1 1093 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑙 ∈ ℕ0) → 𝑁 ∈ Fin) |
53 | 4 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
54 | 53 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑙 ∈ ℕ0) → 𝑅 ∈ Ring) |
55 | | chcoeffeq.k |
. . . . . . . . . 10
⊢ 𝐾 = (𝐶‘𝑀) |
56 | | chcoeffeq.c |
. . . . . . . . . . 11
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
57 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑃) =
(Base‘𝑃) |
58 | 56, 5, 10, 13, 57 | chpmatply1 20456 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) ∈ (Base‘𝑃)) |
59 | 55, 58 | syl5eqel 2692 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐾 ∈ (Base‘𝑃)) |
60 | | eqid 2610 |
. . . . . . . . . 10
⊢
(coe1‘𝐾) = (coe1‘𝐾) |
61 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
62 | 60, 57, 13, 61 | coe1fvalcl 19403 |
. . . . . . . . 9
⊢ ((𝐾 ∈ (Base‘𝑃) ∧ 𝑙 ∈ ℕ0) →
((coe1‘𝐾)‘𝑙) ∈ (Base‘𝑅)) |
63 | 59, 62 | sylan 487 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) →
((coe1‘𝐾)‘𝑙) ∈ (Base‘𝑅)) |
64 | 63 | adantlr 747 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑙 ∈ ℕ0) →
((coe1‘𝐾)‘𝑙) ∈ (Base‘𝑅)) |
65 | | chcoeffeq.1 |
. . . . . . . . . 10
⊢ 1 =
(1r‘𝐴) |
66 | 10, 65 | ringidcl 18391 |
. . . . . . . . 9
⊢ (𝐴 ∈ Ring → 1 ∈ 𝐵) |
67 | 8, 66 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 1 ∈ 𝐵) |
68 | 67 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑙 ∈ ℕ0) → 1 ∈ 𝐵) |
69 | | chcoeffeq.m |
. . . . . . . 8
⊢ ∗ = (
·𝑠 ‘𝐴) |
70 | 61, 5, 10, 69 | matvscl 20056 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧
(((coe1‘𝐾)‘𝑙) ∈ (Base‘𝑅) ∧ 1 ∈ 𝐵)) → (((coe1‘𝐾)‘𝑙) ∗ 1 ) ∈ 𝐵) |
71 | 52, 54, 64, 68, 70 | syl22anc 1319 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑙 ∈ ℕ0) →
(((coe1‘𝐾)‘𝑙) ∗ 1 ) ∈ 𝐵) |
72 | 71 | ralrimiva 2949 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ∀𝑙 ∈ ℕ0
(((coe1‘𝐾)‘𝑙) ∗ 1 ) ∈ 𝐵) |
73 | | nn0ex 11175 |
. . . . . . 7
⊢
ℕ0 ∈ V |
74 | 73 | a1i 11 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ℕ0
∈ V) |
75 | 5 | matlmod 20054 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) |
76 | 4, 75 | sylan2 490 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ LMod) |
77 | 76 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ LMod) |
78 | 77 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝐴 ∈ LMod) |
79 | | eqidd 2611 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (Scalar‘𝐴) = (Scalar‘𝐴)) |
80 | | fvex 6113 |
. . . . . . 7
⊢
((coe1‘𝐾)‘𝑙) ∈ V |
81 | 80 | a1i 11 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑙 ∈ ℕ0) →
((coe1‘𝐾)‘𝑙) ∈ V) |
82 | | eqid 2610 |
. . . . . 6
⊢
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐴)) |
83 | 5 | matsca2 20045 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 = (Scalar‘𝐴)) |
84 | 83 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 = (Scalar‘𝐴)) |
85 | 84, 53 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝐴) ∈ Ring) |
86 | 84 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝐴) = 𝑅) |
87 | 86 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) →
(Poly1‘(Scalar‘𝐴)) = (Poly1‘𝑅)) |
88 | 87, 13 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) →
(Poly1‘(Scalar‘𝐴)) = 𝑃) |
89 | 88 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) →
(Base‘(Poly1‘(Scalar‘𝐴))) = (Base‘𝑃)) |
90 | 59, 89 | eleqtrrd 2691 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐾 ∈
(Base‘(Poly1‘(Scalar‘𝐴)))) |
91 | | eqid 2610 |
. . . . . . . . 9
⊢
(Poly1‘(Scalar‘𝐴)) =
(Poly1‘(Scalar‘𝐴)) |
92 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘(Poly1‘(Scalar‘𝐴))) =
(Base‘(Poly1‘(Scalar‘𝐴))) |
93 | 91, 92, 82 | mptcoe1fsupp 19406 |
. . . . . . . 8
⊢
(((Scalar‘𝐴)
∈ Ring ∧ 𝐾 ∈
(Base‘(Poly1‘(Scalar‘𝐴)))) → (𝑙 ∈ ℕ0 ↦
((coe1‘𝐾)‘𝑙)) finSupp
(0g‘(Scalar‘𝐴))) |
94 | 85, 90, 93 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑙 ∈ ℕ0 ↦
((coe1‘𝐾)‘𝑙)) finSupp
(0g‘(Scalar‘𝐴))) |
95 | 94 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑙 ∈ ℕ0 ↦
((coe1‘𝐾)‘𝑙)) finSupp
(0g‘(Scalar‘𝐴))) |
96 | 74, 78, 79, 10, 81, 68, 12, 82, 69, 95 | mptscmfsupp0 18751 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑙 ∈ ℕ0 ↦
(((coe1‘𝐾)‘𝑙) ∗ 1 )) finSupp
(0g‘𝐴)) |
97 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑙 → (𝐺‘𝑛) = (𝐺‘𝑙)) |
98 | 97 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑛 = 𝑙 → (𝑈‘(𝐺‘𝑛)) = (𝑈‘(𝐺‘𝑙))) |
99 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑛 = 𝑙 → (𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)) = (𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))) |
100 | 98, 99 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑛 = 𝑙 → ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))) = ((𝑈‘(𝐺‘𝑙))(
·𝑠 ‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))) |
101 | 100 | cbvmptv 4678 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))) = (𝑙
∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑙))(
·𝑠 ‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))) |
102 | 101 | oveq2i 6560 |
. . . . . 6
⊢
((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0
↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑙 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑙))(
·𝑠 ‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) |
103 | 102 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) →
((Poly1‘𝐴)
Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑙 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑙))(
·𝑠 ‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) |
104 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑙 → ((coe1‘𝐾)‘𝑛) = ((coe1‘𝐾)‘𝑙)) |
105 | 104 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑛 = 𝑙 → (((coe1‘𝐾)‘𝑛) ∗ 1 ) =
(((coe1‘𝐾)‘𝑙) ∗ 1 )) |
106 | 105, 99 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑛 = 𝑙 → ((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))) = ((((coe1‘𝐾)‘𝑙)
∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))) |
107 | 106 | cbvmptv 4678 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ ((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))) = (𝑙
∈ ℕ0 ↦ ((((coe1‘𝐾)‘𝑙)
∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))) |
108 | 107 | oveq2i 6560 |
. . . . . 6
⊢
((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0
↦ ((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑙 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑙) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) |
109 | 108 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) →
((Poly1‘𝐴)
Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑙 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑙) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑙(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) |
110 | 1, 2, 3, 9, 10, 11, 12, 41, 51, 72, 96, 103, 109 | gsumply1eq 19496 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) →
(((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0
↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) ↔ ∀𝑙 ∈ ℕ0 (𝑈‘(𝐺‘𝑙))
= (((coe1‘𝐾)‘𝑙) ∗ 1 ))) |
111 | 110 | biimpa 500 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧
((Poly1‘𝐴)
Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) → ∀𝑙 ∈ ℕ0 (𝑈‘(𝐺‘𝑙))
= (((coe1‘𝐾)‘𝑙) ∗ 1 )) |
112 | 98, 105 | eqeq12d 2625 |
. . . 4
⊢ (𝑛 = 𝑙 → ((𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) ↔ (𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 ))) |
113 | 112 | cbvralv 3147 |
. . 3
⊢
(∀𝑛 ∈
ℕ0 (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) ↔ ∀𝑙 ∈ ℕ0
(𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 )) |
114 | 111, 113 | sylibr 223 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧
((Poly1‘𝐴)
Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 )) |
115 | 114 | ex 449 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) →
(((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0
↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 ))) |