psr0

Description: The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014)

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		psr0.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
5		psr0.o	$⊢ O = 0_{R}$
6		psr0.z	$⊢ \underset{˙}{0} = 0_{S}$
7		eqid	$⊢ {Base}_{S} = {Base}_{S}$
8		eqid	$⊢ +_{S} = +_{S}$
9	1 2 3 4 5 7	psr0cl	$⊢ φ \to D \times \{O\} \in {Base}_{S}$
10	1 2 3 4 5 7 8 9	psr0lid	$⊢ φ \to (D \times \{O\}) +_{S} (D \times \{O\}) = D \times \{O\}$
11	1 2 3	psrgrp	$⊢ φ \to S \in Grp$
12	7 8 6	grpid	$⊢ (S \in Grp \land D \times \{O\} \in {Base}_{S}) \to ((D \times \{O\}) +_{S} (D \times \{O\}) = D \times \{O\} \leftrightarrow \underset{˙}{0} = D \times \{O\})$
13	11 9 12	syl2anc	$⊢ φ \to ((D \times \{O\}) +_{S} (D \times \{O\}) = D \times \{O\} \leftrightarrow \underset{˙}{0} = D \times \{O\})$
14	10 13	mpbid	$⊢ φ \to \underset{˙}{0} = D \times \{O\}$

Metamath Proof Explorer