Metamath Proof Explorer


Theorem rmodislmod

Description: The right module R induces a left module L by replacing the scalar multiplication with a reversed multiplication if the scalar ring is commutative. The hypothesis "rmodislmod.r" is a definition of a right module analogous to Definition df-lmod of a left module, see also islmod . (Contributed by AV, 3-Dec-2021) (Proof shortened by AV, 18-Oct-2024)

Ref Expression
Hypotheses rmodislmod.v V=BaseR
rmodislmod.a +˙=+R
rmodislmod.s ·˙=R
rmodislmod.f F=ScalarR
rmodislmod.k K=BaseF
rmodislmod.p ˙=+F
rmodislmod.t ×˙=F
rmodislmod.u 1˙=1F
rmodislmod.r RGrpFRingqKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=w
rmodislmod.m ˙=sK,vVv·˙s
rmodislmod.l L=RsSetndx˙
Assertion rmodislmod FCRingLLMod

Proof

Step Hyp Ref Expression
1 rmodislmod.v V=BaseR
2 rmodislmod.a +˙=+R
3 rmodislmod.s ·˙=R
4 rmodislmod.f F=ScalarR
5 rmodislmod.k K=BaseF
6 rmodislmod.p ˙=+F
7 rmodislmod.t ×˙=F
8 rmodislmod.u 1˙=1F
9 rmodislmod.r RGrpFRingqKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=w
10 rmodislmod.m ˙=sK,vVv·˙s
11 rmodislmod.l L=RsSetndx˙
12 baseid Base=SlotBasendx
13 vscandxnbasendx ndxBasendx
14 13 necomi Basendxndx
15 12 14 setsnid BaseR=BaseRsSetndx˙
16 1 15 eqtri V=BaseRsSetndx˙
17 11 eqcomi RsSetndx˙=L
18 17 fveq2i BaseRsSetndx˙=BaseL
19 16 18 eqtri V=BaseL
20 19 a1i FCRingV=BaseL
21 plusgid +𝑔=Slot+ndx
22 vscandxnplusgndx ndx+ndx
23 22 necomi +ndxndx
24 21 23 setsnid +R=+RsSetndx˙
25 11 fveq2i +L=+RsSetndx˙
26 24 2 25 3eqtr4i +˙=+L
27 26 a1i FCRing+˙=+L
28 scaid Scalar=SlotScalarndx
29 vscandxnscandx ndxScalarndx
30 29 necomi Scalarndxndx
31 28 30 setsnid ScalarR=ScalarRsSetndx˙
32 11 fveq2i ScalarL=ScalarRsSetndx˙
33 31 4 32 3eqtr4i F=ScalarL
34 33 a1i FCRingF=ScalarL
35 9 simp1i RGrp
36 5 fvexi KV
37 1 fvexi VV
38 10 mpoexg KVVV˙V
39 36 37 38 mp2an ˙V
40 vscaid 𝑠=Slotndx
41 40 setsid RGrp˙V˙=RsSetndx˙
42 35 39 41 mp2an ˙=RsSetndx˙
43 17 fveq2i RsSetndx˙=L
44 42 43 eqtri ˙=L
45 44 a1i FCRing˙=L
46 5 a1i FCRingK=BaseF
47 6 a1i FCRing˙=+F
48 7 a1i FCRing×˙=F
49 8 a1i FCRing1˙=1F
50 crngring FCRingFRing
51 1 eqcomi BaseR=V
52 51 19 eqtri BaseR=BaseL
53 24 25 eqtr4i +R=+L
54 52 53 grpprop RGrpLGrp
55 35 54 mpbi LGrp
56 55 a1i FCRingLGrp
57 10 a1i FCRingaKbV˙=sK,vVv·˙s
58 oveq12 v=bs=av·˙s=b·˙a
59 58 ancoms s=av=bv·˙s=b·˙a
60 59 adantl FCRingaKbVs=av=bv·˙s=b·˙a
61 simp2 FCRingaKbVaK
62 simp3 FCRingaKbVbV
63 ovexd FCRingaKbVb·˙aV
64 57 60 61 62 63 ovmpod FCRingaKbVa˙b=b·˙a
65 simpl1 w·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=ww·˙rV
66 65 2ralimi xVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wxVwVw·˙rV
67 66 2ralimi qKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wqKrKxVwVw·˙rV
68 ringgrp FRingFGrp
69 5 grpbn0 FGrpK
70 68 69 syl FRingK
71 70 3ad2ant2 RGrpFRingqKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wK
72 9 71 ax-mp K
73 rspn0 KqKrKxVwVw·˙rVrKxVwVw·˙rV
74 72 73 ax-mp qKrKxVwVw·˙rVrKxVwVw·˙rV
75 ralcom rKxVwVw·˙rVxVrKwVw·˙rV
76 1 grpbn0 RGrpV
77 76 3ad2ant1 RGrpFRingqKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wV
78 9 77 ax-mp V
79 rspn0 VxVrKwVw·˙rVrKwVw·˙rV
80 78 79 ax-mp xVrKwVw·˙rVrKwVw·˙rV
81 oveq2 r=aw·˙r=w·˙a
82 81 eleq1d r=aw·˙rVw·˙aV
83 oveq1 w=bw·˙a=b·˙a
84 83 eleq1d w=bw·˙aVb·˙aV
85 82 84 rspc2v aKbVrKwVw·˙rVb·˙aV
86 85 3adant1 FCRingaKbVrKwVw·˙rVb·˙aV
87 80 86 syl5com xVrKwVw·˙rVFCRingaKbVb·˙aV
88 75 87 sylbi rKxVwVw·˙rVFCRingaKbVb·˙aV
89 67 74 88 3syl qKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wFCRingaKbVb·˙aV
90 89 3ad2ant3 RGrpFRingqKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wFCRingaKbVb·˙aV
91 9 90 ax-mp FCRingaKbVb·˙aV
92 64 91 eqeltrd FCRingaKbVa˙bV
93 10 a1i aKbVcV˙=sK,vVv·˙s
94 oveq12 v=b+˙cs=av·˙s=b+˙c·˙a
95 94 ancoms s=av=b+˙cv·˙s=b+˙c·˙a
96 95 adantl aKbVcVs=av=b+˙cv·˙s=b+˙c·˙a
97 simp1 aKbVcVaK
98 1 2 grpcl RGrpbVcVb+˙cV
99 35 98 mp3an1 bVcVb+˙cV
100 99 3adant1 aKbVcVb+˙cV
101 ovexd aKbVcVb+˙c·˙aV
102 93 96 97 100 101 ovmpod aKbVcVa˙b+˙c=b+˙c·˙a
103 simpl2 w·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=ww+˙x·˙r=w·˙r+˙x·˙r
104 103 2ralimi xVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wxVwVw+˙x·˙r=w·˙r+˙x·˙r
105 104 2ralimi qKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wqKrKxVwVw+˙x·˙r=w·˙r+˙x·˙r
106 rspn0 KqKrKxVwVw+˙x·˙r=w·˙r+˙x·˙rrKxVwVw+˙x·˙r=w·˙r+˙x·˙r
107 72 106 ax-mp qKrKxVwVw+˙x·˙r=w·˙r+˙x·˙rrKxVwVw+˙x·˙r=w·˙r+˙x·˙r
108 oveq2 r=aw+˙x·˙r=w+˙x·˙a
109 oveq2 r=ax·˙r=x·˙a
110 81 109 oveq12d r=aw·˙r+˙x·˙r=w·˙a+˙x·˙a
111 108 110 eqeq12d r=aw+˙x·˙r=w·˙r+˙x·˙rw+˙x·˙a=w·˙a+˙x·˙a
112 oveq2 x=cw+˙x=w+˙c
113 112 oveq1d x=cw+˙x·˙a=w+˙c·˙a
114 oveq1 x=cx·˙a=c·˙a
115 114 oveq2d x=cw·˙a+˙x·˙a=w·˙a+˙c·˙a
116 113 115 eqeq12d x=cw+˙x·˙a=w·˙a+˙x·˙aw+˙c·˙a=w·˙a+˙c·˙a
117 oveq1 w=bw+˙c=b+˙c
118 117 oveq1d w=bw+˙c·˙a=b+˙c·˙a
119 83 oveq1d w=bw·˙a+˙c·˙a=b·˙a+˙c·˙a
120 118 119 eqeq12d w=bw+˙c·˙a=w·˙a+˙c·˙ab+˙c·˙a=b·˙a+˙c·˙a
121 111 116 120 rspc3v aKcVbVrKxVwVw+˙x·˙r=w·˙r+˙x·˙rb+˙c·˙a=b·˙a+˙c·˙a
122 121 3com23 aKbVcVrKxVwVw+˙x·˙r=w·˙r+˙x·˙rb+˙c·˙a=b·˙a+˙c·˙a
123 107 122 syl5com qKrKxVwVw+˙x·˙r=w·˙r+˙x·˙raKbVcVb+˙c·˙a=b·˙a+˙c·˙a
124 105 123 syl qKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=waKbVcVb+˙c·˙a=b·˙a+˙c·˙a
125 124 3ad2ant3 RGrpFRingqKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=waKbVcVb+˙c·˙a=b·˙a+˙c·˙a
126 9 125 ax-mp aKbVcVb+˙c·˙a=b·˙a+˙c·˙a
127 102 126 eqtrd aKbVcVa˙b+˙c=b·˙a+˙c·˙a
128 127 adantl FCRingaKbVcVa˙b+˙c=b·˙a+˙c·˙a
129 59 adantl aKbVcVs=av=bv·˙s=b·˙a
130 simp2 aKbVcVbV
131 ovexd aKbVcVb·˙aV
132 93 129 97 130 131 ovmpod aKbVcVa˙b=b·˙a
133 oveq12 v=cs=av·˙s=c·˙a
134 133 ancoms s=av=cv·˙s=c·˙a
135 134 adantl aKbVcVs=av=cv·˙s=c·˙a
136 simp3 aKbVcVcV
137 ovexd aKbVcVc·˙aV
138 93 135 97 136 137 ovmpod aKbVcVa˙c=c·˙a
139 132 138 oveq12d aKbVcVa˙b+˙a˙c=b·˙a+˙c·˙a
140 139 adantl FCRingaKbVcVa˙b+˙a˙c=b·˙a+˙c·˙a
141 128 140 eqtr4d FCRingaKbVcVa˙b+˙c=a˙b+˙a˙c
142 simpl3 w·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=ww·˙q˙r=w·˙q+˙w·˙r
143 142 2ralimi xVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wxVwVw·˙q˙r=w·˙q+˙w·˙r
144 143 2ralimi qKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wqKrKxVwVw·˙q˙r=w·˙q+˙w·˙r
145 ralrot3 qKrKxVwVw·˙q˙r=w·˙q+˙w·˙rxVqKrKwVw·˙q˙r=w·˙q+˙w·˙r
146 rspn0 VxVqKrKwVw·˙q˙r=w·˙q+˙w·˙rqKrKwVw·˙q˙r=w·˙q+˙w·˙r
147 78 146 ax-mp xVqKrKwVw·˙q˙r=w·˙q+˙w·˙rqKrKwVw·˙q˙r=w·˙q+˙w·˙r
148 oveq1 q=aq˙r=a˙r
149 148 oveq2d q=aw·˙q˙r=w·˙a˙r
150 oveq2 q=aw·˙q=w·˙a
151 150 oveq1d q=aw·˙q+˙w·˙r=w·˙a+˙w·˙r
152 149 151 eqeq12d q=aw·˙q˙r=w·˙q+˙w·˙rw·˙a˙r=w·˙a+˙w·˙r
153 oveq2 r=ba˙r=a˙b
154 153 oveq2d r=bw·˙a˙r=w·˙a˙b
155 oveq2 r=bw·˙r=w·˙b
156 155 oveq2d r=bw·˙a+˙w·˙r=w·˙a+˙w·˙b
157 154 156 eqeq12d r=bw·˙a˙r=w·˙a+˙w·˙rw·˙a˙b=w·˙a+˙w·˙b
158 oveq1 w=cw·˙a˙b=c·˙a˙b
159 oveq1 w=cw·˙a=c·˙a
160 oveq1 w=cw·˙b=c·˙b
161 159 160 oveq12d w=cw·˙a+˙w·˙b=c·˙a+˙c·˙b
162 158 161 eqeq12d w=cw·˙a˙b=w·˙a+˙w·˙bc·˙a˙b=c·˙a+˙c·˙b
163 152 157 162 rspc3v aKbKcVqKrKwVw·˙q˙r=w·˙q+˙w·˙rc·˙a˙b=c·˙a+˙c·˙b
164 147 163 syl5com xVqKrKwVw·˙q˙r=w·˙q+˙w·˙raKbKcVc·˙a˙b=c·˙a+˙c·˙b
165 145 164 sylbi qKrKxVwVw·˙q˙r=w·˙q+˙w·˙raKbKcVc·˙a˙b=c·˙a+˙c·˙b
166 144 165 syl qKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=waKbKcVc·˙a˙b=c·˙a+˙c·˙b
167 166 3ad2ant3 RGrpFRingqKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=waKbKcVc·˙a˙b=c·˙a+˙c·˙b
168 9 167 ax-mp aKbKcVc·˙a˙b=c·˙a+˙c·˙b
169 10 a1i aKbKcV˙=sK,vVv·˙s
170 oveq12 v=cs=a˙bv·˙s=c·˙a˙b
171 170 ancoms s=a˙bv=cv·˙s=c·˙a˙b
172 171 adantl aKbKcVs=a˙bv=cv·˙s=c·˙a˙b
173 5 6 grpcl FGrpaKbKa˙bK
174 173 3expib FGrpaKbKa˙bK
175 68 174 syl FRingaKbKa˙bK
176 175 3ad2ant2 RGrpFRingqKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=waKbKa˙bK
177 9 176 ax-mp aKbKa˙bK
178 177 3adant3 aKbKcVa˙bK
179 simp3 aKbKcVcV
180 ovexd aKbKcVc·˙a˙bV
181 169 172 178 179 180 ovmpod aKbKcVa˙b˙c=c·˙a˙b
182 134 adantl aKbKcVs=av=cv·˙s=c·˙a
183 simp1 aKbKcVaK
184 ovexd aKbKcVc·˙aV
185 169 182 183 179 184 ovmpod aKbKcVa˙c=c·˙a
186 oveq12 v=cs=bv·˙s=c·˙b
187 186 ancoms s=bv=cv·˙s=c·˙b
188 187 adantl aKbKcVs=bv=cv·˙s=c·˙b
189 simp2 aKbKcVbK
190 ovexd aKbKcVc·˙bV
191 169 188 189 179 190 ovmpod aKbKcVb˙c=c·˙b
192 185 191 oveq12d aKbKcVa˙c+˙b˙c=c·˙a+˙c·˙b
193 168 181 192 3eqtr4d aKbKcVa˙b˙c=a˙c+˙b˙c
194 193 adantl FCRingaKbKcVa˙b˙c=a˙c+˙b˙c
195 1 2 3 4 5 6 7 8 9 10 11 rmodislmodlem FCRingaKbKcVa×˙b˙c=a˙b˙c
196 10 a1i FCRingaV˙=sK,vVv·˙s
197 oveq12 v=as=1˙v·˙s=a·˙1˙
198 197 ancoms s=1˙v=av·˙s=a·˙1˙
199 198 adantl FCRingaVs=1˙v=av·˙s=a·˙1˙
200 5 8 ringidcl FRing1˙K
201 50 200 syl FCRing1˙K
202 201 adantr FCRingaV1˙K
203 simpr FCRingaVaV
204 ovexd FCRingaVa·˙1˙V
205 196 199 202 203 204 ovmpod FCRingaV1˙˙a=a·˙1˙
206 simprr w·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=ww·˙1˙=w
207 206 2ralimi xVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wxVwVw·˙1˙=w
208 207 2ralimi qKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wqKrKxVwVw·˙1˙=w
209 rspn0 KqKrKxVwVw·˙1˙=wrKxVwVw·˙1˙=w
210 72 209 ax-mp qKrKxVwVw·˙1˙=wrKxVwVw·˙1˙=w
211 rspn0 KrKxVwVw·˙1˙=wxVwVw·˙1˙=w
212 72 211 ax-mp rKxVwVw·˙1˙=wxVwVw·˙1˙=w
213 rspn0 VxVwVw·˙1˙=wwVw·˙1˙=w
214 78 213 ax-mp xVwVw·˙1˙=wwVw·˙1˙=w
215 oveq1 w=aw·˙1˙=a·˙1˙
216 id w=aw=a
217 215 216 eqeq12d w=aw·˙1˙=wa·˙1˙=a
218 217 rspcv aVwVw·˙1˙=wa·˙1˙=a
219 218 adantl FCRingaVwVw·˙1˙=wa·˙1˙=a
220 214 219 syl5com xVwVw·˙1˙=wFCRingaVa·˙1˙=a
221 212 220 syl rKxVwVw·˙1˙=wFCRingaVa·˙1˙=a
222 208 210 221 3syl qKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wFCRingaVa·˙1˙=a
223 222 3ad2ant3 RGrpFRingqKrKxVwVw·˙rVw+˙x·˙r=w·˙r+˙x·˙rw·˙q˙r=w·˙q+˙w·˙rw·˙q×˙r=w·˙q·˙rw·˙1˙=wFCRingaVa·˙1˙=a
224 9 223 ax-mp FCRingaVa·˙1˙=a
225 205 224 eqtrd FCRingaV1˙˙a=a
226 20 27 34 45 46 47 48 49 50 56 92 141 194 195 225 islmodd FCRingLLMod