Theorem psr0

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}$$
	psr0.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psr0.o	$$⊢O=0_R$$
	psr0.z	$$⊢\underset{\dot{}}{0}=0_S$$
Assertion	psr0	$$⊢\phi \to \underset{\dot{}}{0}=D\times \left\{O\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		psr0.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		psr0.o	$$⊢O=0_R$$
6		psr0.z	$$⊢\underset{\dot{}}{0}=0_S$$
7		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
8		eqid	$$⊢{+}_S={+}_S$$
9	1 2 3 4 5 7	psr0cl	$$⊢\phi \to D\times \left\{O\right\}\in {\mathrm{Base}}_S$$
10	1 2 3 4 5 7 8 9	psr0lid	$$⊢\phi \to \left(D\times \left\{O\right\}\right){+}_S\left(D\times \left\{O\right\}\right)=D\times \left\{O\right\}$$
11	1 2 3	psrgrp	$$⊢\phi \to S\in \mathrm{Grp}$$
12	7 8 6	grpid	$$⊢\left(S\in \mathrm{Grp}\wedge D\times \left\{O\right\}\in {\mathrm{Base}}_S\right)\to \left(\left(D\times \left\{O\right\}\right){+}_S\left(D\times \left\{O\right\}\right)=D\times \left\{O\right\}\leftrightarrow \underset{\dot{}}{0}=D\times \left\{O\right\}\right)$$
13	11 9 12	syl2anc	$$⊢\phi \to \left(\left(D\times \left\{O\right\}\right){+}_S\left(D\times \left\{O\right\}\right)=D\times \left\{O\right\}\leftrightarrow \underset{\dot{}}{0}=D\times \left\{O\right\}\right)$$
14	10 13	mpbid	$$⊢\phi \to \underset{\dot{}}{0}=D\times \left\{O\right\}$$