Theorem psr1

Description: The identity element of the ring of power series. (Contributed by Mario Carneiro, 8-Jan-2015)

	Ref	Expression
Hypotheses	psrring.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrring.i	$$⊢\phi \to I\in V$$
	psrring.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	psr1.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psr1.z	$$⊢\underset{\dot{}}{0}=0_R$$
	psr1.o	$$⊢\underset{\dot{}}{1}=1_R$$
	psr1.u	$$⊢U=1_S$$
Assertion	psr1	$$⊢\phi \to U=\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		psrring.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrring.i	$$⊢\phi \to I\in V$$
3		psrring.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4		psr1.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		psr1.z	$$⊢\underset{\dot{}}{0}=0_R$$
6		psr1.o	$$⊢\underset{\dot{}}{1}=1_R$$
7		psr1.u	$$⊢U=1_S$$
8		eqid	$$⊢\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
9		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
10	1 2 3 4 5 6 8 9	psr1cl	$$⊢\phi \to \left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_S$$
11	2	adantr	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_S\right)\to I\in V$$
12	3	adantr	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_S\right)\to R\in \mathrm{Ring}$$
13		eqid	$$⊢{\cdot }_S={\cdot }_S$$
14		simpr	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_S\right)\to y\in {\mathrm{Base}}_S$$
15	1 11 12 4 5 6 8 9 13 14	psrlidm	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_S\right)\to \left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_{S}y=y$$
16	1 11 12 4 5 6 8 9 13 14	psrridm	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_S\right)\to y{\cdot }_S\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=y$$
17	15 16	jca	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_S\right)\to \left(\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_{S}y=y\wedge y{\cdot }_S\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=y\right)$$
18	17	ralrimiva	$$⊢\phi \to \forall y\in {\mathrm{Base}}_S\left(\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_{S}y=y\wedge y{\cdot }_S\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=y\right)$$
19	1 2 3	psrring	$$⊢\phi \to S\in \mathrm{Ring}$$
20	9 13 7	isringid	$$⊢S\in \mathrm{Ring}\to \left(\left(\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_S\wedge \forall y\in {\mathrm{Base}}_S\left(\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_{S}y=y\wedge y{\cdot }_S\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=y\right)\right)\leftrightarrow U=\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
21	19 20	syl	$$⊢\phi \to \left(\left(\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_S\wedge \forall y\in {\mathrm{Base}}_S\left(\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_{S}y=y\wedge y{\cdot }_S\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=y\right)\right)\leftrightarrow U=\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
22	10 18 21	mpbi2and	$$⊢\phi \to U=\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$