Theorem psrascl

Description: Value of the scalar injection into the power series algebra. (Contributed by SN, 18-May-2025)

	Ref	Expression
Hypotheses	psrascl.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrascl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psrascl.z	$$⊢\underset{\dot{}}{0}=0_R$$
	psrascl.k	$$⊢K={\mathrm{Base}}_R$$
	psrascl.a	$$⊢A=\mathrm{algSc}\left(S\right)$$
	psrascl.i	$$⊢\phi \to I\in V$$
	psrascl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	psrascl.x	$$⊢\phi \to X\in K$$
Assertion	psrascl	$$⊢\phi \to A\left(X\right)=\left(y\in D⟼if\left(y=I\times \left\{0\right\},X,\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		psrascl.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrascl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		psrascl.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		psrascl.k	$$⊢K={\mathrm{Base}}_R$$
5		psrascl.a	$$⊢A=\mathrm{algSc}\left(S\right)$$
6		psrascl.i	$$⊢\phi \to I\in V$$
7		psrascl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
8		psrascl.x	$$⊢\phi \to X\in K$$
9	1 6 7	psrsca	$$⊢\phi \to R=\mathrm{Scalar}\left(S\right)$$
10	9	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}$$
11	4 10	eqtrid	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}$$
12	8 11	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}$$
13		eqid	$$⊢\mathrm{Scalar}\left(S\right)=\mathrm{Scalar}\left(S\right)$$
14		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}$$
15		eqid	$$⊢{\cdot }_S={\cdot }_S$$
16		eqid	$$⊢1_S=1_S$$
17	5 13 14 15 16	asclval	$$⊢X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}\to A\left(X\right)=X{\cdot }_S{1}_S$$
18	12 17	syl	$$⊢\phi \to A\left(X\right)=X{\cdot }_S{1}_S$$
19		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
20		eqid	$$⊢{\cdot }_R={\cdot }_R$$
21	1 6 7	psrring	$$⊢\phi \to S\in \mathrm{Ring}$$
22	19 16	ringidcl	$$⊢S\in \mathrm{Ring}\to 1_S\in {\mathrm{Base}}_S$$
23	21 22	syl	$$⊢\phi \to 1_S\in {\mathrm{Base}}_S$$
24	1 15 4 19 20 2 8 23	psrvsca	$$⊢\phi \to X{\cdot }_S{1}_S=\left(D\times \left\{X\right\}\right){{\cdot }_R}_f{1}_S$$
25		fnconstg	$$⊢X\in K\to \left(D\times \left\{X\right\}\right)FnD$$
26	8 25	syl	$$⊢\phi \to \left(D\times \left\{X\right\}\right)FnD$$
27	1 4 2 19 23	psrelbas	$$⊢\phi \to 1_S:D⟶K$$
28	27	ffnd	$$⊢\phi \to 1_{S}FnD$$
29		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^I\in \mathrm{V}$$
30	2 29	rabexd	$$⊢\phi \to D\in \mathrm{V}$$
31		inidm	$$⊢D\cap D=D$$
32		fvconst2g	$$⊢\left(X\in K\wedge y\in D\right)\to \left(D\times \left\{X\right\}\right)\left(y\right)=X$$
33	8 32	sylan	$$⊢\left(\phi \wedge y\in D\right)\to \left(D\times \left\{X\right\}\right)\left(y\right)=X$$
34		eqid	$$⊢1_R=1_R$$
35	1 6 7 2 3 34 16	psr1	$$⊢\phi \to 1_S=\left(d\in D⟼if\left(d=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\right)$$
36	35	adantr	$$⊢\left(\phi \wedge y\in D\right)\to 1_S=\left(d\in D⟼if\left(d=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\right)$$
37	36	fveq1d	$$⊢\left(\phi \wedge y\in D\right)\to 1_S\left(y\right)=\left(d\in D⟼if\left(d=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\right)\left(y\right)$$
38		eqeq1	$$⊢d=y\to \left(d=I\times \left\{0\right\}\leftrightarrow y=I\times \left\{0\right\}\right)$$
39	38	ifbid	$$⊢d=y\to if\left(d=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)=if\left(y=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)$$
40		eqid	$$⊢\left(d\in D⟼if\left(d=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\right)=\left(d\in D⟼if\left(d=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\right)$$
41		fvex	$$⊢1_R\in \mathrm{V}$$
42	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
43	41 42	ifex	$$⊢if\left(y=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\in \mathrm{V}$$
44	39 40 43	fvmpt	$$⊢y\in D\to \left(d\in D⟼if\left(d=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\right)\left(y\right)=if\left(y=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)$$
45	44	adantl	$$⊢\left(\phi \wedge y\in D\right)\to \left(d\in D⟼if\left(d=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\right)\left(y\right)=if\left(y=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)$$
46	37 45	eqtrd	$$⊢\left(\phi \wedge y\in D\right)\to 1_S\left(y\right)=if\left(y=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)$$
47	26 28 30 30 31 33 46	offval	$$⊢\phi \to \left(D\times \left\{X\right\}\right){{\cdot }_R}_f{1}_S=\left(y\in D⟼X{\cdot }_{R}if\left(y=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\right)$$
48		ovif2	$$⊢X{\cdot }_{R}if\left(y=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)=if\left(y=I\times \left\{0\right\},X{\cdot }_R{1}_R,X{\cdot }_R\underset{\dot{}}{0}\right)$$
49	4 20 34 7 8	ringridmd	$$⊢\phi \to X{\cdot }_R{1}_R=X$$
50	4 20 3 7 8	ringrzd	$$⊢\phi \to X{\cdot }_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
51	49 50	ifeq12d	$$⊢\phi \to if\left(y=I\times \left\{0\right\},X{\cdot }_R{1}_R,X{\cdot }_R\underset{\dot{}}{0}\right)=if\left(y=I\times \left\{0\right\},X,\underset{\dot{}}{0}\right)$$
52	48 51	eqtrid	$$⊢\phi \to X{\cdot }_{R}if\left(y=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)=if\left(y=I\times \left\{0\right\},X,\underset{\dot{}}{0}\right)$$
53	52	mpteq2dv	$$⊢\phi \to \left(y\in D⟼X{\cdot }_{R}if\left(y=I\times \left\{0\right\},1_R,\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=I\times \left\{0\right\},X,\underset{\dot{}}{0}\right)\right)$$
54	47 53	eqtrd	$$⊢\phi \to \left(D\times \left\{X\right\}\right){{\cdot }_R}_f{1}_S=\left(y\in D⟼if\left(y=I\times \left\{0\right\},X,\underset{\dot{}}{0}\right)\right)$$
55	18 24 54	3eqtrd	$$⊢\phi \to A\left(X\right)=\left(y\in D⟼if\left(y=I\times \left\{0\right\},X,\underset{\dot{}}{0}\right)\right)$$