Theorem psr1cl

Description: The identity element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014)

	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}$$
	psr1cl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psr1cl.z	$$⊢\underset{\dot{}}{0}=0_R$$
	psr1cl.o	$$⊢\underset{\dot{}}{1}=1_R$$
	psr1cl.u	$$⊢U=\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
	psr1cl.b	$$⊢B={\mathrm{Base}}_S$$
Assertion	psr1cl	$$⊢\phi \to U\in B$$

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		psr1cl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		psr1cl.z	$$⊢\underset{\dot{}}{0}=0_R$$
6		psr1cl.o	$$⊢\underset{\dot{}}{1}=1_R$$
7		psr1cl.u	$$⊢U=\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
8		psr1cl.b	$$⊢B={\mathrm{Base}}_S$$
9		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
10	9 6	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
11	9 5	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
12	10 11	ifcld	$$⊢R\in \mathrm{Ring}\to if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
13	3 12	syl	$$⊢\phi \to if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
14	13	adantr	$$⊢\left(\phi \wedge x\in D\right)\to if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
15	14 7	fmptd	$$⊢\phi \to U:D⟶{\mathrm{Base}}_R$$
16		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
17		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
18	4 17	rabex2	$$⊢D\in \mathrm{V}$$
19	16 18	elmap	$$⊢U\in \left({{\mathrm{Base}}_R}^D\right)\leftrightarrow U:D⟶{\mathrm{Base}}_R$$
20	15 19	sylibr	$$⊢\phi \to U\in \left({{\mathrm{Base}}_R}^D\right)$$
21	1 9 4 8 2	psrbas	$$⊢\phi \to B={{\mathrm{Base}}_R}^D$$
22	20 21	eleqtrrd	$$⊢\phi \to U\in B$$