psrlmod

Description: The ring of power series is a left module. (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$
Assertion	psrlmod	$⊢ φ \to S \in LMod$

Proof

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		eqidd	$⊢ φ \to {Base}_{S} = {Base}_{S}$
5		eqidd	$⊢ φ \to +_{S} = +_{S}$
6	1 2 3	psrsca	$⊢ φ \to R = Scalar (S)$
7		eqidd	$⊢ φ \to \cdot_{S} = \cdot_{S}$
8		eqidd	$⊢ φ \to {Base}_{R} = {Base}_{R}$
9		eqidd	$⊢ φ \to +_{R} = +_{R}$
10		eqidd	$⊢ φ \to \cdot_{R} = \cdot_{R}$
11		eqidd	$⊢ φ \to 1_{R} = 1_{R}$
12		ringgrp	$⊢ R \in Ring \to R \in Grp$
13	3 12	syl	$⊢ φ \to R \in Grp$
14	1 2 13	psrgrp	$⊢ φ \to S \in Grp$
15		eqid	$⊢ \cdot_{S} = \cdot_{S}$
16		eqid	$⊢ {Base}_{R} = {Base}_{R}$
17		eqid	$⊢ {Base}_{S} = {Base}_{S}$
18	3	3ad2ant1	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{S}) \to R \in Ring$
19		simp2	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{S}) \to x \in {Base}_{R}$
20		simp3	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{S}) \to y \in {Base}_{S}$
21	1 15 16 17 18 19 20	psrvscacl	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{S}) \to x \cdot_{S} y \in {Base}_{S}$
22		ovex	$⊢ {ℕ_{0}}^{I} \in V$
23	22	rabex	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
24	23	a1i	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
25		simpr1	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x \in {Base}_{R}$
26		fconst6g	$⊢ x \in {Base}_{R} \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
27	25 26	syl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
28		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
29		simpr2	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to y \in {Base}_{S}$
30	1 16 28 17 29	psrelbas	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to y : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
31		simpr3	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to z \in {Base}_{S}$
32	1 16 28 17 31	psrelbas	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to z : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
33	3	adantr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to R \in Ring$
34		eqid	$⊢ +_{R} = +_{R}$
35		eqid	$⊢ \cdot_{R} = \cdot_{R}$
36	16 34 35	ringdi	$⊢ (R \in Ring \land (r \in {Base}_{R} \land s \in {Base}_{R} \land t \in {Base}_{R})) \to r \cdot_{R} (s +_{R} t) = (r \cdot_{R} s) +_{R} (r \cdot_{R} t)$
37	33 36	sylan	$⊢ ((φ \land (x \in {Base}_{R} \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 \cdot_{R} (s +_{R} t) = (r \cdot_{R} s) +_{R} (r \cdot_{R} t)$
38	24 27 30 32 37	caofdi	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} (y {+_{R}}_{f} z) = ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} y) {+_{R}}_{f} ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} z)$
39		eqid	$⊢ +_{S} = +_{S}$
40	1 17 34 39 29 31	psradd	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to y +_{S} z = y {+_{R}}_{f} z$
41	40	oveq2d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} (y +_{S} z) = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} (y {+_{R}}_{f} z)$
42	1 15 16 17 35 28 25 29	psrvsca	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x \cdot_{S} y = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} y$
43	1 15 16 17 35 28 25 31	psrvsca	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x \cdot_{S} z = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} z$
44	42 43	oveq12d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (x \cdot_{S} y) {+_{R}}_{f} (x \cdot_{S} z) = ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} y) {+_{R}}_{f} ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} z)$
45	38 41 44	3eqtr4d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} (y +_{S} z) = (x \cdot_{S} y) {+_{R}}_{f} (x \cdot_{S} z)$
46	13	grpmgmd	$⊢ φ \to R \in Mgm$
47	46	adantr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to R \in Mgm$
48	1 17 39 47 29 31	psraddcl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to y +_{S} z \in {Base}_{S}$
49	1 15 16 17 35 28 25 48	psrvsca	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x \cdot_{S} (y +_{S} z) = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} (y +_{S} z)$
50	21	3adant3r3	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x \cdot_{S} y \in {Base}_{S}$
51	1 15 16 17 33 25 31	psrvscacl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x \cdot_{S} z \in {Base}_{S}$
52	1 17 34 39 50 51	psradd	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (x \cdot_{S} y) +_{S} (x \cdot_{S} z) = (x \cdot_{S} y) {+_{R}}_{f} (x \cdot_{S} z)$
53	45 49 52	3eqtr4d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x \cdot_{S} (y +_{S} z) = (x \cdot_{S} y) +_{S} (x \cdot_{S} z)$
54		simpr1	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to x \in {Base}_{R}$
55		simpr3	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to z \in {Base}_{S}$
56	1 15 16 17 35 28 54 55	psrvsca	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to x \cdot_{S} z = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} z$
57		simpr2	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to y \in {Base}_{R}$
58	1 15 16 17 35 28 57 55	psrvsca	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to y \cdot_{S} z = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\}) {\cdot_{R}}_{f} z$
59	56 58	oveq12d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (x \cdot_{S} z) {+_{R}}_{f} (y \cdot_{S} z) = ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} z) {+_{R}}_{f} ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\}) {\cdot_{R}}_{f} z)$
60	23	a1i	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
61	1 16 28 17 55	psrelbas	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to z : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
62	54 26	syl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
63		fconst6g	$⊢ y \in {Base}_{R} \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\}) : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
64	57 63	syl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\}) : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
65	3	adantr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to R \in Ring$
66	16 34 35	ringdir	$⊢ (R \in Ring \land (r \in {Base}_{R} \land s \in {Base}_{R} \land t \in {Base}_{R})) \to (r +_{R} s) \cdot_{R} t = (r \cdot_{R} t) +_{R} (s \cdot_{R} t)$
67	65 66	sylan	$⊢ ((φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \land (r \in {Base}_{R} \land s \in {Base}_{R} \land t \in {Base}_{R})) \to (r +_{R} s) \cdot_{R} t = (r \cdot_{R} t) +_{R} (s \cdot_{R} t)$
68	60 61 62 64 67	caofdir	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {+_{R}}_{f} (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\})) {\cdot_{R}}_{f} z = ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} z) {+_{R}}_{f} ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\}) {\cdot_{R}}_{f} z)$
69	60 54 57	ofc12	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {+_{R}}_{f} (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\}) = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x +_{R} y\}$
70	69	oveq1d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {+_{R}}_{f} (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\})) {\cdot_{R}}_{f} z = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x +_{R} y\}) {\cdot_{R}}_{f} z$
71	59 68 70	3eqtr2rd	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x +_{R} y\}) {\cdot_{R}}_{f} z = (x \cdot_{S} z) {+_{R}}_{f} (y \cdot_{S} z)$
72	16 34	ringacl	$⊢ (R \in Ring \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x +_{R} y \in {Base}_{R}$
73	65 54 57 72	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to x +_{R} y \in {Base}_{R}$
74	1 15 16 17 35 28 73 55	psrvsca	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (x +_{R} y) \cdot_{S} z = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x +_{R} y\}) {\cdot_{R}}_{f} z$
75	1 15 16 17 65 54 55	psrvscacl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to x \cdot_{S} z \in {Base}_{S}$
76	1 15 16 17 65 57 55	psrvscacl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to y \cdot_{S} z \in {Base}_{S}$
77	1 17 34 39 75 76	psradd	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (x \cdot_{S} z) +_{S} (y \cdot_{S} z) = (x \cdot_{S} z) {+_{R}}_{f} (y \cdot_{S} z)$
78	71 74 77	3eqtr4d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (x +_{R} y) \cdot_{S} z = (x \cdot_{S} z) +_{S} (y \cdot_{S} z)$
79	58	oveq2d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} (y \cdot_{S} z) = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\}) {\cdot_{R}}_{f} z)$
80	16 35	ringass	$⊢ (R \in Ring \land (r \in {Base}_{R} \land s \in {Base}_{R} \land t \in {Base}_{R})) \to (r \cdot_{R} s) \cdot_{R} t = r \cdot_{R} (s \cdot_{R} t)$
81	65 80	sylan	$⊢ ((φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \land (r \in {Base}_{R} \land s \in {Base}_{R} \land t \in {Base}_{R})) \to (r \cdot_{R} s) \cdot_{R} t = r \cdot_{R} (s \cdot_{R} t)$
82	60 62 64 61 81	caofass	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\})) {\cdot_{R}}_{f} z = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\}) {\cdot_{R}}_{f} z)$
83	60 54 57	ofc12	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\}) = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x \cdot_{R} y\}$
84	83	oveq1d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to ((\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{y\})) {\cdot_{R}}_{f} z = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x \cdot_{R} y\}) {\cdot_{R}}_{f} z$
85	79 82 84	3eqtr2rd	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x \cdot_{R} y\}) {\cdot_{R}}_{f} z = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} (y \cdot_{S} z)$
86	16 35	ringcl	$⊢ (R \in Ring \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \cdot_{R} y \in {Base}_{R}$
87	65 54 57 86	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to x \cdot_{R} y \in {Base}_{R}$
88	1 15 16 17 35 28 87 55	psrvsca	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (x \cdot_{R} y) \cdot_{S} z = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x \cdot_{R} y\}) {\cdot_{R}}_{f} z$
89	1 15 16 17 35 28 54 76	psrvsca	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to x \cdot_{S} (y \cdot_{S} z) = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{x\}) {\cdot_{R}}_{f} (y \cdot_{S} z)$
90	85 88 89	3eqtr4d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to (x \cdot_{R} y) \cdot_{S} z = x \cdot_{S} (y \cdot_{S} z)$
91	3	adantr	$⊢ (φ \land x \in {Base}_{S}) \to R \in Ring$
92		eqid	$⊢ 1_{R} = 1_{R}$
93	16 92	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
94	91 93	syl	$⊢ (φ \land x \in {Base}_{S}) \to 1_{R} \in {Base}_{R}$
95		simpr	$⊢ (φ \land x \in {Base}_{S}) \to x \in {Base}_{S}$
96	1 15 16 17 35 28 94 95	psrvsca	$⊢ (φ \land x \in {Base}_{S}) \to 1_{R} \cdot_{S} x = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{1_{R}\}) {\cdot_{R}}_{f} x$
97	23	a1i	$⊢ (φ \land x \in {Base}_{S}) \to \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
98	1 16 28 17 95	psrelbas	$⊢ (φ \land x \in {Base}_{S}) \to x : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
99	16 35 92	ringlidm	$⊢ (R \in Ring \land r \in {Base}_{R}) \to 1_{R} \cdot_{R} r = r$
100	91 99	sylan	$⊢ ((φ \land x \in {Base}_{S}) \land r \in {Base}_{R}) \to 1_{R} \cdot_{R} r = r$
101	97 98 94 100	caofid0l	$⊢ (φ \land x \in {Base}_{S}) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{1_{R}\}) {\cdot_{R}}_{f} x = x$
102	96 101	eqtrd	$⊢ (φ \land x \in {Base}_{S}) \to 1_{R} \cdot_{S} x = x$
103	4 5 6 7 8 9 10 11 3 14 21 53 78 90 102	islmodd	$⊢ φ \to S \in LMod$

Metamath Proof Explorer

Theorem psrlmod

Proof