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	1	ply1ring	|- ( R e. Ring -> P e. Ring )
7	3	ringmgp	|- ( P e. Ring -> N e. Mnd )
8	6 7	syl	|- ( R e. Ring -> N e. Mnd )
9	8	adantr	|- ( ( R e. Ring /\ D e. NN0 ) -> N e. Mnd )
10		simpr	|- ( ( R e. Ring /\ D e. NN0 ) -> D e. NN0 )
11	2 1 5	vr1cl	|- ( R e. Ring -> X e. B )
12	11	adantr	|- ( ( R e. Ring /\ D e. NN0 ) -> X e. B )
13	3 5	mgpbas	|- B = ( Base ` N )
14	13 4	mulgnn0cl	|- ( ( N e. Mnd /\ D e. NN0 /\ X e. B ) -> ( D .^ X ) e. B )
15	9 10 12 14	syl3anc	|- ( ( R e. Ring /\ D e. NN0 ) -> ( D .^ X ) e. B )