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	adantr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to R \in Grp$
47	1 17 39 46 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}$
48	1 15 16 17 35 28 25 47	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)$
49	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}$
50	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}$
51	1 17 34 39 49 50	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)$
52	45 48 51	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)$
53		simpr1	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to x \in {Base}_{R}$
54		simpr3	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to z \in {Base}_{S}$
55	1 15 16 17 35 28 53 54	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$
56		simpr2	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to y \in {Base}_{R}$
57	1 15 16 17 35 28 56 54	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$
58	55 57	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)$
59	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$
60	1 16 28 17 54	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}$
61	53 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}$
62		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}$
63	56 62	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}$
64	3	adantr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to R \in Ring$
65	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)$
66	64 65	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)$
67	59 60 61 63 66	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)$
68	59 53 56	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\}$
69	68	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$
70	58 67 69	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)$
71	16 34	ringacl	$⊢ (R \in Ring \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x +_{R} y \in {Base}_{R}$
72	64 53 56 71	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to x +_{R} y \in {Base}_{R}$
73	1 15 16 17 35 28 72 54	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$
74	1 15 16 17 64 53 54	psrvscacl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to x \cdot_{S} z \in {Base}_{S}$
75	1 15 16 17 64 56 54	psrvscacl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to y \cdot_{S} z \in {Base}_{S}$
76	1 17 34 39 74 75	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)$
77	70 73 76	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)$
78	57	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)$
79	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)$
80	64 79	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)$
81	59 61 63 60 80	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)$
82	59 53 56	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\}$
83	82	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$
84	78 81 83	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)$
85	16 35	ringcl	$⊢ (R \in Ring \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \cdot_{R} y \in {Base}_{R}$
86	64 53 56 85	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{S})) \to x \cdot_{R} y \in {Base}_{R}$
87	1 15 16 17 35 28 86 54	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$
88	1 15 16 17 35 28 53 75	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)$
89	84 87 88	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)$
90	3	adantr	$⊢ (φ \land x \in {Base}_{S}) \to R \in Ring$
91		eqid	$⊢ 1_{R} = 1_{R}$
92	16 91	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
93	90 92	syl	$⊢ (φ \land x \in {Base}_{S}) \to 1_{R} \in {Base}_{R}$
94		simpr	$⊢ (φ \land x \in {Base}_{S}) \to x \in {Base}_{S}$
95	1 15 16 17 35 28 93 94	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$
96	23	a1i	$⊢ (φ \land x \in {Base}_{S}) \to \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
97	1 16 28 17 94	psrelbas	$⊢ (φ \land x \in {Base}_{S}) \to x : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
98	16 35 91	ringlidm	$⊢ (R \in Ring \land r \in {Base}_{R}) \to 1_{R} \cdot_{R} r = r$
99	90 98	sylan	$⊢ ((φ \land x \in {Base}_{S}) \land r \in {Base}_{R}) \to 1_{R} \cdot_{R} r = r$
100	96 97 93 99	caofid0l	$⊢ (φ \land x \in {Base}_{S}) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{1_{R}\}) {\cdot_{R}}_{f} x = x$
101	95 100	eqtrd	$⊢ (φ \land x \in {Base}_{S}) \to 1_{R} \cdot_{S} x = x$
102	4 5 6 7 8 9 10 11 3 14 21 52 77 89 101	islmodd	$⊢ φ \to S \in LMod$

Metamath Proof Explorer

Theorem psrlmod

Proof