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		df-base	⊢ Base = Slot 1
15	14 1	strfvi	⊢ 𝐾 = ( Base ‘ ( I ‘ 𝑅 ) )
16	7 13 4 15	lmodvscl	⊢ ( ( 𝑃 ∈ LMod ∧ 𝐶 ∈ 𝐾 ∧ ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 ) → ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∈ 𝐵 )
17	9 10 12 16	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∈ 𝐵 )