Metamath Proof Explorer

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 · 𝐺 ) ∈ 𝑄 )