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 ⊢ 𝐾 = ( Base ‘ 𝑅 )
ply1tmcl.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1tmcl.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
ply1tmcl.m ⊢ · = ( ·𝑠 ‘ 𝑃 )
ply1tmcl.n ⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
ply1tmcl.e ⊢ ↑ = ( .g ‘ 𝑁 )
ply1tmcl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion ply1tmcl ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ply1tmcl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 ply1tmcl.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 ply1tmcl.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
4 ply1tmcl.m ⊢ · = ( ·𝑠 ‘ 𝑃 )
5 ply1tmcl.n ⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
6 ply1tmcl.e ⊢ ↑ = ( .g ‘ 𝑁 )
7 ply1tmcl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
8 2 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
9 8 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → 𝑃 ∈ LMod )
10 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → 𝐶 ∈ 𝐾 )
11 2 3 5 6 7 ply1moncl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0 ) → ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 )
12 11 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 )
13 2 ply1sca2 ⊢ ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 )
14 baseid ⊢ Base = Slot ( Base ‘ ndx )
15 14 1 strfvi ⊢ 𝐾 = ( Base ‘ ( I ‘ 𝑅 ) )
16 7 13 4 15 lmodvscl ⊢ ( ( 𝑃 ∈ LMod ∧ 𝐶 ∈ 𝐾 ∧ ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 ) → ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∈ 𝐵 )
17 9 10 12 16 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∈ 𝐵 )