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 → ( coe1 ‘ 0 ) = ( ℕ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 × { 𝑎 } ) ∈ ( ℕ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 × { 𝑌 } ) )