Theorem mpfmulcl

Description: The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015)

	Ref	Expression
Hypotheses	mpfsubrg.q	⊢ 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	mpfmulcl.t	⊢ · = ( .r ‘ 𝑆 )
Assertion	mpfmulcl	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ∘f · 𝐺 ) ∈ 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		mpfsubrg.q	⊢ 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		mpfmulcl.t	⊢ · = ( .r ‘ 𝑆 )
3		eqid	⊢ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) = ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) )
4		eqid	⊢ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) )
5	1	mpfrcl	⊢ ( 𝐹 ∈ 𝑄 → ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) )
6	5	adantr	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) )
7	6	simp2d	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝑆 ∈ CRing )
8		ovexd	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ∈ V )
9	1	mpfsubrg	⊢ ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( SubRing ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
10	6 9	syl	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝑄 ∈ ( SubRing ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
11	4	subrgss	⊢ ( 𝑄 ∈ ( SubRing ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) → 𝑄 ⊆ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
12	10 11	syl	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝑄 ⊆ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
13		simpl	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝐹 ∈ 𝑄 )
14	12 13	sseldd	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝐹 ∈ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
15		simpr	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝐺 ∈ 𝑄 )
16	12 15	sseldd	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝐺 ∈ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
17		eqid	⊢ ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) = ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) )
18	3 4 7 8 14 16 2 17	pwsmulrval	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) 𝐺 ) = ( 𝐹 ∘f · 𝐺 ) )
19	17	subrgmcl	⊢ ( ( 𝑄 ∈ ( SubRing ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ∧ 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) 𝐺 ) ∈ 𝑄 )
20	19	3expib	⊢ ( 𝑄 ∈ ( SubRing ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) → ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) 𝐺 ) ∈ 𝑄 ) )
21	10 20	mpcom	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ( .r ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) 𝐺 ) ∈ 𝑄 )
22	18 21	eqeltrrd	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ∘f · 𝐺 ) ∈ 𝑄 )