This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )