Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . 3
⊢
(1𝑜 mPoly 𝑅) = (1𝑜 mPoly 𝑅) |
2 | | psr1baslem 19376 |
. . 3
⊢
(ℕ0 ↑𝑚 1𝑜) =
{𝑑 ∈
(ℕ0 ↑𝑚 1𝑜) ∣
(◡𝑑 “ ℕ) ∈
Fin} |
3 | | eqid 2610 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
4 | | eqid 2610 |
. . 3
⊢
(1r‘𝑅) = (1r‘𝑅) |
5 | | 1onn 7606 |
. . . 4
⊢
1𝑜 ∈ ω |
6 | 5 | a1i 11 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 1𝑜 ∈
ω) |
7 | | ply1coe.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
8 | | eqid 2610 |
. . . 4
⊢
(PwSer1‘𝑅) = (PwSer1‘𝑅) |
9 | | ply1coe.b |
. . . 4
⊢ 𝐵 = (Base‘𝑃) |
10 | 7, 8, 9 | ply1bas 19386 |
. . 3
⊢ 𝐵 =
(Base‘(1𝑜 mPoly 𝑅)) |
11 | | ply1coe.n |
. . . 4
⊢ · = (
·𝑠 ‘𝑃) |
12 | 7, 1, 11 | ply1vsca 19417 |
. . 3
⊢ · = (
·𝑠 ‘(1𝑜 mPoly 𝑅)) |
13 | | simpl 472 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝑅 ∈ Ring) |
14 | | simpr 476 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 ∈ 𝐵) |
15 | 1, 2, 3, 4, 6, 10,
12, 13, 14 | mplcoe1 19286 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = ((1𝑜 mPoly 𝑅) Σg
(𝑎 ∈
(ℕ0 ↑𝑚 1𝑜) ↦
((𝐾‘𝑎) · (𝑏 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))))))) |
16 | | ply1coe.a |
. . . . . . 7
⊢ 𝐴 = (coe1‘𝐾) |
17 | 16 | fvcoe1 19398 |
. . . . . 6
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → (𝐾‘𝑎) = (𝐴‘(𝑎‘∅))) |
18 | 17 | adantll 746 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → (𝐾‘𝑎) = (𝐴‘(𝑎‘∅))) |
19 | 5 | a1i 11 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → 1𝑜
∈ ω) |
20 | | eqid 2610 |
. . . . . . 7
⊢
(mulGrp‘(1𝑜 mPoly 𝑅)) = (mulGrp‘(1𝑜
mPoly 𝑅)) |
21 | | eqid 2610 |
. . . . . . 7
⊢
(.g‘(mulGrp‘(1𝑜 mPoly 𝑅))) =
(.g‘(mulGrp‘(1𝑜 mPoly 𝑅))) |
22 | | eqid 2610 |
. . . . . . 7
⊢
(1𝑜 mVar 𝑅) = (1𝑜 mVar 𝑅) |
23 | | simpll 786 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → 𝑅 ∈ Ring) |
24 | | simpr 476 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) |
25 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) →
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘∅)) = (((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘∅))) |
26 | | 0ex 4718 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
27 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ∅ →
((1𝑜 mVar 𝑅)‘𝑏) = ((1𝑜 mVar 𝑅)‘∅)) |
28 | 27 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∅ →
(((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅)) =
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘∅))) |
29 | 27 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∅ →
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑏)) =
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘∅))) |
30 | 28, 29 | eqeq12d 2625 |
. . . . . . . . . . 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 4169 |
. . . . . . . . . 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 223 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ∀𝑏 ∈ {∅}
(((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅)) =
(((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑏))) |
33 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ →
((1𝑜 mVar 𝑅)‘𝑥) = ((1𝑜 mVar 𝑅)‘∅)) |
34 | 33 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ →
(((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑥)) = (((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘∅))) |
35 | 33 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ →
(((1𝑜 mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑏)) = (((1𝑜 mVar 𝑅)‘∅)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑏))) |
36 | 34, 35 | eqeq12d 2625 |
. . . . . . . . . . 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 2969 |
. . . . . . . . . 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 4169 |
. . . . . . . . 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 223 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ∀𝑥 ∈ {∅}∀𝑏 ∈ {∅}
(((1𝑜 mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑥)) = (((1𝑜 mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑏))) |
40 | | df1o2 7459 |
. . . . . . . . 9
⊢
1𝑜 = {∅} |
41 | 40 | raleqi 3119 |
. . . . . . . . 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 2973 |
. . . . . . . 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 223 |
. . . . . . 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 19289 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → (𝑏 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))) = ((mulGrp‘(1𝑜
mPoly 𝑅))
Σg (𝑐 ∈ 1𝑜 ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐))))) |
45 | | mpteq1 4665 |
. . . . . . . . 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 6560 |
. . . . . . 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 19273 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ ω ∧ 𝑅 ∈ Ring) → (1𝑜
mPoly 𝑅) ∈
Ring) |
49 | 5, 48 | mpan 702 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(1𝑜 mPoly 𝑅) ∈ Ring) |
50 | 20 | ringmgp 18376 |
. . . . . . . . . 10
⊢
((1𝑜 mPoly 𝑅) ∈ Ring →
(mulGrp‘(1𝑜 mPoly 𝑅)) ∈ Mnd) |
51 | 49, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(mulGrp‘(1𝑜 mPoly 𝑅)) ∈ Mnd) |
52 | 51 | ad2antrr 758 |
. . . . . . . 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 18318 |
. . . . . . . . . . . . 13
⊢ 𝐵 =
(Base‘(mulGrp‘(1𝑜 mPoly 𝑅))) |
56 | 55 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 =
(Base‘(mulGrp‘(1𝑜 mPoly 𝑅)))) |
57 | | ply1coe.m |
. . . . . . . . . . . . . 14
⊢ 𝑀 = (mulGrp‘𝑃) |
58 | 57, 9 | mgpbas 18318 |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑀) |
59 | 58 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 = (Base‘𝑀)) |
60 | | ssv 3588 |
. . . . . . . . . . . . 13
⊢ 𝐵 ⊆ V |
61 | 60 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 ⊆ V) |
62 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝑎(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑏) ∈ V |
63 | 62 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑏) ∈ V) |
64 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑃) = (.r‘𝑃) |
65 | 7, 1, 64 | ply1mulr 19418 |
. . . . . . . . . . . . . . . 16
⊢
(.r‘𝑃) =
(.r‘(1𝑜 mPoly 𝑅)) |
66 | 20, 65 | mgpplusg 18316 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝑃) =
(+g‘(mulGrp‘(1𝑜 mPoly 𝑅))) |
67 | 57, 64 | mgpplusg 18316 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝑃) = (+g‘𝑀) |
68 | 66, 67 | eqtr3i 2634 |
. . . . . . . . . . . . . 14
⊢
(+g‘(mulGrp‘(1𝑜 mPoly 𝑅))) = (+g‘𝑀) |
69 | 68 | oveqi 6562 |
. . . . . . . . . . . . 13
⊢ (𝑎(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑏) = (𝑎(+g‘𝑀)𝑏) |
70 | 69 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(+g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑏) = (𝑎(+g‘𝑀)𝑏)) |
71 | 21, 54, 56, 59, 61, 63, 70 | mulgpropd 17407 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) →
(.g‘(mulGrp‘(1𝑜 mPoly 𝑅))) = ↑ ) |
72 | 71 | oveqd 6566 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋) = ((𝑎‘∅) ↑ 𝑋)) |
73 | 72 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋) = ((𝑎‘∅) ↑ 𝑋)) |
74 | 7 | ply1ring 19439 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
75 | 57 | ringmgp 18376 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring → 𝑀 ∈ Mnd) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
77 | 76 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → 𝑀 ∈ Mnd) |
78 | | elmapi 7765 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) → 𝑎:1𝑜⟶ℕ0) |
79 | | 0lt1o 7471 |
. . . . . . . . . . . 12
⊢ ∅
∈ 1𝑜 |
80 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝑎:1𝑜⟶ℕ0
∧ ∅ ∈ 1𝑜) → (𝑎‘∅) ∈
ℕ0) |
81 | 78, 79, 80 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) → (𝑎‘∅) ∈
ℕ0) |
82 | 81 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → (𝑎‘∅) ∈
ℕ0) |
83 | | ply1coe.x |
. . . . . . . . . . . 12
⊢ 𝑋 = (var1‘𝑅) |
84 | 83, 7, 9 | vr1cl 19408 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) |
85 | 84 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → 𝑋 ∈ 𝐵) |
86 | 58, 54 | mulgnn0cl 17381 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ (𝑎‘∅) ∈
ℕ0 ∧ 𝑋
∈ 𝐵) → ((𝑎‘∅) ↑ 𝑋) ∈ 𝐵) |
87 | 77, 82, 85, 86 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ((𝑎‘∅) ↑ 𝑋) ∈ 𝐵) |
88 | 73, 87 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋) ∈ 𝐵) |
89 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑐 = ∅ → (𝑎‘𝑐) = (𝑎‘∅)) |
90 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑐 = ∅ →
((1𝑜 mVar 𝑅)‘𝑐) = ((1𝑜 mVar 𝑅)‘∅)) |
91 | 83 | vr1val 19383 |
. . . . . . . . . . 11
⊢ 𝑋 = ((1𝑜 mVar
𝑅)‘∅) |
92 | 90, 91 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑐 = ∅ →
((1𝑜 mVar 𝑅)‘𝑐) = 𝑋) |
93 | 89, 92 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑐 = ∅ → ((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐)) = ((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋)) |
94 | 55, 93 | gsumsn 18177 |
. . . . . . . 8
⊢
(((mulGrp‘(1𝑜 mPoly 𝑅)) ∈ Mnd ∧ ∅ ∈ V ∧
((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋) ∈ 𝐵) →
((mulGrp‘(1𝑜 mPoly 𝑅))
Σg (𝑐 ∈ {∅} ↦
((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜 mPoly 𝑅)))((1𝑜 mVar 𝑅)‘𝑐)))) =
((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋)) |
95 | 52, 53, 88, 94 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) →
((mulGrp‘(1𝑜 mPoly 𝑅)) Σg (𝑐 ∈ {∅} ↦
((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐)))) = ((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋)) |
96 | 47, 95 | syl5eq 2656 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) →
((mulGrp‘(1𝑜 mPoly 𝑅)) Σg (𝑐 ∈ 1𝑜
↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))((1𝑜 mVar
𝑅)‘𝑐)))) = ((𝑎‘∅)(.g‘(mulGrp‘(1𝑜
mPoly 𝑅)))𝑋)) |
97 | 44, 96, 73 | 3eqtrd 2648 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → (𝑏 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))) = ((𝑎‘∅) ↑ 𝑋)) |
98 | 18, 97 | oveq12d 6567 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0
↑𝑚 1𝑜)) → ((𝐾‘𝑎) · (𝑏 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅)))) = ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))) |
99 | 98 | mpteq2dva 4672 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))))) = (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))) |
100 | 99 | oveq2d 6565 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1𝑜 mPoly 𝑅) Σg
(𝑎 ∈
(ℕ0 ↑𝑚 1𝑜) ↦
((𝐾‘𝑎) · (𝑏 ∈ (ℕ0
↑𝑚 1𝑜) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅)))))) = ((1𝑜 mPoly 𝑅) Σg
(𝑎 ∈
(ℕ0 ↑𝑚 1𝑜) ↦
((𝐴‘(𝑎‘∅)) ·
((𝑎‘∅) ↑ 𝑋))))) |
101 | | nn0ex 11175 |
. . . . . 6
⊢
ℕ0 ∈ V |
102 | 101 | mptex 6390 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∈ V |
103 | 102 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∈ V) |
104 | | fvex 6113 |
. . . . . 6
⊢
(Poly1‘𝑅) ∈ V |
105 | 7, 104 | eqeltri 2684 |
. . . . 5
⊢ 𝑃 ∈ V |
106 | 105 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝑃 ∈ V) |
107 | | ovex 6577 |
. . . . 5
⊢
(1𝑜 mPoly 𝑅) ∈ V |
108 | 107 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1𝑜 mPoly 𝑅) ∈ V) |
109 | 9, 10 | eqtr3i 2634 |
. . . . 5
⊢
(Base‘𝑃) =
(Base‘(1𝑜 mPoly 𝑅)) |
110 | 109 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (Base‘𝑃) = (Base‘(1𝑜 mPoly
𝑅))) |
111 | | eqid 2610 |
. . . . . 6
⊢
(+g‘𝑃) = (+g‘𝑃) |
112 | 7, 1, 111 | ply1plusg 19416 |
. . . . 5
⊢
(+g‘𝑃) =
(+g‘(1𝑜 mPoly 𝑅)) |
113 | 112 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (+g‘𝑃) =
(+g‘(1𝑜 mPoly 𝑅))) |
114 | 103, 106,
108, 110, 113 | gsumpropd 17095 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) = ((1𝑜 mPoly 𝑅) Σg
(𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))))) |
115 | | eqid 2610 |
. . . . 5
⊢
(0g‘𝑃) = (0g‘𝑃) |
116 | 1, 7, 115 | ply1mpl0 19446 |
. . . 4
⊢
(0g‘𝑃) =
(0g‘(1𝑜 mPoly 𝑅)) |
117 | 1 | mpllmod 19272 |
. . . . . 6
⊢
((1𝑜 ∈ ω ∧ 𝑅 ∈ Ring) → (1𝑜
mPoly 𝑅) ∈
LMod) |
118 | 5, 13, 117 | sylancr 694 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1𝑜 mPoly 𝑅) ∈ LMod) |
119 | | lmodcmn 18734 |
. . . . 5
⊢
((1𝑜 mPoly 𝑅) ∈ LMod → (1𝑜
mPoly 𝑅) ∈
CMnd) |
120 | 118, 119 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1𝑜 mPoly 𝑅) ∈ CMnd) |
121 | 101 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ℕ0 ∈
V) |
122 | 7 | ply1lmod 19443 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
123 | 122 | ad2antrr 758 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑃 ∈ LMod) |
124 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
125 | 16, 9, 7, 124 | coe1f 19402 |
. . . . . . . . 9
⊢ (𝐾 ∈ 𝐵 → 𝐴:ℕ0⟶(Base‘𝑅)) |
126 | 125 | adantl 481 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐴:ℕ0⟶(Base‘𝑅)) |
127 | 126 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘𝑅)) |
128 | 7 | ply1sca 19444 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
129 | 128 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(Scalar‘𝑃) = 𝑅) |
130 | 129 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
(Scalar‘𝑃) = 𝑅) |
131 | 130 | fveq2d 6107 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
(Base‘(Scalar‘𝑃)) = (Base‘𝑅)) |
132 | 127, 131 | eleqtrrd 2691 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑃))) |
133 | 76 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈ Mnd) |
134 | | simpr 476 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
135 | 84 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
136 | 58, 54 | mulgnn0cl 17381 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ 𝑘 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝑘 ↑ 𝑋) ∈ 𝐵) |
137 | 133, 134,
135, 136 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐵) |
138 | | eqid 2610 |
. . . . . . 7
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
139 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
140 | 9, 138, 11, 139 | lmodvscl 18703 |
. . . . . 6
⊢ ((𝑃 ∈ LMod ∧ (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑘 ↑ 𝑋) ∈ 𝐵) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐵) |
141 | 123, 132,
137, 140 | syl3anc 1318 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐵) |
142 | | eqid 2610 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) |
143 | 141, 142 | fmptd 6292 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))):ℕ0⟶𝐵) |
144 | 7, 83, 9, 11, 57, 54, 16 | ply1coefsupp 19486 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃)) |
145 | | eqid 2610 |
. . . . . 6
⊢ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅)) |
146 | 40, 101, 26, 145 | mapsnf1o2 7791 |
. . . . 5
⊢ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅)):(ℕ0
↑𝑚 1𝑜)–1-1-onto→ℕ0 |
147 | 146 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅)):(ℕ0
↑𝑚 1𝑜)–1-1-onto→ℕ0) |
148 | 10, 116, 120, 121, 143, 144, 147 | gsumf1o 18140 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1𝑜 mPoly 𝑅) Σg
(𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) = ((1𝑜 mPoly 𝑅) Σg
((𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅))))) |
149 | | eqidd 2611 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅))) |
150 | | eqidd 2611 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) |
151 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = (𝑎‘∅) → (𝐴‘𝑘) = (𝐴‘(𝑎‘∅))) |
152 | | oveq1 6556 |
. . . . . 6
⊢ (𝑘 = (𝑎‘∅) → (𝑘 ↑ 𝑋) = ((𝑎‘∅) ↑ 𝑋)) |
153 | 151, 152 | oveq12d 6567 |
. . . . 5
⊢ (𝑘 = (𝑎‘∅) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) = ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))) |
154 | 82, 149, 150, 153 | fmptco 6303 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅))) = (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))) |
155 | 154 | oveq2d 6565 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1𝑜 mPoly 𝑅) Σg
((𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ (𝑎‘∅)))) = ((1𝑜
mPoly 𝑅)
Σg (𝑎 ∈ (ℕ0
↑𝑚 1𝑜) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))))) |
156 | 114, 148,
155 | 3eqtrrd 2649 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1𝑜 mPoly 𝑅) Σg
(𝑎 ∈
(ℕ0 ↑𝑚 1𝑜) ↦
((𝐴‘(𝑎‘∅)) ·
((𝑎‘∅) ↑ 𝑋)))) = (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))))) |
157 | 15, 100, 156 | 3eqtrd 2648 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))))) |