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