coe1z

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

	Ref	Expression
Hypotheses	coe1z.p	\|- P = ( Poly1 ` R )
	coe1z.z	\|- .0. = ( 0g ` P )
	coe1z.y	\|- Y = ( 0g ` R )
Assertion	coe1z	\|- ( R e. Ring -> ( coe1 ` .0. ) = ( NN0 X. { Y } ) )

Proof

Step	Hyp	Ref	Expression
1		coe1z.p	\|- P = ( Poly1 ` R )
2		coe1z.z	\|- .0. = ( 0g ` P )
3		coe1z.y	\|- Y = ( 0g ` R )
4		fconst6g	\|- ( a e. NN0 -> ( 1o X. { a } ) : 1o --> NN0 )
5	4	adantl	\|- ( ( R e. Ring /\ a e. NN0 ) -> ( 1o X. { a } ) : 1o --> NN0 )
6		nn0ex	\|- NN0 e. _V
7		1oex	\|- 1o e. _V
8	6 7	elmap	\|- ( ( 1o X. { a } ) e. ( NN0 ^m 1o ) <-> ( 1o X. { a } ) : 1o --> NN0 )
9	5 8	sylibr	\|- ( ( R e. Ring /\ a e. NN0 ) -> ( 1o X. { a } ) e. ( NN0 ^m 1o ) )
10		eqidd	\|- ( R e. Ring -> ( a e. NN0 \|-> ( 1o X. { a } ) ) = ( a e. NN0 \|-> ( 1o X. { a } ) ) )
11		eqid	\|- ( 1o mPoly R ) = ( 1o mPoly R )
12		psr1baslem	\|- ( NN0 ^m 1o ) = { c e. ( NN0 ^m 1o ) \| ( `' c " NN ) e. Fin }
13	11 1 2	ply1mpl0	\|- .0. = ( 0g ` ( 1o mPoly R ) )
14		1on	\|- 1o e. On
15	14	a1i	\|- ( R e. Ring -> 1o e. On )
16		ringgrp	\|- ( R e. Ring -> R e. Grp )
17	11 12 3 13 15 16	mpl0	\|- ( R e. Ring -> .0. = ( ( NN0 ^m 1o ) X. { Y } ) )
18		fconstmpt	\|- ( ( NN0 ^m 1o ) X. { Y } ) = ( b e. ( NN0 ^m 1o ) \|-> Y )
19	17 18	eqtrdi	\|- ( R e. Ring -> .0. = ( b e. ( NN0 ^m 1o ) \|-> Y ) )
20		eqidd	\|- ( b = ( 1o X. { a } ) -> Y = Y )
21	9 10 19 20	fmptco	\|- ( R e. Ring -> ( .0. o. ( a e. NN0 \|-> ( 1o X. { a } ) ) ) = ( a e. NN0 \|-> Y ) )
22	1	ply1ring	\|- ( R e. Ring -> P e. Ring )
23		eqid	\|- ( Base ` P ) = ( Base ` P )
24	23 2	ring0cl	\|- ( P e. Ring -> .0. e. ( Base ` P ) )
25		eqid	\|- ( coe1 ` .0. ) = ( coe1 ` .0. )
26		eqid	\|- ( a e. NN0 \|-> ( 1o X. { a } ) ) = ( a e. NN0 \|-> ( 1o X. { a } ) )
27	25 23 1 26	coe1fval2	\|- ( .0. e. ( Base ` P ) -> ( coe1 ` .0. ) = ( .0. o. ( a e. NN0 \|-> ( 1o X. { a } ) ) ) )
28	22 24 27	3syl	\|- ( R e. Ring -> ( coe1 ` .0. ) = ( .0. o. ( a e. NN0 \|-> ( 1o X. { a } ) ) ) )
29		fconstmpt	\|- ( NN0 X. { Y } ) = ( a e. NN0 \|-> Y )
30	29	a1i	\|- ( R e. Ring -> ( NN0 X. { Y } ) = ( a e. NN0 \|-> Y ) )
31	21 28 30	3eqtr4d	\|- ( R e. Ring -> ( coe1 ` .0. ) = ( NN0 X. { Y } ) )

Metamath Proof Explorer

Theorem coe1z

Proof