Step |
Hyp |
Ref |
Expression |
1 |
|
coe1z.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
2 |
|
coe1z.z |
⊢ 0 = ( 0g ‘ 𝑃 ) |
3 |
|
coe1z.y |
⊢ 𝑌 = ( 0g ‘ 𝑅 ) |
4 |
|
fconst6g |
⊢ ( 𝑎 ∈ ℕ0 → ( 1o × { 𝑎 } ) : 1o ⟶ ℕ0 ) |
5 |
4
|
adantl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ ℕ0 ) → ( 1o × { 𝑎 } ) : 1o ⟶ ℕ0 ) |
6 |
|
nn0ex |
⊢ ℕ0 ∈ V |
7 |
|
1oex |
⊢ 1o ∈ V |
8 |
6 7
|
elmap |
⊢ ( ( 1o × { 𝑎 } ) ∈ ( ℕ0 ↑m 1o ) ↔ ( 1o × { 𝑎 } ) : 1o ⟶ ℕ0 ) |
9 |
5 8
|
sylibr |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ ℕ0 ) → ( 1o × { 𝑎 } ) ∈ ( ℕ0 ↑m 1o ) ) |
10 |
|
eqidd |
⊢ ( 𝑅 ∈ Ring → ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) = ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) |
11 |
|
eqid |
⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 ) |
12 |
|
psr1baslem |
⊢ ( ℕ0 ↑m 1o ) = { 𝑐 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } |
13 |
11 1 2
|
ply1mpl0 |
⊢ 0 = ( 0g ‘ ( 1o mPoly 𝑅 ) ) |
14 |
|
1on |
⊢ 1o ∈ On |
15 |
14
|
a1i |
⊢ ( 𝑅 ∈ Ring → 1o ∈ On ) |
16 |
|
ringgrp |
⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp ) |
17 |
11 12 3 13 15 16
|
mpl0 |
⊢ ( 𝑅 ∈ Ring → 0 = ( ( ℕ0 ↑m 1o ) × { 𝑌 } ) ) |
18 |
|
fconstmpt |
⊢ ( ( ℕ0 ↑m 1o ) × { 𝑌 } ) = ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ 𝑌 ) |
19 |
17 18
|
eqtrdi |
⊢ ( 𝑅 ∈ Ring → 0 = ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ 𝑌 ) ) |
20 |
|
eqidd |
⊢ ( 𝑏 = ( 1o × { 𝑎 } ) → 𝑌 = 𝑌 ) |
21 |
9 10 19 20
|
fmptco |
⊢ ( 𝑅 ∈ Ring → ( 0 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) = ( 𝑎 ∈ ℕ0 ↦ 𝑌 ) ) |
22 |
1
|
ply1ring |
⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring ) |
23 |
|
eqid |
⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) |
24 |
23 2
|
ring0cl |
⊢ ( 𝑃 ∈ Ring → 0 ∈ ( Base ‘ 𝑃 ) ) |
25 |
|
eqid |
⊢ ( coe1 ‘ 0 ) = ( coe1 ‘ 0 ) |
26 |
|
eqid |
⊢ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) = ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) |
27 |
25 23 1 26
|
coe1fval2 |
⊢ ( 0 ∈ ( Base ‘ 𝑃 ) → ( coe1 ‘ 0 ) = ( 0 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ) |
28 |
22 24 27
|
3syl |
⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ 0 ) = ( 0 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ) |
29 |
|
fconstmpt |
⊢ ( ℕ0 × { 𝑌 } ) = ( 𝑎 ∈ ℕ0 ↦ 𝑌 ) |
30 |
29
|
a1i |
⊢ ( 𝑅 ∈ Ring → ( ℕ0 × { 𝑌 } ) = ( 𝑎 ∈ ℕ0 ↦ 𝑌 ) ) |
31 |
21 28 30
|
3eqtr4d |
⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ 0 ) = ( ℕ0 × { 𝑌 } ) ) |