Theorem psrnegcl

Description: The negative function in 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}$$
	psrnegcl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psrnegcl.i	$$⊢N={inv}_g\left(R\right)$$
	psrnegcl.b	$$⊢B={\mathrm{Base}}_S$$
	psrnegcl.z	$$⊢\phi \to X\in B$$
Assertion	psrnegcl	$$⊢\phi \to N\circ X\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		psrnegcl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		psrnegcl.i	$$⊢N={inv}_g\left(R\right)$$
6		psrnegcl.b	$$⊢B={\mathrm{Base}}_S$$
7		psrnegcl.z	$$⊢\phi \to X\in B$$
8		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
9	8 5 3	grpinvf1o	$$⊢\phi \to N:{\mathrm{Base}}_R\underset{1-1\; onto}{⟶}{\mathrm{Base}}_R$$
10		f1of	$$⊢N:{\mathrm{Base}}_R\underset{1-1\; onto}{⟶}{\mathrm{Base}}_R\to N:{\mathrm{Base}}_R⟶{\mathrm{Base}}_R$$
11	9 10	syl	$$⊢\phi \to N:{\mathrm{Base}}_R⟶{\mathrm{Base}}_R$$
12	1 8 4 6 7	psrelbas	$$⊢\phi \to X:D⟶{\mathrm{Base}}_R$$
13		fco	$$⊢\left(N:{\mathrm{Base}}_R⟶{\mathrm{Base}}_R\wedge X:D⟶{\mathrm{Base}}_R\right)\to \left(N\circ X\right):D⟶{\mathrm{Base}}_R$$
14	11 12 13	syl2anc	$$⊢\phi \to \left(N\circ X\right):D⟶{\mathrm{Base}}_R$$
15		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
16		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
17	4 16	rabex2	$$⊢D\in \mathrm{V}$$
18	15 17	elmap	$$⊢N\circ X\in \left({{\mathrm{Base}}_R}^D\right)\leftrightarrow \left(N\circ X\right):D⟶{\mathrm{Base}}_R$$
19	14 18	sylibr	$$⊢\phi \to N\circ X\in \left({{\mathrm{Base}}_R}^D\right)$$
20	1 8 4 6 2	psrbas	$$⊢\phi \to B={{\mathrm{Base}}_R}^D$$
21	19 20	eleqtrrd	$$⊢\phi \to N\circ X\in B$$