Metamath Proof Explorer


Theorem mpfaddcl

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

Ref Expression
Hypotheses mpfsubrg.q 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
mpfaddcl.p + = ( +g𝑆 )
Assertion mpfaddcl ( ( 𝐹𝑄𝐺𝑄 ) → ( 𝐹f + 𝐺 ) ∈ 𝑄 )

Proof

Step Hyp Ref Expression
1 mpfsubrg.q 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 mpfaddcl.p + = ( +g𝑆 )
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 ( +g ‘ ( 𝑆s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) = ( +g ‘ ( 𝑆s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) )
18 3 4 7 8 14 16 2 17 pwsplusgval ( ( 𝐹𝑄𝐺𝑄 ) → ( 𝐹 ( +g ‘ ( 𝑆s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) 𝐺 ) = ( 𝐹f + 𝐺 ) )
19 17 subrgacl ( ( 𝑄 ∈ ( SubRing ‘ ( 𝑆s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ∧ 𝐹𝑄𝐺𝑄 ) → ( 𝐹 ( +g ‘ ( 𝑆s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) 𝐺 ) ∈ 𝑄 )
20 19 3expib ( 𝑄 ∈ ( SubRing ‘ ( 𝑆s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) → ( ( 𝐹𝑄𝐺𝑄 ) → ( 𝐹 ( +g ‘ ( 𝑆s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) 𝐺 ) ∈ 𝑄 ) )
21 10 20 mpcom ( ( 𝐹𝑄𝐺𝑄 ) → ( 𝐹 ( +g ‘ ( 𝑆s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) 𝐺 ) ∈ 𝑄 )
22 18 21 eqeltrrd ( ( 𝐹𝑄𝐺𝑄 ) → ( 𝐹f + 𝐺 ) ∈ 𝑄 )