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 mPwSer R$
	psrgrp.i	$⊢ φ \to I \in V$
	psrgrp.r	$⊢ φ \to R \in Grp$
	psr0cl.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psr0cl.o	$⊢ \underset{˙}{0} = 0_{R}$
	psr0cl.b	$⊢ B = {Base}_{S}$
	psr0lid.p	$⊢ \underset{˙}{+} = +_{S}$
	psr0lid.x	$⊢ φ \to X \in B$
Assertion	psr0lid	$⊢ φ \to (D \times \{\underset{˙}{0}\}) \underset{˙}{+} X = X$

Step	Hyp	Ref	Expression
1		psrgrp.s	$⊢ S = I mPwSer R$
2		psrgrp.i	$⊢ φ \to I \in V$
3		psrgrp.r	$⊢ φ \to R \in Grp$
4		psr0cl.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
5		psr0cl.o	$⊢ \underset{˙}{0} = 0_{R}$
6		psr0cl.b	$⊢ B = {Base}_{S}$
7		psr0lid.p	$⊢ \underset{˙}{+} = +_{S}$
8		psr0lid.x	$⊢ φ \to X \in B$
9		eqid	$⊢ +_{R} = +_{R}$
10	1 2 3 4 5 6	psr0cl	$⊢ φ \to D \times \{\underset{˙}{0}\} \in B$
11	1 6 9 7 10 8	psradd	$⊢ φ \to (D \times \{\underset{˙}{0}\}) \underset{˙}{+} X = (D \times \{\underset{˙}{0}\}) {+_{R}}_{f} X$
12		ovex	$⊢ {ℕ_{0}}^{I} \in V$
13	4 12	rabex2	$⊢ D \in V$
14	13	a1i	$⊢ φ \to D \in V$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16	1 15 4 6 8	psrelbas	$⊢ φ \to X : D ⟶ {Base}_{R}$
17	5	fvexi	$⊢ \underset{˙}{0} \in V$
18	17	a1i	$⊢ φ \to \underset{˙}{0} \in V$
19	15 9 5	grplid	$⊢ (R \in Grp \land x \in {Base}_{R}) \to \underset{˙}{0} +_{R} x = x$
20	3 19	sylan	$⊢ (φ \land x \in {Base}_{R}) \to \underset{˙}{0} +_{R} x = x$
21	14 16 18 20	caofid0l	$⊢ φ \to (D \times \{\underset{˙}{0}\}) {+_{R}}_{f} X = X$
22	11 21	eqtrd	$⊢ φ \to (D \times \{\underset{˙}{0}\}) \underset{˙}{+} X = X$

Metamath Proof Explorer