Metamath Proof Explorer


Theorem coe1z

Description: The coefficient vector of 0. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses coe1z.p 𝑃 = ( Poly1𝑅 )
coe1z.z 0 = ( 0g𝑃 )
coe1z.y 𝑌 = ( 0g𝑅 )
Assertion coe1z ( 𝑅 ∈ Ring → ( coe10 ) = ( ℕ0 × { 𝑌 } ) )

Proof

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 × { 𝑎 } ) ∈ ( ℕ0m 1o ) ↔ ( 1o × { 𝑎 } ) : 1o ⟶ ℕ0 )
9 5 8 sylibr ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ ℕ0 ) → ( 1o × { 𝑎 } ) ∈ ( ℕ0m 1o ) )
10 eqidd ( 𝑅 ∈ Ring → ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) = ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) )
11 eqid ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
12 psr1baslem ( ℕ0m 1o ) = { 𝑐 ∈ ( ℕ0m 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 = ( ( ℕ0m 1o ) × { 𝑌 } ) )
18 fconstmpt ( ( ℕ0m 1o ) × { 𝑌 } ) = ( 𝑏 ∈ ( ℕ0m 1o ) ↦ 𝑌 )
19 17 18 eqtrdi ( 𝑅 ∈ Ring → 0 = ( 𝑏 ∈ ( ℕ0m 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 ( coe10 ) = ( coe10 )
26 eqid ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) = ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) )
27 25 23 1 26 coe1fval2 ( 0 ∈ ( Base ‘ 𝑃 ) → ( coe10 ) = ( 0 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
28 22 24 27 3syl ( 𝑅 ∈ Ring → ( coe10 ) = ( 0 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
29 fconstmpt ( ℕ0 × { 𝑌 } ) = ( 𝑎 ∈ ℕ0𝑌 )
30 29 a1i ( 𝑅 ∈ Ring → ( ℕ0 × { 𝑌 } ) = ( 𝑎 ∈ ℕ0𝑌 ) )
31 21 28 30 3eqtr4d ( 𝑅 ∈ Ring → ( coe10 ) = ( ℕ0 × { 𝑌 } ) )