Theorem ply1tmcl

Description: Closure of the expression for a univariate polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015) (Proof shortened by AV, 25-Nov-2019)

	Ref	Expression
Hypotheses	ply1tmcl.k	|- K = ( Base ` R )
	ply1tmcl.p	|- P = ( Poly1 ` R )
	ply1tmcl.x	|- X = ( var1 ` R )
	ply1tmcl.m	|- .x. = ( .s ` P )
	ply1tmcl.n	|- N = ( mulGrp ` P )
	ply1tmcl.e	|- .^ = ( .g ` N )
	ply1tmcl.b	|- B = ( Base ` P )
Assertion	ply1tmcl	|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( C .x. ( D .^ X ) ) e. B )

Proof

Step	Hyp	Ref	Expression
1		ply1tmcl.k	|- K = ( Base ` R )
2		ply1tmcl.p	|- P = ( Poly1 ` R )
3		ply1tmcl.x	|- X = ( var1 ` R )
4		ply1tmcl.m	|- .x. = ( .s ` P )
5		ply1tmcl.n	|- N = ( mulGrp ` P )
6		ply1tmcl.e	|- .^ = ( .g ` N )
7		ply1tmcl.b	|- B = ( Base ` P )
8	2	ply1lmod	|- ( R e. Ring -> P e. LMod )
9	8	3ad2ant1	|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> P e. LMod )
10		simp2	|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> C e. K )
11	2 3 5 6 7	ply1moncl	|- ( ( R e. Ring /\ D e. NN0 ) -> ( D .^ X ) e. B )
12	11	3adant2	|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( D .^ X ) e. B )
13	2	ply1sca2	|- ( _I ` R ) = ( Scalar ` P )
14		baseid	|- Base = Slot ( Base ` ndx )
15	14 1	strfvi	|- K = ( Base ` ( _I ` R ) )
16	7 13 4 15	lmodvscl	|- ( ( P e. LMod /\ C e. K /\ ( D .^ X ) e. B ) -> ( C .x. ( D .^ X ) ) e. B )
17	9 10 12 16	syl3anc	|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( C .x. ( D .^ X ) ) e. B )