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

Metamath Proof Explorer

Theorem ply1moncl

Description: Closure of the expression for a univariate primitive monomial. (Contributed by AV, 14-Aug-2019)

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

Proof

Step Hyp Ref Expression
1 ply1moncl.p 
 |-  P = ( Poly1 ` R )
2 ply1moncl.x 
 |-  X = ( var1 ` R )
3 ply1moncl.n 
 |-  N = ( mulGrp ` P )
4 ply1moncl.e 
 |-  .^ = ( .g ` N )
5 ply1moncl.b 
 |-  B = ( Base ` P )
6 3 5 mgpbas 
 |-  B = ( Base ` N )
7 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
8 3 ringmgp 
 |-  ( P e. Ring -> N e. Mnd )
9 7 8 syl 
 |-  ( R e. Ring -> N e. Mnd )
10 9 adantr 
 |-  ( ( R e. Ring /\ D e. NN0 ) -> N e. Mnd )
11 simpr 
 |-  ( ( R e. Ring /\ D e. NN0 ) -> D e. NN0 )
12 2 1 5 vr1cl 
 |-  ( R e. Ring -> X e. B )
13 12 adantr 
 |-  ( ( R e. Ring /\ D e. NN0 ) -> X e. B )
14 6 4 10 11 13 mulgnn0cld 
 |-  ( ( R e. Ring /\ D e. NN0 ) -> ( D .^ X ) e. B )