This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mpff

Description: Polynomial functions are functions. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypotheses mpfsubrg.q ⊢ 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
mpff.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion mpff ( 𝐹 ∈ 𝑄 → 𝐹 : ( 𝐵 ↑m 𝐼 ) ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 mpfsubrg.q ⊢ 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 mpff.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 2 eqcomi ⊢ ( Base ‘ 𝑆 ) = 𝐵
4 3 oveq1i ⊢ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) = ( 𝐵 ↑m 𝐼 )
5 4 oveq2i ⊢ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
6 eqid ⊢ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) )
7 1 mpfrcl ⊢ ( 𝐹 ∈ 𝑄 → ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) )
8 7 simp2d ⊢ ( 𝐹 ∈ 𝑄 → 𝑆 ∈ CRing )
9 ovexd ⊢ ( 𝐹 ∈ 𝑄 → ( 𝐵 ↑m 𝐼 ) ∈ V )
10 1 mpfsubrg ⊢ ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( SubRing ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
11 6 subrgss ⊢ ( 𝑄 ∈ ( SubRing ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) → 𝑄 ⊆ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
12 7 10 11 3syl ⊢ ( 𝐹 ∈ 𝑄 → 𝑄 ⊆ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
13 id ⊢ ( 𝐹 ∈ 𝑄 → 𝐹 ∈ 𝑄 )
14 12 13 sseldd ⊢ ( 𝐹 ∈ 𝑄 → 𝐹 ∈ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
15 5 2 6 8 9 14 pwselbas ⊢ ( 𝐹 ∈ 𝑄 → 𝐹 : ( 𝐵 ↑m 𝐼 ) ⟶ 𝐵 )