mpff

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

Step	Hyp	Ref	Expression
1		mpfsubrg.q	$⊢ Q = ran (I evalSub S) (R)$
2		mpff.b	$⊢ B = {Base}_{S}$
3	2	eqcomi	$⊢ {Base}_{S} = B$
4	3	oveq1i	$⊢ {Base}_{S}^{I} = B^{I}$
5	4	oveq2i	$⊢ S ↑_{𝑠} ({Base}_{S}^{I}) = S ↑_{𝑠} (B^{I})$
6		eqid	$⊢ {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))} = {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))}$
7	1	mpfrcl	$⊢ F \in Q \to (I \in V \land S \in CRing \land R \in SubRing (S))$
8	7	simp2d	$⊢ F \in Q \to S \in CRing$
9		ovexd	$⊢ F \in Q \to B^{I} \in V$
10	1	mpfsubrg	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to Q \in SubRing (S ↑_{𝑠} ({Base}_{S}^{I}))$
11	6	subrgss	$⊢ Q \in SubRing (S ↑_{𝑠} ({Base}_{S}^{I})) \to Q \subseteq {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))}$
12	7 10 11	3syl	$⊢ F \in Q \to Q \subseteq {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))}$
13		id	$⊢ F \in Q \to F \in Q$
14	12 13	sseldd	$⊢ F \in Q \to F \in {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))}$
15	5 2 6 8 9 14	pwselbas	$⊢ F \in Q \to F : B^{I} ⟶ B$

Metamath Proof Explorer