psrgrp

Description: The ring of power series is a group. (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$
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		eqidd	$⊢ φ \to {Base}_{S} = {Base}_{S}$
5		eqidd	$⊢ φ \to +_{S} = +_{S}$
6		eqid	$⊢ {Base}_{S} = {Base}_{S}$
7		eqid	$⊢ +_{S} = +_{S}$
8	3	3ad2ant1	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to R \in Grp$
9		simp2	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x \in {Base}_{S}$
10		simp3	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to y \in {Base}_{S}$
11	1 6 7 8 9 10	psraddcl	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x +_{S} y \in {Base}_{S}$
12		ovex	$⊢ {ℕ_{0}}^{I} \in V$
13	12	rabex	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
14	13	a1i	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
17		simpr1	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x \in {Base}_{S}$
18	1 15 16 6 17	psrelbas	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
19		simpr2	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to y \in {Base}_{S}$
20	1 15 16 6 19	psrelbas	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to y : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
21		simpr3	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to z \in {Base}_{S}$
22	1 15 16 6 21	psrelbas	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to z : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
23	3	adantr	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to R \in Grp$
24		eqid	$⊢ +_{R} = +_{R}$
25	15 24	grpass	$⊢ (R \in Grp \land (r \in {Base}_{R} \land s \in {Base}_{R} \land t \in {Base}_{R})) \to (r +_{R} s) +_{R} t = r +_{R} (s +_{R} t)$
26	23 25	sylan	$⊢ ((φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \land (r \in {Base}_{R} \land s \in {Base}_{R} \land t \in {Base}_{R})) \to (r +_{R} s) +_{R} t = r +_{R} (s +_{R} t)$
27	14 18 20 22 26	caofass	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (x {+_{R}}_{f} y) {+_{R}}_{f} z = x {+_{R}}_{f} (y {+_{R}}_{f} z)$
28	1 6 24 7 17 19	psradd	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x +_{S} y = x {+_{R}}_{f} y$
29	28	oveq1d	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (x +_{S} y) {+_{R}}_{f} z = (x {+_{R}}_{f} y) {+_{R}}_{f} z$
30	1 6 24 7 19 21	psradd	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to y +_{S} z = y {+_{R}}_{f} z$
31	30	oveq2d	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x {+_{R}}_{f} (y +_{S} z) = x {+_{R}}_{f} (y {+_{R}}_{f} z)$
32	27 29 31	3eqtr4d	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (x +_{S} y) {+_{R}}_{f} z = x {+_{R}}_{f} (y +_{S} z)$
33	11	3adant3r3	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x +_{S} y \in {Base}_{S}$
34	1 6 24 7 33 21	psradd	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (x +_{S} y) +_{S} z = (x +_{S} y) {+_{R}}_{f} z$
35	1 6 7 23 19 21	psraddcl	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to y +_{S} z \in {Base}_{S}$
36	1 6 24 7 17 35	psradd	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x +_{S} (y +_{S} z) = x {+_{R}}_{f} (y +_{S} z)$
37	32 34 36	3eqtr4d	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (x +_{S} y) +_{S} z = x +_{S} (y +_{S} z)$
38		eqid	$⊢ 0_{R} = 0_{R}$
39	1 2 3 16 38 6	psr0cl	$⊢ φ \to \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{0_{R}\} \in {Base}_{S}$
40	2	adantr	$⊢ (φ \land x \in {Base}_{S}) \to I \in V$
41	3	adantr	$⊢ (φ \land x \in {Base}_{S}) \to R \in Grp$
42		simpr	$⊢ (φ \land x \in {Base}_{S}) \to x \in {Base}_{S}$
43	1 40 41 16 38 6 7 42	psr0lid	$⊢ (φ \land x \in {Base}_{S}) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{0_{R}\}) +_{S} x = x$
44		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
45	1 40 41 16 44 6 42	psrnegcl	$⊢ (φ \land x \in {Base}_{S}) \to {inv}_{g} (R) \circ x \in {Base}_{S}$
46	1 40 41 16 44 6 42 38 7	psrlinv	$⊢ (φ \land x \in {Base}_{S}) \to ({inv}_{g} (R) \circ x) +_{S} x = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{0_{R}\}$
47	4 5 11 37 39 43 45 46	isgrpd	$⊢ φ \to S \in Grp$

Metamath Proof Explorer

Theorem psrgrp

Proof