mpfconst

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

	Ref	Expression
Hypotheses	mpfconst.b	$⊢ B = {Base}_{S}$
	mpfconst.q	$⊢ Q = ran (I evalSub S) (R)$
	mpfconst.i	$⊢ φ \to I \in V$
	mpfconst.s	$⊢ φ \to S \in CRing$
	mpfconst.r	$⊢ φ \to R \in SubRing (S)$
	mpfconst.x	$⊢ φ \to X \in R$
Assertion	mpfconst	$⊢ φ \to (B^{I}) \times \{X\} \in Q$

Proof

Step	Hyp	Ref	Expression
1		mpfconst.b	$⊢ B = {Base}_{S}$
2		mpfconst.q	$⊢ Q = ran (I evalSub S) (R)$
3		mpfconst.i	$⊢ φ \to I \in V$
4		mpfconst.s	$⊢ φ \to S \in CRing$
5		mpfconst.r	$⊢ φ \to R \in SubRing (S)$
6		mpfconst.x	$⊢ φ \to X \in R$
7		eqid	$⊢ (I evalSub S) (R) = (I evalSub S) (R)$
8		eqid	$⊢ I mPoly (S ↾_{𝑠} R) = I mPoly (S ↾_{𝑠} R)$
9		eqid	$⊢ S ↾_{𝑠} R = S ↾_{𝑠} R$
10		eqid	$⊢ algSc (I mPoly (S ↾_{𝑠} R)) = algSc (I mPoly (S ↾_{𝑠} R))$
11	7 8 9 1 10 3 4 5 6	evlssca	$⊢ φ \to (I evalSub S) (R) (algSc (I mPoly (S ↾_{𝑠} R)) (X)) = (B^{I}) \times \{X\}$
12		eqid	$⊢ S ↑_{𝑠} (B^{I}) = S ↑_{𝑠} (B^{I})$
13	7 8 9 12 1	evlsrhm	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to (I evalSub S) (R) \in ((I mPoly (S ↾_{𝑠} R)) RingHom (S ↑_{𝑠} (B^{I})))$
14	3 4 5 13	syl3anc	$⊢ φ \to (I evalSub S) (R) \in ((I mPoly (S ↾_{𝑠} R)) RingHom (S ↑_{𝑠} (B^{I})))$
15		eqid	$⊢ {Base}_{(I mPoly (S ↾_{𝑠} R))} = {Base}_{(I mPoly (S ↾_{𝑠} R))}$
16		eqid	$⊢ {Base}_{(S ↑_{𝑠} (B^{I}))} = {Base}_{(S ↑_{𝑠} (B^{I}))}$
17	15 16	rhmf	$⊢ (I evalSub S) (R) \in ((I mPoly (S ↾_{𝑠} R)) RingHom (S ↑_{𝑠} (B^{I}))) \to (I evalSub S) (R) : {Base}_{(I mPoly (S ↾_{𝑠} R))} ⟶ {Base}_{(S ↑_{𝑠} (B^{I}))}$
18		ffn	$⊢ (I evalSub S) (R) : {Base}_{(I mPoly (S ↾_{𝑠} R))} ⟶ {Base}_{(S ↑_{𝑠} (B^{I}))} \to (I evalSub S) (R) Fn {Base}_{(I mPoly (S ↾_{𝑠} R))}$
19	14 17 18	3syl	$⊢ φ \to (I evalSub S) (R) Fn {Base}_{(I mPoly (S ↾_{𝑠} R))}$
20	9	subrgring	$⊢ R \in SubRing (S) \to S ↾_{𝑠} R \in Ring$
21	5 20	syl	$⊢ φ \to S ↾_{𝑠} R \in Ring$
22		eqid	$⊢ Scalar (I mPoly (S ↾_{𝑠} R)) = Scalar (I mPoly (S ↾_{𝑠} R))$
23	8	mplring	$⊢ (I \in V \land S ↾_{𝑠} R \in Ring) \to I mPoly (S ↾_{𝑠} R) \in Ring$
24	8	mpllmod	$⊢ (I \in V \land S ↾_{𝑠} R \in Ring) \to I mPoly (S ↾_{𝑠} R) \in LMod$
25		eqid	$⊢ {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))} = {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))}$
26	10 22 23 24 25 15	asclf	$⊢ (I \in V \land S ↾_{𝑠} R \in Ring) \to algSc (I mPoly (S ↾_{𝑠} R)) : {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))} ⟶ {Base}_{(I mPoly (S ↾_{𝑠} R))}$
27	3 21 26	syl2anc	$⊢ φ \to algSc (I mPoly (S ↾_{𝑠} R)) : {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))} ⟶ {Base}_{(I mPoly (S ↾_{𝑠} R))}$
28	1	subrgss	$⊢ R \in SubRing (S) \to R \subseteq B$
29	9 1	ressbas2	$⊢ R \subseteq B \to R = {Base}_{(S ↾_{𝑠} R)}$
30	5 28 29	3syl	$⊢ φ \to R = {Base}_{(S ↾_{𝑠} R)}$
31		ovexd	$⊢ φ \to S ↾_{𝑠} R \in V$
32	8 3 31	mplsca	$⊢ φ \to S ↾_{𝑠} R = Scalar (I mPoly (S ↾_{𝑠} R))$
33	32	fveq2d	$⊢ φ \to {Base}_{(S ↾_{𝑠} R)} = {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))}$
34	30 33	eqtrd	$⊢ φ \to R = {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))}$
35	6 34	eleqtrd	$⊢ φ \to X \in {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))}$
36	27 35	ffvelcdmd	$⊢ φ \to algSc (I mPoly (S ↾_{𝑠} R)) (X) \in {Base}_{(I mPoly (S ↾_{𝑠} R))}$
37		fnfvelrn	$⊢ ((I evalSub S) (R) Fn {Base}_{(I mPoly (S ↾_{𝑠} R))} \land algSc (I mPoly (S ↾_{𝑠} R)) (X) \in {Base}_{(I mPoly (S ↾_{𝑠} R))}) \to (I evalSub S) (R) (algSc (I mPoly (S ↾_{𝑠} R)) (X)) \in ran (I evalSub S) (R)$
38	19 36 37	syl2anc	$⊢ φ \to (I evalSub S) (R) (algSc (I mPoly (S ↾_{𝑠} R)) (X)) \in ran (I evalSub S) (R)$
39	11 38	eqeltrrd	$⊢ φ \to (B^{I}) \times \{X\} \in ran (I evalSub S) (R)$
40	39 2	eleqtrrdi	$⊢ φ \to (B^{I}) \times \{X\} \in Q$

Metamath Proof Explorer

Theorem mpfconst

Proof