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 𝐼 ) ⟶ 𝐵 )