psr0cl

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		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		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	7 5	grpidcl	$⊢ R \in Grp \to \underset{˙}{0} \in {Base}_{R}$
9		fconst6g	$⊢ \underset{˙}{0} \in {Base}_{R} \to (D \times \{\underset{˙}{0}\}) : D ⟶ {Base}_{R}$
10	3 8 9	3syl	$⊢ φ \to (D \times \{\underset{˙}{0}\}) : D ⟶ {Base}_{R}$
11		fvex	$⊢ {Base}_{R} \in V$
12		ovex	$⊢ {ℕ_{0}}^{I} \in V$
13	4 12	rabex2	$⊢ D \in V$
14	11 13	elmap	$⊢ D \times \{\underset{˙}{0}\} \in ({Base}_{R}^{D}) \leftrightarrow (D \times \{\underset{˙}{0}\}) : D ⟶ {Base}_{R}$
15	10 14	sylibr	$⊢ φ \to D \times \{\underset{˙}{0}\} \in ({Base}_{R}^{D})$
16	1 7 4 6 2	psrbas	$⊢ φ \to B = {Base}_{R}^{D}$
17	15 16	eleqtrrd	$⊢ φ \to D \times \{\underset{˙}{0}\} \in B$

Metamath Proof Explorer