Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(1𝑜 mPoly 𝑅) = (1𝑜 mPoly 𝑅) |
2 | | psr1baslem 19555 |
. . 3
⊢
(ℕ0 ↑𝑚 1𝑜) =
{𝑑 ∈
(ℕ0 ↑𝑚 1𝑜) ∣
(◡𝑑 “ ℕ) ∈
Fin} |
3 | | eqid 2622 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
4 | | eqid 2622 |
. . 3
⊢
(1r‘𝑅) = (1r‘𝑅) |
5 | | 1onn 7719 |
. . . 4
⊢
1𝑜 ∈ ω |
6 | 5 | a1i 11 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 1𝑜 ∈
ω) |
7 | | ply1coe.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
8 | | eqid 2622 |
. . . 4
⊢
(PwSer1‘𝑅) = (PwSer1‘𝑅) |
9 | | ply1coe.b |
. . . 4
⊢ 𝐵 = (Base‘𝑃) |
10 | 7, 8, 9 | ply1bas 19565 |
. . 3
⊢ 𝐵 =
(Base‘(1𝑜 mPoly 𝑅)) |
11 | | ply1coe.n |
. . . 4
⊢ · = (
·𝑠 ‘𝑃) |
12 | 7, 1, 11 | ply1vsca 19596 |
. . 3
⊢ · = (
·𝑠 ‘(1𝑜 mPoly 𝑅)) |
13 | | simpl 473 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝑅 ∈ Ring) |
14 | | simpr 477 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 ∈ 𝐵) |
15 | 1, 2, 3, 4, 6, 10,
12, 13, 14 | mplcoe1 19465 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = ((1𝑜 mPoly 𝑅) Σg
(𝑎 ∈
(ℕ0 ↑𝑚 1𝑜) ↦
((𝐾‘𝑎) · (𝑏 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))))))) |
16 | | ply1coe.a |
. . . . . . 7
⊢ 𝐴 = (coe1‘𝐾) |
17 | 16 | fvcoe1 19577 |
. . . . . 6
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → (𝐾‘𝑎) = (𝐴‘(𝑎‘∅))) |
18 | 17 | adantll 750 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → (𝐾‘𝑎) = (𝐴‘(𝑎‘∅))) |
19 | 5 | a1i 11 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → 1𝑜
∈ ω) |
20 | | eqid 2622 |
. . . . . . 7
⊢
(mulGrp‘(1𝑜 mPoly 𝑅)) = (mulGrp‘(1𝑜
mPoly 𝑅)) |
21 | | eqid 2622 |
. . . . . . 7
⊢
(.g‘(mulGrp‘(1𝑜 mPoly 𝑅))) =
(.g‘(mulGrp‘(1𝑜 mPoly 𝑅))) |
22 | | eqid 2622 |
. . . . . . 7
⊢
(1𝑜 mVar 𝑅) = (1𝑜 mVar 𝑅) |
23 | | simpll 790 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → 𝑅 ∈ Ring) |
24 | | simpr 477 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) |
25 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) →
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘∅)) = (((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘∅))) |
26 | | 0ex 4790 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
27 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ∅ →
((1𝑜 mVar 𝑅)‘𝑏) = ((1𝑜 mVar 𝑅)‘∅)) |
28 | 27 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∅ →
(((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅)) =
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘∅))) |
29 | 27 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∅ →
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑏)) =
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘∅))) |
30 | 28, 29 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ (𝑏 = ∅ →
((((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅)) =
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑏)) ↔
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘∅)) = (((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘∅)))) |
31 | 26, 30 | ralsn 4222 |
. . . . . . . . . 10
⊢
(∀𝑏 ∈
{∅} (((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅)) =
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑏)) ↔
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘∅)) = (((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘∅))) |
32 | 25, 31 | sylibr 224 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ∀𝑏 ∈ {∅}
(((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅)) =
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑏))) |
33 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ →
((1𝑜 mVar 𝑅)‘𝑥) = ((1𝑜 mVar 𝑅)‘∅)) |
34 | 33 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ →
(((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑥)) = (((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅))) |
35 | 33 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ →
(((1𝑜 mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑏)) = (((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑏))) |
36 | 34, 35 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ →
((((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑥)) = (((1𝑜 mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑏)) ↔ (((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅)) =
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑏)))) |
37 | 36 | ralbidv 2986 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (∀𝑏 ∈ {∅}
(((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑥)) = (((1𝑜 mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑏)) ↔ ∀𝑏 ∈ {∅} (((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅)) =
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑏)))) |
38 | 26, 37 | ralsn 4222 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
{∅}∀𝑏 ∈
{∅} (((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑥)) = (((1𝑜 mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑏)) ↔ ∀𝑏 ∈ {∅} (((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅)) =
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑏))) |
39 | 32, 38 | sylibr 224 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ∀𝑥 ∈ {∅}∀𝑏 ∈ {∅}
(((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑥)) = (((1𝑜 mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑏))) |
40 | | df1o2 7572 |
. . . . . . . . 9
⊢
1𝑜 = {∅} |
41 | 40 | raleqi 3142 |
. . . . . . . . 9
⊢
(∀𝑏 ∈
1𝑜 (((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑥)) = (((1𝑜 mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑏)) ↔ ∀𝑏 ∈ {∅} (((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑥)) = (((1𝑜 mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑏))) |
42 | 40, 41 | raleqbii 2990 |
. . . . . . . 8
⊢
(∀𝑥 ∈
1𝑜 ∀𝑏 ∈ 1𝑜
(((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑥)) = (((1𝑜 mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑏)) ↔ ∀𝑥 ∈ {∅}∀𝑏 ∈ {∅} (((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑥)) = (((1𝑜 mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑏))) |
43 | 39, 42 | sylibr 224 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ∀𝑥 ∈ 1𝑜
∀𝑏 ∈
1𝑜 (((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑥)) = (((1𝑜 mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑏))) |
44 | 1, 2, 3, 4, 19, 20, 21, 22, 23, 24, 43 | mplcoe5 19468 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → (𝑏 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))) = ((mulGrp‘(1𝑜
mPoly 𝑅))
Σg (𝑐 ∈ 1𝑜 ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐))))) |
45 | | mpteq1 4737 |
. . . . . . . . 9
⊢
(1𝑜 = {∅} → (𝑐 ∈ 1𝑜 ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐))) = (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐)))) |
46 | 40, 45 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑐 ∈ 1𝑜
↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐))) = (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐))) |
47 | 46 | oveq2i 6661 |
. . . . . . 7
⊢
((mulGrp‘(1𝑜 mPoly 𝑅)) Σg (𝑐 ∈ 1𝑜
↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐)))) = ((mulGrp‘(1𝑜 mPoly 𝑅)) Σg (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐)))) |
48 | 1 | mplring 19452 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ ω ∧ 𝑅 ∈ Ring) → (1𝑜
mPoly 𝑅) ∈
Ring) |
49 | 5, 48 | mpan 706 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(1𝑜 mPoly 𝑅) ∈ Ring) |
50 | 20 | ringmgp 18553 |
. . . . . . . . . 10
⊢
((1𝑜 mPoly 𝑅) ∈ Ring →
(mulGrp‘(1𝑜 mPoly 𝑅)) ∈ Mnd) |
51 | 49, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(mulGrp‘(1𝑜 mPoly 𝑅)) ∈ Mnd) |
52 | 51 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) →
(mulGrp‘(1𝑜 mPoly 𝑅)) ∈ Mnd) |
53 | 26 | a1i 11 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ∅ ∈
V) |
54 | | ply1coe.e |
. . . . . . . . . . . 12
⊢ ↑ =
(.g‘𝑀) |
55 | 20, 10 | mgpbas 18495 |
. . . . . . . . . . . . 13
⊢ 𝐵 =
(Base‘(mulGrp‘(1𝑜 mPoly 𝑅))) |
56 | 55 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 =
(Base‘(mulGrp‘(1𝑜 mPoly 𝑅)))) |
57 | | ply1coe.m |
. . . . . . . . . . . . . 14
⊢ 𝑀 = (mulGrp‘𝑃) |
58 | 57, 9 | mgpbas 18495 |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑀) |
59 | 58 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 = (Base‘𝑀)) |
60 | | ssv 3625 |
. . . . . . . . . . . . 13
⊢ 𝐵 ⊆ V |
61 | 60 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 ⊆ V) |
62 | | ovexd 6680 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑏) ∈ V) |
63 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑃) = (.r‘𝑃) |
64 | 7, 1, 63 | ply1mulr 19597 |
. . . . . . . . . . . . . . . 16
⊢
(.r‘𝑃) =
(.r‘(1𝑜 mPoly 𝑅)) |
65 | 20, 64 | mgpplusg 18493 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝑃) =
(+g‘(mulGrp‘(1𝑜 mPoly 𝑅))) |
66 | 57, 63 | mgpplusg 18493 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝑃) = (+g‘𝑀) |
67 | 65, 66 | eqtr3i 2646 |
. . . . . . . . . . . . . 14
⊢
(+g‘(mulGrp‘(1𝑜 mPoly 𝑅))) = (+g‘𝑀) |
68 | 67 | oveqi 6663 |
. . . . . . . . . . . . 13
⊢ (𝑎(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑏) = (𝑎(+g‘𝑀)𝑏) |
69 | 68 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑏) = (𝑎(+g‘𝑀)𝑏)) |
70 | 21, 54, 56, 59, 61, 62, 69 | mulgpropd 17584 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) →
(.g‘(mulGrp‘(1𝑜 mPoly 𝑅))) = ↑ ) |
71 | 70 | oveqd 6667 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋) = ((𝑎‘∅) ↑ 𝑋)) |
72 | 71 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋) = ((𝑎‘∅) ↑ 𝑋)) |
73 | 7 | ply1ring 19618 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
74 | 57 | ringmgp 18553 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring → 𝑀 ∈ Mnd) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
76 | 75 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → 𝑀 ∈ Mnd) |
77 | | elmapi 7879 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) → 𝑎:1𝑜⟶ℕ0) |
78 | | 0lt1o 7584 |
. . . . . . . . . . . 12
⊢ ∅
∈ 1𝑜 |
79 | | ffvelrn 6357 |
. . . . . . . . . . . 12
⊢ ((𝑎:1𝑜⟶ℕ0
∧ ∅ ∈ 1𝑜) → (𝑎‘∅) ∈
ℕ0) |
80 | 77, 78, 79 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) → (𝑎‘∅) ∈
ℕ0) |
81 | 80 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → (𝑎‘∅) ∈
ℕ0) |
82 | | ply1coe.x |
. . . . . . . . . . . 12
⊢ 𝑋 = (var1‘𝑅) |
83 | 82, 7, 9 | vr1cl 19587 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) |
84 | 83 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → 𝑋 ∈ 𝐵) |
85 | 58, 54 | mulgnn0cl 17558 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ (𝑎‘∅) ∈
ℕ0 ∧ 𝑋
∈ 𝐵) → ((𝑎‘∅) ↑ 𝑋) ∈ 𝐵) |
86 | 76, 81, 84, 85 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ((𝑎‘∅) ↑ 𝑋) ∈ 𝐵) |
87 | 72, 86 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋) ∈ 𝐵) |
88 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑐 = ∅ → (𝑎‘𝑐) = (𝑎‘∅)) |
89 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑐 = ∅ →
((1𝑜 mVar 𝑅)‘𝑐) = ((1𝑜 mVar 𝑅)‘∅)) |
90 | 82 | vr1val 19562 |
. . . . . . . . . . 11
⊢ 𝑋 = ((1𝑜 mVar
𝑅)‘∅) |
91 | 89, 90 | syl6eqr 2674 |
. . . . . . . . . 10
⊢ (𝑐 = ∅ →
((1𝑜 mVar 𝑅)‘𝑐) = 𝑋) |
92 | 88, 91 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑐 = ∅ → ((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐)) = ((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋)) |
93 | 55, 92 | gsumsn 18354 |
. . . . . . . 8
⊢
(((mulGrp‘(1𝑜 mPoly 𝑅)) ∈ Mnd ∧ ∅ ∈ V ∧
((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋) ∈ 𝐵) →
((mulGrp‘(1𝑜 mPoly 𝑅))
Σg (𝑐 ∈ {∅} ↦
((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜 mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑐)))) =
((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋)) |
94 | 52, 53, 87, 93 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) →
((mulGrp‘(1𝑜 mPoly 𝑅)) Σg (𝑐 ∈ {∅} ↦
((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐)))) = ((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋)) |
95 | 47, 94 | syl5eq 2668 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) →
((mulGrp‘(1𝑜 mPoly 𝑅)) Σg (𝑐 ∈ 1𝑜
↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐)))) = ((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋)) |
96 | 44, 95, 72 | 3eqtrd 2660 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → (𝑏 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))) = ((𝑎‘∅) ↑ 𝑋)) |
97 | 18, 96 | oveq12d 6668 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ((𝐾‘𝑎) · (𝑏 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅)))) = ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))) |
98 | 97 | mpteq2dva 4744 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))))) = (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))) |
99 | 98 | oveq2d 6666 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1𝑜 mPoly 𝑅) Σg
(𝑎 ∈
(ℕ0 ↑𝑚 1𝑜) ↦
((𝐾‘𝑎) · (𝑏 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅)))))) = ((1𝑜 mPoly 𝑅) Σg
(𝑎 ∈
(ℕ0 ↑𝑚 1𝑜) ↦
((𝐴‘(𝑎‘∅)) ·
((𝑎‘∅) ↑ 𝑋))))) |
100 | | nn0ex 11298 |
. . . . . 6
⊢
ℕ0 ∈ V |
101 | 100 | mptex 6486 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∈ V |
102 | 101 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∈ V) |
103 | | fvex 6201 |
. . . . . 6
⊢
(Poly1‘𝑅) ∈ V |
104 | 7, 103 | eqeltri 2697 |
. . . . 5
⊢ 𝑃 ∈ V |
105 | 104 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝑃 ∈ V) |
106 | | ovexd 6680 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1𝑜 mPoly 𝑅) ∈ V) |
107 | 9, 10 | eqtr3i 2646 |
. . . . 5
⊢
(Base‘𝑃) =
(Base‘(1𝑜 mPoly 𝑅)) |
108 | 107 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (Base‘𝑃) = (Base‘(1𝑜 mPoly
𝑅))) |
109 | | eqid 2622 |
. . . . . 6
⊢
(+g‘𝑃) = (+g‘𝑃) |
110 | 7, 1, 109 | ply1plusg 19595 |
. . . . 5
⊢
(+g‘𝑃) =
(+g‘(1𝑜 mPoly 𝑅)) |
111 | 110 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (+g‘𝑃) =
(+g‘(1𝑜 mPoly 𝑅))) |
112 | 102, 105,
106, 108, 111 | gsumpropd 17272 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) = ((1𝑜 mPoly 𝑅) Σg
(𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))))) |
113 | | eqid 2622 |
. . . . 5
⊢
(0g‘𝑃) = (0g‘𝑃) |
114 | 1, 7, 113 | ply1mpl0 19625 |
. . . 4
⊢
(0g‘𝑃) =
(0g‘(1𝑜 mPoly 𝑅)) |
115 | 1 | mpllmod 19451 |
. . . . . 6
⊢
((1𝑜 ∈ ω ∧ 𝑅 ∈ Ring) → (1𝑜
mPoly 𝑅) ∈
LMod) |
116 | 5, 13, 115 | sylancr 695 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1𝑜 mPoly 𝑅) ∈ LMod) |
117 | | lmodcmn 18911 |
. . . . 5
⊢
((1𝑜 mPoly 𝑅) ∈ LMod → (1𝑜
mPoly 𝑅) ∈
CMnd) |
118 | 116, 117 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1𝑜 mPoly 𝑅) ∈ CMnd) |
119 | 100 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ℕ0 ∈
V) |
120 | 7 | ply1lmod 19622 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
121 | 120 | ad2antrr 762 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑃 ∈ LMod) |
122 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
123 | 16, 9, 7, 122 | coe1f 19581 |
. . . . . . . . 9
⊢ (𝐾 ∈ 𝐵 → 𝐴:ℕ0⟶(Base‘𝑅)) |
124 | 123 | adantl 482 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐴:ℕ0⟶(Base‘𝑅)) |
125 | 124 | ffvelrnda 6359 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘𝑅)) |
126 | 7 | ply1sca 19623 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
127 | 126 | eqcomd 2628 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(Scalar‘𝑃) = 𝑅) |
128 | 127 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
(Scalar‘𝑃) = 𝑅) |
129 | 128 | fveq2d 6195 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
(Base‘(Scalar‘𝑃)) = (Base‘𝑅)) |
130 | 125, 129 | eleqtrrd 2704 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑃))) |
131 | 75 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈ Mnd) |
132 | | simpr 477 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
133 | 83 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
134 | 58, 54 | mulgnn0cl 17558 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ 𝑘 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝑘 ↑ 𝑋) ∈ 𝐵) |
135 | 131, 132,
133, 134 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐵) |
136 | | eqid 2622 |
. . . . . . 7
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
137 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
138 | 9, 136, 11, 137 | lmodvscl 18880 |
. . . . . 6
⊢ ((𝑃 ∈ LMod ∧ (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑘 ↑ 𝑋) ∈ 𝐵) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐵) |
139 | 121, 130,
135, 138 | syl3anc 1326 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐵) |
140 | | eqid 2622 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) |
141 | 139, 140 | fmptd 6385 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))):ℕ0⟶𝐵) |
142 | 7, 82, 9, 11, 57, 54, 16 | ply1coefsupp 19665 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃)) |
143 | | eqid 2622 |
. . . . . 6
⊢ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅)) |
144 | 40, 100, 26, 143 | mapsnf1o2 7905 |
. . . . 5
⊢ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅)):(ℕ0
↑𝑚 1𝑜)–1-1-onto→ℕ0 |
145 | 144 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅)):(ℕ0
↑𝑚 1𝑜)–1-1-onto→ℕ0) |
146 | 10, 114, 118, 119, 141, 142, 145 | gsumf1o 18317 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1𝑜 mPoly 𝑅) Σg
(𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) = ((1𝑜 mPoly 𝑅) Σg
((𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅))))) |
147 | | eqidd 2623 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅))) |
148 | | eqidd 2623 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) |
149 | | fveq2 6191 |
. . . . . 6
⊢ (𝑘 = (𝑎‘∅) → (𝐴‘𝑘) = (𝐴‘(𝑎‘∅))) |
150 | | oveq1 6657 |
. . . . . 6
⊢ (𝑘 = (𝑎‘∅) → (𝑘 ↑ 𝑋) = ((𝑎‘∅) ↑ 𝑋)) |
151 | 149, 150 | oveq12d 6668 |
. . . . 5
⊢ (𝑘 = (𝑎‘∅) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) = ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))) |
152 | 81, 147, 148, 151 | fmptco 6396 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅))) = (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))) |
153 | 152 | oveq2d 6666 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1𝑜 mPoly 𝑅) Σg
((𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅)))) = ((1𝑜
mPoly 𝑅)
Σg (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))))) |
154 | 112, 146,
153 | 3eqtrrd 2661 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1𝑜 mPoly 𝑅) Σg
(𝑎 ∈
(ℕ0 ↑𝑚 1𝑜) ↦
((𝐴‘(𝑎‘∅)) ·
((𝑎‘∅) ↑ 𝑋)))) = (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))))) |
155 | 15, 99, 154 | 3eqtrd 2660 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))))) |