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 ⊢ 𝑃 = ( 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 3 5 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑁 )
7 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
8 3 ringmgp ⊢ ( 𝑃 ∈ Ring → 𝑁 ∈ Mnd )
9 7 8 syl ⊢ ( 𝑅 ∈ Ring → 𝑁 ∈ Mnd )
10 9 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0 ) → 𝑁 ∈ Mnd )
11 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0 ) → 𝐷 ∈ ℕ0 )
12 2 1 5 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
13 12 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
14 6 4 10 11 13 mulgnn0cld ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0 ) → ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 )