Theorem coe1sclmulval

Description: The value of the coefficient vector of a polynomial multiplied on the left by a scalar. (Contributed by AV, 14-Aug-2019)

	Ref	Expression
Hypotheses	coe1sclmulval.p	|- P = ( Poly1 ` R )
	coe1sclmulval.b	|- B = ( Base ` P )
	coe1sclmulval.k	|- K = ( Base ` R )
	coe1sclmulval.a	|- A = ( algSc ` P )
	coe1sclmulval.s	|- S = ( .s ` P )
	coe1sclmulval.t	|- .xb = ( .r ` P )
	coe1sclmulval.u	|- .x. = ( .r ` R )
Assertion	coe1sclmulval	|- ( ( R e. Ring /\ ( Y e. K /\ Z e. B ) /\ N e. NN0 ) -> ( ( coe1 ` ( Y S Z ) ) ` N ) = ( Y .x. ( ( coe1 ` Z ) ` N ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1sclmulval.p	|- P = ( Poly1 ` R )
2		coe1sclmulval.b	|- B = ( Base ` P )
3		coe1sclmulval.k	|- K = ( Base ` R )
4		coe1sclmulval.a	|- A = ( algSc ` P )
5		coe1sclmulval.s	|- S = ( .s ` P )
6		coe1sclmulval.t	|- .xb = ( .r ` P )
7		coe1sclmulval.u	|- .x. = ( .r ` R )
8		simp1	|- ( ( R e. Ring /\ ( Y e. K /\ Z e. B ) /\ N e. NN0 ) -> R e. Ring )
9		simp2l	|- ( ( R e. Ring /\ ( Y e. K /\ Z e. B ) /\ N e. NN0 ) -> Y e. K )
10		simp2r	|- ( ( R e. Ring /\ ( Y e. K /\ Z e. B ) /\ N e. NN0 ) -> Z e. B )
11		eqid	|- ( var1 ` R ) = ( var1 ` R )
12		eqid	|- ( mulGrp ` P ) = ( mulGrp ` P )
13		eqid	|- ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
14		eqid	|- ( algSc ` P ) = ( algSc ` P )
15	3 1 2 11 5 6 12 13 14	ply1sclrmsm	|- ( ( R e. Ring /\ Y e. K /\ Z e. B ) -> ( ( ( algSc ` P ) ` Y ) .xb Z ) = ( Y S Z ) )
16	8 9 10 15	syl3anc	|- ( ( R e. Ring /\ ( Y e. K /\ Z e. B ) /\ N e. NN0 ) -> ( ( ( algSc ` P ) ` Y ) .xb Z ) = ( Y S Z ) )
17	16	eqcomd	|- ( ( R e. Ring /\ ( Y e. K /\ Z e. B ) /\ N e. NN0 ) -> ( Y S Z ) = ( ( ( algSc ` P ) ` Y ) .xb Z ) )
18	17	fveq2d	|- ( ( R e. Ring /\ ( Y e. K /\ Z e. B ) /\ N e. NN0 ) -> ( coe1 ` ( Y S Z ) ) = ( coe1 ` ( ( ( algSc ` P ) ` Y ) .xb Z ) ) )
19	18	fveq1d	|- ( ( R e. Ring /\ ( Y e. K /\ Z e. B ) /\ N e. NN0 ) -> ( ( coe1 ` ( Y S Z ) ) ` N ) = ( ( coe1 ` ( ( ( algSc ` P ) ` Y ) .xb Z ) ) ` N ) )
20	1 2 3 14 6 7	coe1sclmulfv	|- ( ( R e. Ring /\ ( Y e. K /\ Z e. B ) /\ N e. NN0 ) -> ( ( coe1 ` ( ( ( algSc ` P ) ` Y ) .xb Z ) ) ` N ) = ( Y .x. ( ( coe1 ` Z ) ` N ) ) )
21	19 20	eqtrd	|- ( ( R e. Ring /\ ( Y e. K /\ Z e. B ) /\ N e. NN0 ) -> ( ( coe1 ` ( Y S Z ) ) ` N ) = ( Y .x. ( ( coe1 ` Z ) ` N ) ) )