evlssca

Description: Polynomial evaluation maps scalars to constant functions. (Contributed by Stefan O'Rear, 13-Mar-2015) (Proof shortened by AV, 18-Sep-2021)

	Ref	Expression
Hypotheses	evlssca.q	$⊢ Q = (I evalSub S) (R)$
	evlssca.w	$⊢ W = I mPoly U$
	evlssca.u	$⊢ U = S ↾_{𝑠} R$
	evlssca.b	$⊢ B = {Base}_{S}$
	evlssca.a	$⊢ A = algSc (W)$
	evlssca.i	$⊢ φ \to I \in V$
	evlssca.s	$⊢ φ \to S \in CRing$
	evlssca.r	$⊢ φ \to R \in SubRing (S)$
	evlssca.x	$⊢ φ \to X \in R$
Assertion	evlssca	$⊢ φ \to Q (A (X)) = (B^{I}) \times \{X\}$

Proof

Step	Hyp	Ref	Expression
1		evlssca.q	$⊢ Q = (I evalSub S) (R)$
2		evlssca.w	$⊢ W = I mPoly U$
3		evlssca.u	$⊢ U = S ↾_{𝑠} R$
4		evlssca.b	$⊢ B = {Base}_{S}$
5		evlssca.a	$⊢ A = algSc (W)$
6		evlssca.i	$⊢ φ \to I \in V$
7		evlssca.s	$⊢ φ \to S \in CRing$
8		evlssca.r	$⊢ φ \to R \in SubRing (S)$
9		evlssca.x	$⊢ φ \to X \in R$
10		eqid	$⊢ I mVar U = I mVar U$
11		eqid	$⊢ S ↑_{𝑠} (B^{I}) = S ↑_{𝑠} (B^{I})$
12		eqid	$⊢ (x \in R ⟼ (B^{I}) \times \{x\}) = (x \in R ⟼ (B^{I}) \times \{x\})$
13		eqid	$⊢ (x \in I ⟼ (y \in (B^{I}) ⟼ y (x))) = (x \in I ⟼ (y \in (B^{I}) ⟼ y (x)))$
14	1 2 10 3 11 4 5 12 13	evlsval2	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to (Q \in (W RingHom (S ↑_{𝑠} (B^{I}))) \land (Q \circ A = (x \in R ⟼ (B^{I}) \times \{x\}) \land Q \circ (I mVar U) = (x \in I ⟼ (y \in (B^{I}) ⟼ y (x)))))$
15	6 7 8 14	syl3anc	$⊢ φ \to (Q \in (W RingHom (S ↑_{𝑠} (B^{I}))) \land (Q \circ A = (x \in R ⟼ (B^{I}) \times \{x\}) \land Q \circ (I mVar U) = (x \in I ⟼ (y \in (B^{I}) ⟼ y (x)))))$
16	15	simprld	$⊢ φ \to Q \circ A = (x \in R ⟼ (B^{I}) \times \{x\})$
17	16	fveq1d	$⊢ φ \to (Q \circ A) (X) = (x \in R ⟼ (B^{I}) \times \{x\}) (X)$
18		eqid	$⊢ {Base}_{W} = {Base}_{W}$
19		eqid	$⊢ {Base}_{U} = {Base}_{U}$
20	3	subrgring	$⊢ R \in SubRing (S) \to U \in Ring$
21	8 20	syl	$⊢ φ \to U \in Ring$
22	2 18 19 5 6 21	mplasclf	$⊢ φ \to A : {Base}_{U} ⟶ {Base}_{W}$
23	4	subrgss	$⊢ R \in SubRing (S) \to R \subseteq B$
24	3 4	ressbas2	$⊢ R \subseteq B \to R = {Base}_{U}$
25	8 23 24	3syl	$⊢ φ \to R = {Base}_{U}$
26	25	feq2d	$⊢ φ \to (A : R ⟶ {Base}_{W} \leftrightarrow A : {Base}_{U} ⟶ {Base}_{W})$
27	22 26	mpbird	$⊢ φ \to A : R ⟶ {Base}_{W}$
28		fvco3	$⊢ (A : R ⟶ {Base}_{W} \land X \in R) \to (Q \circ A) (X) = Q (A (X))$
29	27 9 28	syl2anc	$⊢ φ \to (Q \circ A) (X) = Q (A (X))$
30		sneq	$⊢ x = X \to \{x\} = \{X\}$
31	30	xpeq2d	$⊢ x = X \to (B^{I}) \times \{x\} = (B^{I}) \times \{X\}$
32		ovex	$⊢ B^{I} \in V$
33		snex	$⊢ \{X\} \in V$
34	32 33	xpex	$⊢ (B^{I}) \times \{X\} \in V$
35	31 12 34	fvmpt	$⊢ X \in R \to (x \in R ⟼ (B^{I}) \times \{x\}) (X) = (B^{I}) \times \{X\}$
36	9 35	syl	$⊢ φ \to (x \in R ⟼ (B^{I}) \times \{x\}) (X) = (B^{I}) \times \{X\}$
37	17 29 36	3eqtr3d	$⊢ φ \to Q (A (X)) = (B^{I}) \times \{X\}$

Metamath Proof Explorer

Theorem evlssca

Proof