Theorem ply1moncl

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

	Ref	Expression
Hypotheses	ply1moncl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1moncl.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	ply1moncl.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
	ply1moncl.e	⊢ ↑ = ( .g ‘ 𝑁 )
	ply1moncl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion	ply1moncl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0 ) → ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ply1moncl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1moncl.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
3		ply1moncl.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
4		ply1moncl.e	⊢ ↑ = ( .g ‘ 𝑁 )
5		ply1moncl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
6	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
7	3	ringmgp	⊢ ( 𝑃 ∈ Ring → 𝑁 ∈ Mnd )
8	6 7	syl	⊢ ( 𝑅 ∈ Ring → 𝑁 ∈ Mnd )
9	8	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0 ) → 𝑁 ∈ Mnd )
10		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0 ) → 𝐷 ∈ ℕ0 )
11	2 1 5	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
12	11	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
13	3 5	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑁 )
14	13 4	mulgnn0cl	⊢ ( ( 𝑁 ∈ Mnd ∧ 𝐷 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 )
15	9 10 12 14	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0 ) → ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 )