Theorem psr0cl

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

	Ref	Expression
Hypotheses	psrgrp.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrgrp.i	$$⊢\phi \to I\in V$$
	psrgrp.r	$$⊢\phi \to R\in \mathrm{Grp}$$
	psr0cl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psr0cl.o	$$⊢\underset{\dot{}}{0}=0_R$$
	psr0cl.b	$$⊢B={\mathrm{Base}}_S$$
Assertion	psr0cl	$$⊢\phi \to D\times \left\{\underset{\dot{}}{0}\right\}\in B$$

Proof

Step	Hyp	Ref	Expression
1		psrgrp.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrgrp.i	$$⊢\phi \to I\in V$$
3		psrgrp.r	$$⊢\phi \to R\in \mathrm{Grp}$$
4		psr0cl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		psr0cl.o	$$⊢\underset{\dot{}}{0}=0_R$$
6		psr0cl.b	$$⊢B={\mathrm{Base}}_S$$
7		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8	7 5	grpidcl	$$⊢R\in \mathrm{Grp}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
9		fconst6g	$$⊢\underset{\dot{}}{0}\in {\mathrm{Base}}_R\to \left(D\times \left\{\underset{\dot{}}{0}\right\}\right):D⟶{\mathrm{Base}}_R$$
10	3 8 9	3syl	$$⊢\phi \to \left(D\times \left\{\underset{\dot{}}{0}\right\}\right):D⟶{\mathrm{Base}}_R$$
11		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
12		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
13	4 12	rabex2	$$⊢D\in \mathrm{V}$$
14	11 13	elmap	$$⊢D\times \left\{\underset{\dot{}}{0}\right\}\in \left({{\mathrm{Base}}_R}^D\right)\leftrightarrow \left(D\times \left\{\underset{\dot{}}{0}\right\}\right):D⟶{\mathrm{Base}}_R$$
15	10 14	sylibr	$$⊢\phi \to D\times \left\{\underset{\dot{}}{0}\right\}\in \left({{\mathrm{Base}}_R}^D\right)$$
16	1 7 4 6 2	psrbas	$$⊢\phi \to B={{\mathrm{Base}}_R}^D$$
17	15 16	eleqtrrd	$$⊢\phi \to D\times \left\{\underset{\dot{}}{0}\right\}\in B$$