Metamath Proof Explorer

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