Theorem psrneg

Description: The negative function 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}$$
	psrneg.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psrneg.i	$$⊢N={inv}_g\left(R\right)$$
	psrneg.b	$$⊢B={\mathrm{Base}}_S$$
	psrneg.m	$$⊢M={inv}_g\left(S\right)$$
	psrneg.x	$$⊢\phi \to X\in B$$
Assertion	psrneg	$$⊢\phi \to M\left(X\right)=N\circ X$$

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		psrneg.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		psrneg.i	$$⊢N={inv}_g\left(R\right)$$
6		psrneg.b	$$⊢B={\mathrm{Base}}_S$$
7		psrneg.m	$$⊢M={inv}_g\left(S\right)$$
8		psrneg.x	$$⊢\phi \to X\in B$$
9		eqid	$$⊢0_R=0_R$$
10		eqid	$$⊢{+}_S={+}_S$$
11	1 2 3 4 5 6 8 9 10	psrlinv	$$⊢\phi \to \left(N\circ X\right){+}_{S}X=D\times \left\{0_R\right\}$$
12		eqid	$$⊢0_S=0_S$$
13	1 2 3 4 9 12	psr0	$$⊢\phi \to 0_S=D\times \left\{0_R\right\}$$
14	11 13	eqtr4d	$$⊢\phi \to \left(N\circ X\right){+}_{S}X=0_S$$
15	1 2 3	psrgrp	$$⊢\phi \to S\in \mathrm{Grp}$$
16	1 2 3 4 5 6 8	psrnegcl	$$⊢\phi \to N\circ X\in B$$
17	6 10 12 7	grpinvid2	$$⊢\left(S\in \mathrm{Grp}\wedge X\in B\wedge N\circ X\in B\right)\to \left(M\left(X\right)=N\circ X\leftrightarrow \left(N\circ X\right){+}_{S}X=0_S\right)$$
18	15 8 16 17	syl3anc	$$⊢\phi \to \left(M\left(X\right)=N\circ X\leftrightarrow \left(N\circ X\right){+}_{S}X=0_S\right)$$
19	14 18	mpbird	$$⊢\phi \to M\left(X\right)=N\circ X$$