psrgrp

Description: The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014) (Proof shortened by SN, 7-Feb-2025)

	Ref	Expression
Hypotheses	psrgrp.s	$⊢ S = I mPwSer R$
	psrgrp.i	$⊢ φ \to I \in V$
	psrgrp.r	$⊢ φ \to R \in Grp$
Assertion	psrgrp	$⊢ φ \to S \in Grp$

Proof

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		ovex	$⊢ {ℕ_{0}}^{I} \in V$
5	4	rabex	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
6		eqid	$⊢ R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
7	6	pwsgrp	$⊢ (R \in Grp \land \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V) \to R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in Grp$
8	3 5 7	sylancl	$⊢ φ \to R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in Grp$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10	6 9	pwsbas	$⊢ (R \in Grp \land \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V) \to {Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}} = {Base}_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})}$
11	3 5 10	sylancl	$⊢ φ \to {Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}} = {Base}_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})}$
12		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
13		eqid	$⊢ {Base}_{S} = {Base}_{S}$
14	1 9 12 13 2	psrbas	$⊢ φ \to {Base}_{S} = {Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}$
15	14	eqcomd	$⊢ φ \to {Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}} = {Base}_{S}$
16		eqid	$⊢ {Base}_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})} = {Base}_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})}$
17	3	adantr	$⊢ (φ \land (x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}) \land y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}))) \to R \in Grp$
18	5	a1i	$⊢ (φ \land (x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}) \land y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}))) \to \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
19	11	eleq2d	$⊢ φ \to (x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}) \leftrightarrow x \in {Base}_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})})$
20	19	biimpa	$⊢ (φ \land x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}})) \to x \in {Base}_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})}$
21	20	adantrr	$⊢ (φ \land (x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}) \land y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}))) \to x \in {Base}_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})}$
22	11	eleq2d	$⊢ φ \to (y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}) \leftrightarrow y \in {Base}_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})})$
23	22	biimpa	$⊢ (φ \land y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}})) \to y \in {Base}_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})}$
24	23	adantrl	$⊢ (φ \land (x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}) \land y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}))) \to y \in {Base}_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})}$
25		eqid	$⊢ +_{R} = +_{R}$
26		eqid	$⊢ +_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})} = +_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})}$
27	6 16 17 18 21 24 25 26	pwsplusgval	$⊢ (φ \land (x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}) \land y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}))) \to x +_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})} y = x {+_{R}}_{f} y$
28		eqid	$⊢ +_{S} = +_{S}$
29	14	eleq2d	$⊢ φ \to (x \in {Base}_{S} \leftrightarrow x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}))$
30	29	biimpar	$⊢ (φ \land x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}})) \to x \in {Base}_{S}$
31	30	adantrr	$⊢ (φ \land (x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}) \land y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}))) \to x \in {Base}_{S}$
32	14	eleq2d	$⊢ φ \to (y \in {Base}_{S} \leftrightarrow y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}))$
33	32	biimpar	$⊢ (φ \land y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}})) \to y \in {Base}_{S}$
34	33	adantrl	$⊢ (φ \land (x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}) \land y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}))) \to y \in {Base}_{S}$
35	1 13 25 28 31 34	psradd	$⊢ (φ \land (x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}) \land y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}))) \to x +_{S} y = x {+_{R}}_{f} y$
36	27 35	eqtr4d	$⊢ (φ \land (x \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}) \land y \in ({Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}))) \to x +_{(R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\})} y = x +_{S} y$
37	11 15 36	grppropd	$⊢ φ \to (R ↑_{𝑠} \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in Grp \leftrightarrow S \in Grp)$
38	8 37	mpbid	$⊢ φ \to S \in Grp$

Metamath Proof Explorer

Theorem psrgrp

Proof