psr1cl

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

	Ref	Expression
Hypotheses	psrring.s	$⊢ S = I mPwSer R$
	psrring.i	$⊢ φ \to I \in V$
	psrring.r	$⊢ φ \to R \in Ring$
	psr1cl.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psr1cl.z	$⊢ \underset{˙}{0} = 0_{R}$
	psr1cl.o	$⊢ \underset{˙}{1} = 1_{R}$
	psr1cl.u	$⊢ U = (x \in D ⟼ if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}))$
	psr1cl.b	$⊢ B = {Base}_{S}$
Assertion	psr1cl	$⊢ φ \to U \in B$

Step	Hyp	Ref	Expression
1		psrring.s	$⊢ S = I mPwSer R$
2		psrring.i	$⊢ φ \to I \in V$
3		psrring.r	$⊢ φ \to R \in Ring$
4		psr1cl.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
5		psr1cl.z	$⊢ \underset{˙}{0} = 0_{R}$
6		psr1cl.o	$⊢ \underset{˙}{1} = 1_{R}$
7		psr1cl.u	$⊢ U = (x \in D ⟼ if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}))$
8		psr1cl.b	$⊢ B = {Base}_{S}$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10	9 6	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in {Base}_{R}$
11	9 5	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in {Base}_{R}$
12	10 11	ifcld	$⊢ R \in Ring \to if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) \in {Base}_{R}$
13	3 12	syl	$⊢ φ \to if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) \in {Base}_{R}$
14	13	adantr	$⊢ (φ \land x \in D) \to if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}) \in {Base}_{R}$
15	14 7	fmptd	$⊢ φ \to U : D ⟶ {Base}_{R}$
16		fvex	$⊢ {Base}_{R} \in V$
17		ovex	$⊢ {ℕ_{0}}^{I} \in V$
18	4 17	rabex2	$⊢ D \in V$
19	16 18	elmap	$⊢ U \in ({Base}_{R}^{D}) \leftrightarrow U : D ⟶ {Base}_{R}$
20	15 19	sylibr	$⊢ φ \to U \in ({Base}_{R}^{D})$
21	1 9 4 8 2	psrbas	$⊢ φ \to B = {Base}_{R}^{D}$
22	20 21	eleqtrrd	$⊢ φ \to U \in B$

Metamath Proof Explorer