Theorem pf1mulcl

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

	Ref	Expression
Hypotheses	pf1rcl.q	⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
	pf1mulcl.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	pf1mulcl	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ∘f · 𝐺 ) ∈ 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		pf1rcl.q	⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
2		pf1mulcl.t	⊢ · = ( .r ‘ 𝑅 )
3		eqid	⊢ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) = ( 𝑅 ↑s ( Base ‘ 𝑅 ) )
4		eqid	⊢ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) = ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) )
5	1	pf1rcl	⊢ ( 𝐹 ∈ 𝑄 → 𝑅 ∈ CRing )
6	5	adantr	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝑅 ∈ CRing )
7		fvexd	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( Base ‘ 𝑅 ) ∈ V )
8		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9	1 8	pf1f	⊢ ( 𝐹 ∈ 𝑄 → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
10	9	adantr	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
11		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
12	3 8 4	pwselbasb	⊢ ( ( 𝑅 ∈ CRing ∧ ( Base ‘ 𝑅 ) ∈ V ) → ( 𝐹 ∈ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) ↔ 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) ) )
13	6 11 12	sylancl	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ∈ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) ↔ 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) ) )
14	10 13	mpbird	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝐹 ∈ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) )
15	1 8	pf1f	⊢ ( 𝐺 ∈ 𝑄 → 𝐺 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
16	15	adantl	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝐺 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
17	3 8 4	pwselbasb	⊢ ( ( 𝑅 ∈ CRing ∧ ( Base ‘ 𝑅 ) ∈ V ) → ( 𝐺 ∈ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) ↔ 𝐺 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) ) )
18	6 11 17	sylancl	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐺 ∈ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) ↔ 𝐺 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) ) )
19	16 18	mpbird	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝐺 ∈ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) )
20		eqid	⊢ ( .r ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) = ( .r ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) )
21	3 4 6 7 14 19 2 20	pwsmulrval	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ( .r ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) 𝐺 ) = ( 𝐹 ∘f · 𝐺 ) )
22	8 1	pf1subrg	⊢ ( 𝑅 ∈ CRing → 𝑄 ∈ ( SubRing ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) )
23	6 22	syl	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → 𝑄 ∈ ( SubRing ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) )
24	20	subrgmcl	⊢ ( ( 𝑄 ∈ ( SubRing ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) ∧ 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ( .r ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) 𝐺 ) ∈ 𝑄 )
25	24	3expib	⊢ ( 𝑄 ∈ ( SubRing ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) → ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ( .r ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) 𝐺 ) ∈ 𝑄 ) )
26	23 25	mpcom	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ( .r ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) 𝐺 ) ∈ 𝑄 )
27	21 26	eqeltrrd	⊢ ( ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ) → ( 𝐹 ∘f · 𝐺 ) ∈ 𝑄 )