psrgrpOLD

Description: Obsolete proof of psrgrp as of 7-Feb-2025. (Contributed by Mario Carneiro, 29-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	psrgrp.s	$⊢ S = I mPwSer R$
	psrgrp.i	$⊢ φ \to I \in V$
	psrgrp.r	$⊢ φ \to R \in Grp$
Assertion	psrgrpOLD	$⊢ φ \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	grpmgmd	$⊢ φ \to R \in Mgm$
9	8	3ad2ant1	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to R \in Mgm$
10		simp2	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x \in {Base}_{S}$
11		simp3	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to y \in {Base}_{S}$
12	1 6 7 9 10 11	psraddcl	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x +_{S} y \in {Base}_{S}$
13		ovex	$⊢ {ℕ_{0}}^{I} \in V$
14	13	rabex	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
15	14	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$
16		eqid	$⊢ {Base}_{R} = {Base}_{R}$
17		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
18		simpr1	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x \in {Base}_{S}$
19	1 16 17 6 18	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}$
20		simpr2	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to y \in {Base}_{S}$
21	1 16 17 6 20	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}$
22		simpr3	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to z \in {Base}_{S}$
23	1 16 17 6 22	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}$
24	3	adantr	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to R \in Grp$
25		eqid	$⊢ +_{R} = +_{R}$
26	16 25	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)$
27	24 26	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)$
28	15 19 21 23 27	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)$
29	1 6 25 7 18 20	psradd	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x +_{S} y = x {+_{R}}_{f} y$
30	29	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$
31	1 6 25 7 20 22	psradd	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to y +_{S} z = y {+_{R}}_{f} z$
32	31	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)$
33	28 30 32	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)$
34	12	3adant3r3	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x +_{S} y \in {Base}_{S}$
35	1 6 25 7 34 22	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$
36	8	adantr	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to R \in Mgm$
37	1 6 7 36 20 22	psraddcl	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to y +_{S} z \in {Base}_{S}$
38	1 6 25 7 18 37	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)$
39	33 35 38	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)$
40		eqid	$⊢ 0_{R} = 0_{R}$
41	1 2 3 17 40 6	psr0cl	$⊢ φ \to \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{0_{R}\} \in {Base}_{S}$
42	2	adantr	$⊢ (φ \land x \in {Base}_{S}) \to I \in V$
43	3	adantr	$⊢ (φ \land x \in {Base}_{S}) \to R \in Grp$
44		simpr	$⊢ (φ \land x \in {Base}_{S}) \to x \in {Base}_{S}$
45	1 42 43 17 40 6 7 44	psr0lid	$⊢ (φ \land x \in {Base}_{S}) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{0_{R}\}) +_{S} x = x$
46		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
47	1 42 43 17 46 6 44	psrnegcl	$⊢ (φ \land x \in {Base}_{S}) \to {inv}_{g} (R) \circ x \in {Base}_{S}$
48	1 42 43 17 46 6 44 40 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}\}$
49	4 5 12 39 41 45 47 48	isgrpd	$⊢ φ \to S \in Grp$

Metamath Proof Explorer

Theorem psrgrpOLD

Proof