Theorem ply1scltm

Description: A scalar is a term with zero exponent. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	ply1scltm.k	|- K = ( Base ` R )
	ply1scltm.p	|- P = ( Poly1 ` R )
	ply1scltm.x	|- X = ( var1 ` R )
	ply1scltm.m	|- .x. = ( .s ` P )
	ply1scltm.n	|- N = ( mulGrp ` P )
	ply1scltm.e	|- .^ = ( .g ` N )
	ply1scltm.a	|- A = ( algSc ` P )
Assertion	ply1scltm	|- ( ( R e. Ring /\ F e. K ) -> ( A ` F ) = ( F .x. ( 0 .^ X ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1scltm.k	|- K = ( Base ` R )
2		ply1scltm.p	|- P = ( Poly1 ` R )
3		ply1scltm.x	|- X = ( var1 ` R )
4		ply1scltm.m	|- .x. = ( .s ` P )
5		ply1scltm.n	|- N = ( mulGrp ` P )
6		ply1scltm.e	|- .^ = ( .g ` N )
7		ply1scltm.a	|- A = ( algSc ` P )
8	2	ply1sca2	|- ( _I ` R ) = ( Scalar ` P )
9		baseid	|- Base = Slot ( Base ` ndx )
10	9 1	strfvi	|- K = ( Base ` ( _I ` R ) )
11		eqid	|- ( 1r ` P ) = ( 1r ` P )
12	7 8 10 4 11	asclval	|- ( F e. K -> ( A ` F ) = ( F .x. ( 1r ` P ) ) )
13	12	adantl	|- ( ( R e. Ring /\ F e. K ) -> ( A ` F ) = ( F .x. ( 1r ` P ) ) )
14		eqid	|- ( Base ` P ) = ( Base ` P )
15	3 2 14	vr1cl	|- ( R e. Ring -> X e. ( Base ` P ) )
16	5 14	mgpbas	|- ( Base ` P ) = ( Base ` N )
17	5 11	ringidval	|- ( 1r ` P ) = ( 0g ` N )
18	16 17 6	mulg0	|- ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 1r ` P ) )
19	15 18	syl	|- ( R e. Ring -> ( 0 .^ X ) = ( 1r ` P ) )
20	19	adantr	|- ( ( R e. Ring /\ F e. K ) -> ( 0 .^ X ) = ( 1r ` P ) )
21	20	oveq2d	|- ( ( R e. Ring /\ F e. K ) -> ( F .x. ( 0 .^ X ) ) = ( F .x. ( 1r ` P ) ) )
22	13 21	eqtr4d	|- ( ( R e. Ring /\ F e. K ) -> ( A ` F ) = ( F .x. ( 0 .^ X ) ) )