Step | Hyp | Ref
| Expression |
1 | | ply1gsumz.a |
. . . . 5
⊢ (𝜑 → 𝐴:(0..^𝑁)⟶𝐵) |
2 | 1 | ffnd 6708 |
. . . 4
⊢ (𝜑 → 𝐴 Fn (0..^𝑁)) |
3 | | ply1gsumz.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | | ply1gsumz.p |
. . . . . . . . 9
⊢ 𝑃 = (Poly1‘𝑅) |
5 | 4 | ply1ring 22080 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
6 | | eqid 2724 |
. . . . . . . . 9
⊢
(Base‘𝑃) =
(Base‘𝑃) |
7 | | ply1gsumz.z |
. . . . . . . . 9
⊢ 𝑍 = (0g‘𝑃) |
8 | 6, 7 | ring0cl 20151 |
. . . . . . . 8
⊢ (𝑃 ∈ Ring → 𝑍 ∈ (Base‘𝑃)) |
9 | 3, 5, 8 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (Base‘𝑃)) |
10 | | eqid 2724 |
. . . . . . . 8
⊢
(coe1‘𝑍) = (coe1‘𝑍) |
11 | | ply1gsumz.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
12 | 10, 6, 4, 11 | coe1f 22044 |
. . . . . . 7
⊢ (𝑍 ∈ (Base‘𝑃) →
(coe1‘𝑍):ℕ0⟶𝐵) |
13 | 9, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(coe1‘𝑍):ℕ0⟶𝐵) |
14 | 13 | ffnd 6708 |
. . . . 5
⊢ (𝜑 →
(coe1‘𝑍)
Fn ℕ0) |
15 | | fzo0ssnn0 13709 |
. . . . . 6
⊢
(0..^𝑁) ⊆
ℕ0 |
16 | 15 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0..^𝑁) ⊆
ℕ0) |
17 | 14, 16 | fnssresd 6664 |
. . . 4
⊢ (𝜑 →
((coe1‘𝑍)
↾ (0..^𝑁)) Fn
(0..^𝑁)) |
18 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁)) |
19 | 18 | fvresd 6901 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((coe1‘𝑍) ↾ (0..^𝑁))‘𝑗) = ((coe1‘𝑍)‘𝑗)) |
20 | | elfzonn0 13673 |
. . . . . 6
⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℕ0) |
21 | | ply1gsumz.s |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 Σg (𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)) = 𝑍) |
22 | 21, 9 | eqeltrd 2825 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 Σg (𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)) ∈ (Base‘𝑃)) |
23 | | eqid 2724 |
. . . . . . . . . 10
⊢
(coe1‘(𝑃 Σg (𝐴 ∘f (
·𝑠 ‘𝑃)𝐹))) = (coe1‘(𝑃 Σg
(𝐴 ∘f (
·𝑠 ‘𝑃)𝐹))) |
24 | 4, 6, 23, 10 | ply1coe1eq 22132 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑃 Σg
(𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)) ∈ (Base‘𝑃) ∧ 𝑍 ∈ (Base‘𝑃)) → (∀𝑗 ∈ ℕ0
((coe1‘(𝑃
Σg (𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)))‘𝑗) = ((coe1‘𝑍)‘𝑗) ↔ (𝑃 Σg (𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)) = 𝑍)) |
25 | 24 | biimpar 477 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ (𝑃 Σg
(𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)) ∈ (Base‘𝑃) ∧ 𝑍 ∈ (Base‘𝑃)) ∧ (𝑃 Σg (𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)) = 𝑍) → ∀𝑗 ∈ ℕ0
((coe1‘(𝑃
Σg (𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)))‘𝑗) = ((coe1‘𝑍)‘𝑗)) |
26 | 3, 22, 9, 21, 25 | syl31anc 1370 |
. . . . . . 7
⊢ (𝜑 → ∀𝑗 ∈ ℕ0
((coe1‘(𝑃
Σg (𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)))‘𝑗) = ((coe1‘𝑍)‘𝑗)) |
27 | 26 | r19.21bi 3240 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((coe1‘(𝑃
Σg (𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)))‘𝑗) = ((coe1‘𝑍)‘𝑗)) |
28 | 20, 27 | sylan2 592 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((coe1‘(𝑃 Σg
(𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)))‘𝑗) = ((coe1‘𝑍)‘𝑗)) |
29 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 Fn (0..^𝑁)) |
30 | | nfv 1909 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛𝜑 |
31 | | ovexd 7436 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ V) |
32 | | ply1gsumz.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
33 | 30, 31, 32 | fnmptd 6681 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 Fn (0..^𝑁)) |
34 | 33 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐹 Fn (0..^𝑁)) |
35 | | ovexd 7436 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (0..^𝑁) ∈ V) |
36 | | inidm 4210 |
. . . . . . . . . 10
⊢
((0..^𝑁) ∩
(0..^𝑁)) = (0..^𝑁) |
37 | | eqidd 2725 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝐴‘𝑖) = (𝐴‘𝑖)) |
38 | | oveq1 7408 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑖 → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
39 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^𝑁)) |
40 | | ovexd 7436 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ V) |
41 | 32, 38, 39, 40 | fvmptd3 7011 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝐹‘𝑖) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
42 | 29, 34, 35, 35, 36, 37, 41 | offval 7672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 ∘f (
·𝑠 ‘𝑃)𝐹) = (𝑖 ∈ (0..^𝑁) ↦ ((𝐴‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) |
43 | 42 | oveq2d 7417 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑃 Σg (𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)) = (𝑃 Σg (𝑖 ∈ (0..^𝑁) ↦ ((𝐴‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) |
44 | 43 | fveq2d 6885 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (coe1‘(𝑃 Σg
(𝐴 ∘f (
·𝑠 ‘𝑃)𝐹))) = (coe1‘(𝑃 Σg
(𝑖 ∈ (0..^𝑁) ↦ ((𝐴‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))) |
45 | 44 | fveq1d 6883 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((coe1‘(𝑃 Σg
(𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)))‘𝑗) = ((coe1‘(𝑃 Σg
(𝑖 ∈ (0..^𝑁) ↦ ((𝐴‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))‘𝑗)) |
46 | | eqid 2724 |
. . . . . . 7
⊢
(var1‘𝑅) = (var1‘𝑅) |
47 | | eqid 2724 |
. . . . . . 7
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
48 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑅 ∈ Ring) |
49 | | eqid 2724 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) |
50 | | ply1gsumz.1 |
. . . . . . 7
⊢ 0 =
(0g‘𝑅) |
51 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴:(0..^𝑁)⟶𝐵) |
52 | 51 | ffvelcdmda 7076 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝐴‘𝑖) ∈ 𝐵) |
53 | 52 | ralrimiva 3138 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∀𝑖 ∈ (0..^𝑁)(𝐴‘𝑖) ∈ 𝐵) |
54 | | ply1gsumz.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
55 | 54 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑁 ∈
ℕ0) |
56 | | fveq2 6881 |
. . . . . . 7
⊢ (𝑖 = 𝑗 → (𝐴‘𝑖) = (𝐴‘𝑗)) |
57 | 4, 6, 46, 47, 48, 11, 49, 50, 53, 18, 55, 56 | gsummoncoe1fzo 33100 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((coe1‘(𝑃 Σg
(𝑖 ∈ (0..^𝑁) ↦ ((𝐴‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))‘𝑗) = (𝐴‘𝑗)) |
58 | 45, 57 | eqtrd 2764 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((coe1‘(𝑃 Σg
(𝐴 ∘f (
·𝑠 ‘𝑃)𝐹)))‘𝑗) = (𝐴‘𝑗)) |
59 | 19, 28, 58 | 3eqtr2rd 2771 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴‘𝑗) = (((coe1‘𝑍) ↾ (0..^𝑁))‘𝑗)) |
60 | 2, 17, 59 | eqfnfvd 7025 |
. . 3
⊢ (𝜑 → 𝐴 = ((coe1‘𝑍) ↾ (0..^𝑁))) |
61 | 4, 7, 50 | coe1z 22095 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(coe1‘𝑍) =
(ℕ0 × { 0 })) |
62 | 3, 61 | syl 17 |
. . . 4
⊢ (𝜑 →
(coe1‘𝑍) =
(ℕ0 × { 0 })) |
63 | 62 | reseq1d 5970 |
. . 3
⊢ (𝜑 →
((coe1‘𝑍)
↾ (0..^𝑁)) =
((ℕ0 × { 0 }) ↾ (0..^𝑁))) |
64 | 60, 63 | eqtrd 2764 |
. 2
⊢ (𝜑 → 𝐴 = ((ℕ0 × { 0 }) ↾
(0..^𝑁))) |
65 | | xpssres 6008 |
. . 3
⊢
((0..^𝑁) ⊆
ℕ0 → ((ℕ0 × { 0 }) ↾ (0..^𝑁)) = ((0..^𝑁) × { 0 })) |
66 | 15, 65 | ax-mp 5 |
. 2
⊢
((ℕ0 × { 0 }) ↾ (0..^𝑁)) = ((0..^𝑁) × { 0 }) |
67 | 64, 66 | eqtrdi 2780 |
1
⊢ (𝜑 → 𝐴 = ((0..^𝑁) × { 0 })) |