Theorem psr0lid

Description: The zero element of the ring of power series is a left identity. (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$$
	psr0lid.p	$$⊢\underset{\dot{}}{+}={+}_S$$
	psr0lid.x	$$⊢\phi \to X\in B$$
Assertion	psr0lid	$$⊢\phi \to \left(D\times \left\{\underset{\dot{}}{0}\right\}\right)\underset{\dot{}}{+}X=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		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		psr0lid.p	$$⊢\underset{\dot{}}{+}={+}_S$$
8		psr0lid.x	$$⊢\phi \to X\in B$$
9		eqid	$$⊢{+}_R={+}_R$$
10	1 2 3 4 5 6	psr0cl	$$⊢\phi \to D\times \left\{\underset{\dot{}}{0}\right\}\in B$$
11	1 6 9 7 10 8	psradd	$$⊢\phi \to \left(D\times \left\{\underset{\dot{}}{0}\right\}\right)\underset{\dot{}}{+}X=\left(D\times \left\{\underset{\dot{}}{0}\right\}\right){{+}_R}_{f}X$$
12		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
13	4 12	rabex2	$$⊢D\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to D\in \mathrm{V}$$
15		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
16	1 15 4 6 8	psrelbas	$$⊢\phi \to X:D⟶{\mathrm{Base}}_R$$
17	5	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
18	17	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
19	15 9 5	grplid	$$⊢\left(R\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{0}{+}_{R}x=x$$
20	3 19	sylan	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{0}{+}_{R}x=x$$
21	14 16 18 20	caofid0l	$$⊢\phi \to \left(D\times \left\{\underset{\dot{}}{0}\right\}\right){{+}_R}_{f}X=X$$
22	11 21	eqtrd	$$⊢\phi \to \left(D\times \left\{\underset{\dot{}}{0}\right\}\right)\underset{\dot{}}{+}X=X$$