Theorem psrlinv

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$$
	psrlinv.o	$$⊢\underset{\dot{}}{0}=0_R$$
	psrlinv.p	$$⊢\underset{\dot{}}{+}={+}_S$$
Assertion	psrlinv	$$⊢\phi \to \left(N\circ X\right)\underset{\dot{}}{+}X=D\times \left\{\underset{\dot{}}{0}\right\}$$

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		psrlinv.o	$$⊢\underset{\dot{}}{0}=0_R$$
9		psrlinv.p	$$⊢\underset{\dot{}}{+}={+}_S$$
10		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
11	4 10	rabex2	$$⊢D\in \mathrm{V}$$
12	11	a1i	$$⊢\phi \to D\in \mathrm{V}$$
13		fvexd	$$⊢\left(\phi \wedge x\in D\right)\to N\left(X\left(x\right)\right)\in \mathrm{V}$$
14		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
15	1 14 4 6 7	psrelbas	$$⊢\phi \to X:D⟶{\mathrm{Base}}_R$$
16	15	ffvelrnda	$$⊢\left(\phi \wedge x\in D\right)\to X\left(x\right)\in {\mathrm{Base}}_R$$
17	15	feqmptd	$$⊢\phi \to X=\left(x\in D⟼X\left(x\right)\right)$$
18	14 5 3	grpinvf1o	$$⊢\phi \to N:{\mathrm{Base}}_R\underset{1-1\; onto}{⟶}{\mathrm{Base}}_R$$
19		f1of	$$⊢N:{\mathrm{Base}}_R\underset{1-1\; onto}{⟶}{\mathrm{Base}}_R\to N:{\mathrm{Base}}_R⟶{\mathrm{Base}}_R$$
20	18 19	syl	$$⊢\phi \to N:{\mathrm{Base}}_R⟶{\mathrm{Base}}_R$$
21	20	feqmptd	$$⊢\phi \to N=\left(y\in {\mathrm{Base}}_R⟼N\left(y\right)\right)$$
22		fveq2	$$⊢y=X\left(x\right)\to N\left(y\right)=N\left(X\left(x\right)\right)$$
23	16 17 21 22	fmptco	$$⊢\phi \to N\circ X=\left(x\in D⟼N\left(X\left(x\right)\right)\right)$$
24	12 13 16 23 17	offval2	$$⊢\phi \to \left(N\circ X\right){{+}_R}_{f}X=\left(x\in D⟼N\left(X\left(x\right)\right){+}_{R}X\left(x\right)\right)$$
25		eqid	$$⊢{+}_R={+}_R$$
26	1 2 3 4 5 6 7	psrnegcl	$$⊢\phi \to N\circ X\in B$$
27	1 6 25 9 26 7	psradd	$$⊢\phi \to \left(N\circ X\right)\underset{\dot{}}{+}X=\left(N\circ X\right){{+}_R}_{f}X$$
28		fconstmpt	$$⊢D\times \left\{\underset{\dot{}}{0}\right\}=\left(x\in D⟼\underset{\dot{}}{0}\right)$$
29	14 25 8 5	grplinv	$$⊢\left(R\in \mathrm{Grp}\wedge X\left(x\right)\in {\mathrm{Base}}_R\right)\to N\left(X\left(x\right)\right){+}_{R}X\left(x\right)=\underset{\dot{}}{0}$$
30	3 16 29	syl2an2r	$$⊢\left(\phi \wedge x\in D\right)\to N\left(X\left(x\right)\right){+}_{R}X\left(x\right)=\underset{\dot{}}{0}$$
31	30	mpteq2dva	$$⊢\phi \to \left(x\in D⟼N\left(X\left(x\right)\right){+}_{R}X\left(x\right)\right)=\left(x\in D⟼\underset{\dot{}}{0}\right)$$
32	28 31	eqtr4id	$$⊢\phi \to D\times \left\{\underset{\dot{}}{0}\right\}=\left(x\in D⟼N\left(X\left(x\right)\right){+}_{R}X\left(x\right)\right)$$
33	24 27 32	3eqtr4d	$$⊢\phi \to \left(N\circ X\right)\underset{\dot{}}{+}X=D\times \left\{\underset{\dot{}}{0}\right\}$$