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 = ( Base ` R )
rmodislmod.a 
|- .+ = ( +g ` R )
rmodislmod.s 
|- .x. = ( .s ` R )
rmodislmod.f 
|- F = ( Scalar ` R )
rmodislmod.k 
|- K = ( Base ` F )
rmodislmod.p 
|- .+^ = ( +g ` F )
rmodislmod.t 
|- .X. = ( .r ` F )
rmodislmod.u 
|- .1. = ( 1r ` F )
rmodislmod.r 
|- ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) )
rmodislmod.m 
|- .* = ( s e. K , v e. V |-> ( v .x. s ) )
rmodislmod.l 
|- L = ( R sSet <. ( .s ` ndx ) , .* >. )
Assertion rmodislmod 
|- ( F e. CRing -> L e. LMod )

Proof

Step Hyp Ref Expression
1 rmodislmod.v 
 |-  V = ( Base ` R )
2 rmodislmod.a 
 |-  .+ = ( +g ` R )
3 rmodislmod.s 
 |-  .x. = ( .s ` R )
4 rmodislmod.f 
 |-  F = ( Scalar ` R )
5 rmodislmod.k 
 |-  K = ( Base ` F )
6 rmodislmod.p 
 |-  .+^ = ( +g ` F )
7 rmodislmod.t 
 |-  .X. = ( .r ` F )
8 rmodislmod.u 
 |-  .1. = ( 1r ` F )
9 rmodislmod.r 
 |-  ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) )
10 rmodislmod.m 
 |-  .* = ( s e. K , v e. V |-> ( v .x. s ) )
11 rmodislmod.l 
 |-  L = ( R sSet <. ( .s ` ndx ) , .* >. )
12 baseid 
 |-  Base = Slot ( Base ` ndx )
13 vscandxnbasendx 
 |-  ( .s ` ndx ) =/= ( Base ` ndx )
14 13 necomi 
 |-  ( Base ` ndx ) =/= ( .s ` ndx )
15 12 14 setsnid 
 |-  ( Base ` R ) = ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
16 1 15 eqtri 
 |-  V = ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
17 11 eqcomi 
 |-  ( R sSet <. ( .s ` ndx ) , .* >. ) = L
18 17 fveq2i 
 |-  ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) = ( Base ` L )
19 16 18 eqtri 
 |-  V = ( Base ` L )
20 19 a1i 
 |-  ( F e. CRing -> V = ( Base ` L ) )
21 plusgid 
 |-  +g = Slot ( +g ` ndx )
22 vscandxnplusgndx 
 |-  ( .s ` ndx ) =/= ( +g ` ndx )
23 22 necomi 
 |-  ( +g ` ndx ) =/= ( .s ` ndx )
24 21 23 setsnid 
 |-  ( +g ` R ) = ( +g ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
25 11 fveq2i 
 |-  ( +g ` L ) = ( +g ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
26 24 2 25 3eqtr4i 
 |-  .+ = ( +g ` L )
27 26 a1i 
 |-  ( F e. CRing -> .+ = ( +g ` L ) )
28 scaid 
 |-  Scalar = Slot ( Scalar ` ndx )
29 vscandxnscandx 
 |-  ( .s ` ndx ) =/= ( Scalar ` ndx )
30 29 necomi 
 |-  ( Scalar ` ndx ) =/= ( .s ` ndx )
31 28 30 setsnid 
 |-  ( Scalar ` R ) = ( Scalar ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
32 11 fveq2i 
 |-  ( Scalar ` L ) = ( Scalar ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
33 31 4 32 3eqtr4i 
 |-  F = ( Scalar ` L )
34 33 a1i 
 |-  ( F e. CRing -> F = ( Scalar ` L ) )
35 9 simp1i 
 |-  R e. Grp
36 5 fvexi 
 |-  K e. _V
37 1 fvexi 
 |-  V e. _V
38 10 mpoexg 
 |-  ( ( K e. _V /\ V e. _V ) -> .* e. _V )
39 36 37 38 mp2an 
 |-  .* e. _V
40 vscaid 
 |-  .s = Slot ( .s ` ndx )
41 40 setsid 
 |-  ( ( R e. Grp /\ .* e. _V ) -> .* = ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) )
42 35 39 41 mp2an 
 |-  .* = ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
43 17 fveq2i 
 |-  ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) = ( .s ` L )
44 42 43 eqtri 
 |-  .* = ( .s ` L )
45 44 a1i 
 |-  ( F e. CRing -> .* = ( .s ` L ) )
46 5 a1i 
 |-  ( F e. CRing -> K = ( Base ` F ) )
47 6 a1i 
 |-  ( F e. CRing -> .+^ = ( +g ` F ) )
48 7 a1i 
 |-  ( F e. CRing -> .X. = ( .r ` F ) )
49 8 a1i 
 |-  ( F e. CRing -> .1. = ( 1r ` F ) )
50 crngring 
 |-  ( F e. CRing -> F e. Ring )
51 1 eqcomi 
 |-  ( Base ` R ) = V
52 51 19 eqtri 
 |-  ( Base ` R ) = ( Base ` L )
53 24 25 eqtr4i 
 |-  ( +g ` R ) = ( +g ` L )
54 52 53 grpprop 
 |-  ( R e. Grp <-> L e. Grp )
55 35 54 mpbi 
 |-  L e. Grp
56 55 a1i 
 |-  ( F e. CRing -> L e. Grp )
57 10 a1i 
 |-  ( ( F e. CRing /\ a e. K /\ b e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
58 oveq12 
 |-  ( ( v = b /\ s = a ) -> ( v .x. s ) = ( b .x. a ) )
59 58 ancoms 
 |-  ( ( s = a /\ v = b ) -> ( v .x. s ) = ( b .x. a ) )
60 59 adantl 
 |-  ( ( ( F e. CRing /\ a e. K /\ b e. V ) /\ ( s = a /\ v = b ) ) -> ( v .x. s ) = ( b .x. a ) )
61 simp2 
 |-  ( ( F e. CRing /\ a e. K /\ b e. V ) -> a e. K )
62 simp3 
 |-  ( ( F e. CRing /\ a e. K /\ b e. V ) -> b e. V )
63 ovexd 
 |-  ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( b .x. a ) e. _V )
64 57 60 61 62 63 ovmpod 
 |-  ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( a .* b ) = ( b .x. a ) )
65 simpl1 
 |-  ( ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> ( w .x. r ) e. V )
66 65 2ralimi 
 |-  ( A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> A. x e. V A. w e. V ( w .x. r ) e. V )
67 66 2ralimi 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V )
68 ringgrp 
 |-  ( F e. Ring -> F e. Grp )
69 5 grpbn0 
 |-  ( F e. Grp -> K =/= (/) )
70 68 69 syl 
 |-  ( F e. Ring -> K =/= (/) )
71 70 3ad2ant2 
 |-  ( ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) ) -> K =/= (/) )
72 9 71 ax-mp 
 |-  K =/= (/)
73 rspn0 
 |-  ( K =/= (/) -> ( A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V -> A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V ) )
74 72 73 ax-mp 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V -> A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V )
75 ralcom 
 |-  ( A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V <-> A. x e. V A. r e. K A. w e. V ( w .x. r ) e. V )
76 1 grpbn0 
 |-  ( R e. Grp -> V =/= (/) )
77 76 3ad2ant1 
 |-  ( ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) ) -> V =/= (/) )
78 9 77 ax-mp 
 |-  V =/= (/)
79 rspn0 
 |-  ( V =/= (/) -> ( A. x e. V A. r e. K A. w e. V ( w .x. r ) e. V -> A. r e. K A. w e. V ( w .x. r ) e. V ) )
80 78 79 ax-mp 
 |-  ( A. x e. V A. r e. K A. w e. V ( w .x. r ) e. V -> A. r e. K A. w e. V ( w .x. r ) e. V )
81 oveq2 
 |-  ( r = a -> ( w .x. r ) = ( w .x. a ) )
82 81 eleq1d 
 |-  ( r = a -> ( ( w .x. r ) e. V <-> ( w .x. a ) e. V ) )
83 oveq1 
 |-  ( w = b -> ( w .x. a ) = ( b .x. a ) )
84 83 eleq1d 
 |-  ( w = b -> ( ( w .x. a ) e. V <-> ( b .x. a ) e. V ) )
85 82 84 rspc2v 
 |-  ( ( a e. K /\ b e. V ) -> ( A. r e. K A. w e. V ( w .x. r ) e. V -> ( b .x. a ) e. V ) )
86 85 3adant1 
 |-  ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( A. r e. K A. w e. V ( w .x. r ) e. V -> ( b .x. a ) e. V ) )
87 80 86 syl5com 
 |-  ( A. x e. V A. r e. K A. w e. V ( w .x. r ) e. V -> ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( b .x. a ) e. V ) )
88 75 87 sylbi 
 |-  ( A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V -> ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( b .x. a ) e. V ) )
89 67 74 88 3syl 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( b .x. a ) e. V ) )
90 89 3ad2ant3 
 |-  ( ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) ) -> ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( b .x. a ) e. V ) )
91 9 90 ax-mp 
 |-  ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( b .x. a ) e. V )
92 64 91 eqeltrd 
 |-  ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( a .* b ) e. V )
93 10 a1i 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
94 oveq12 
 |-  ( ( v = ( b .+ c ) /\ s = a ) -> ( v .x. s ) = ( ( b .+ c ) .x. a ) )
95 94 ancoms 
 |-  ( ( s = a /\ v = ( b .+ c ) ) -> ( v .x. s ) = ( ( b .+ c ) .x. a ) )
96 95 adantl 
 |-  ( ( ( a e. K /\ b e. V /\ c e. V ) /\ ( s = a /\ v = ( b .+ c ) ) ) -> ( v .x. s ) = ( ( b .+ c ) .x. a ) )
97 simp1 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> a e. K )
98 1 2 grpcl 
 |-  ( ( R e. Grp /\ b e. V /\ c e. V ) -> ( b .+ c ) e. V )
99 35 98 mp3an1 
 |-  ( ( b e. V /\ c e. V ) -> ( b .+ c ) e. V )
100 99 3adant1 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> ( b .+ c ) e. V )
101 ovexd 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> ( ( b .+ c ) .x. a ) e. _V )
102 93 96 97 100 101 ovmpod 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* ( b .+ c ) ) = ( ( b .+ c ) .x. a ) )
103 simpl2 
 |-  ( ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) )
104 103 2ralimi 
 |-  ( A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> A. x e. V A. w e. V ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) )
105 104 2ralimi 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> A. q e. K A. r e. K A. x e. V A. w e. V ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) )
106 rspn0 
 |-  ( K =/= (/) -> ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) -> A. r e. K A. x e. V A. w e. V ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) ) )
107 72 106 ax-mp 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) -> A. r e. K A. x e. V A. w e. V ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) )
108 oveq2 
 |-  ( r = a -> ( ( w .+ x ) .x. r ) = ( ( w .+ x ) .x. a ) )
109 oveq2 
 |-  ( r = a -> ( x .x. r ) = ( x .x. a ) )
110 81 109 oveq12d 
 |-  ( r = a -> ( ( w .x. r ) .+ ( x .x. r ) ) = ( ( w .x. a ) .+ ( x .x. a ) ) )
111 108 110 eqeq12d 
 |-  ( r = a -> ( ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) <-> ( ( w .+ x ) .x. a ) = ( ( w .x. a ) .+ ( x .x. a ) ) ) )
112 oveq2 
 |-  ( x = c -> ( w .+ x ) = ( w .+ c ) )
113 112 oveq1d 
 |-  ( x = c -> ( ( w .+ x ) .x. a ) = ( ( w .+ c ) .x. a ) )
114 oveq1 
 |-  ( x = c -> ( x .x. a ) = ( c .x. a ) )
115 114 oveq2d 
 |-  ( x = c -> ( ( w .x. a ) .+ ( x .x. a ) ) = ( ( w .x. a ) .+ ( c .x. a ) ) )
116 113 115 eqeq12d 
 |-  ( x = c -> ( ( ( w .+ x ) .x. a ) = ( ( w .x. a ) .+ ( x .x. a ) ) <-> ( ( w .+ c ) .x. a ) = ( ( w .x. a ) .+ ( c .x. a ) ) ) )
117 oveq1 
 |-  ( w = b -> ( w .+ c ) = ( b .+ c ) )
118 117 oveq1d 
 |-  ( w = b -> ( ( w .+ c ) .x. a ) = ( ( b .+ c ) .x. a ) )
119 83 oveq1d 
 |-  ( w = b -> ( ( w .x. a ) .+ ( c .x. a ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
120 118 119 eqeq12d 
 |-  ( w = b -> ( ( ( w .+ c ) .x. a ) = ( ( w .x. a ) .+ ( c .x. a ) ) <-> ( ( b .+ c ) .x. a ) = ( ( b .x. a ) .+ ( c .x. a ) ) ) )
121 111 116 120 rspc3v 
 |-  ( ( a e. K /\ c e. V /\ b e. V ) -> ( A. r e. K A. x e. V A. w e. V ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) -> ( ( b .+ c ) .x. a ) = ( ( b .x. a ) .+ ( c .x. a ) ) ) )
122 121 3com23 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> ( A. r e. K A. x e. V A. w e. V ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) -> ( ( b .+ c ) .x. a ) = ( ( b .x. a ) .+ ( c .x. a ) ) ) )
123 107 122 syl5com 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) -> ( ( a e. K /\ b e. V /\ c e. V ) -> ( ( b .+ c ) .x. a ) = ( ( b .x. a ) .+ ( c .x. a ) ) ) )
124 105 123 syl 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> ( ( a e. K /\ b e. V /\ c e. V ) -> ( ( b .+ c ) .x. a ) = ( ( b .x. a ) .+ ( c .x. a ) ) ) )
125 124 3ad2ant3 
 |-  ( ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) ) -> ( ( a e. K /\ b e. V /\ c e. V ) -> ( ( b .+ c ) .x. a ) = ( ( b .x. a ) .+ ( c .x. a ) ) ) )
126 9 125 ax-mp 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> ( ( b .+ c ) .x. a ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
127 102 126 eqtrd 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* ( b .+ c ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
128 127 adantl 
 |-  ( ( F e. CRing /\ ( a e. K /\ b e. V /\ c e. V ) ) -> ( a .* ( b .+ c ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
129 59 adantl 
 |-  ( ( ( a e. K /\ b e. V /\ c e. V ) /\ ( s = a /\ v = b ) ) -> ( v .x. s ) = ( b .x. a ) )
130 simp2 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> b e. V )
131 ovexd 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> ( b .x. a ) e. _V )
132 93 129 97 130 131 ovmpod 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* b ) = ( b .x. a ) )
133 oveq12 
 |-  ( ( v = c /\ s = a ) -> ( v .x. s ) = ( c .x. a ) )
134 133 ancoms 
 |-  ( ( s = a /\ v = c ) -> ( v .x. s ) = ( c .x. a ) )
135 134 adantl 
 |-  ( ( ( a e. K /\ b e. V /\ c e. V ) /\ ( s = a /\ v = c ) ) -> ( v .x. s ) = ( c .x. a ) )
136 simp3 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> c e. V )
137 ovexd 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> ( c .x. a ) e. _V )
138 93 135 97 136 137 ovmpod 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
139 132 138 oveq12d 
 |-  ( ( a e. K /\ b e. V /\ c e. V ) -> ( ( a .* b ) .+ ( a .* c ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
140 139 adantl 
 |-  ( ( F e. CRing /\ ( a e. K /\ b e. V /\ c e. V ) ) -> ( ( a .* b ) .+ ( a .* c ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
141 128 140 eqtr4d 
 |-  ( ( F e. CRing /\ ( a e. K /\ b e. V /\ c e. V ) ) -> ( a .* ( b .+ c ) ) = ( ( a .* b ) .+ ( a .* c ) ) )
142 simpl3 
 |-  ( ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) )
143 142 2ralimi 
 |-  ( A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> A. x e. V A. w e. V ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) )
144 143 2ralimi 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) )
145 ralrot3 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) <-> A. x e. V A. q e. K A. r e. K A. w e. V ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) )
146 rspn0 
 |-  ( V =/= (/) -> ( A. x e. V A. q e. K A. r e. K A. w e. V ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) -> A. q e. K A. r e. K A. w e. V ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) )
147 78 146 ax-mp 
 |-  ( A. x e. V A. q e. K A. r e. K A. w e. V ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) -> A. q e. K A. r e. K A. w e. V ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) )
148 oveq1 
 |-  ( q = a -> ( q .+^ r ) = ( a .+^ r ) )
149 148 oveq2d 
 |-  ( q = a -> ( w .x. ( q .+^ r ) ) = ( w .x. ( a .+^ r ) ) )
150 oveq2 
 |-  ( q = a -> ( w .x. q ) = ( w .x. a ) )
151 150 oveq1d 
 |-  ( q = a -> ( ( w .x. q ) .+ ( w .x. r ) ) = ( ( w .x. a ) .+ ( w .x. r ) ) )
152 149 151 eqeq12d 
 |-  ( q = a -> ( ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) <-> ( w .x. ( a .+^ r ) ) = ( ( w .x. a ) .+ ( w .x. r ) ) ) )
153 oveq2 
 |-  ( r = b -> ( a .+^ r ) = ( a .+^ b ) )
154 153 oveq2d 
 |-  ( r = b -> ( w .x. ( a .+^ r ) ) = ( w .x. ( a .+^ b ) ) )
155 oveq2 
 |-  ( r = b -> ( w .x. r ) = ( w .x. b ) )
156 155 oveq2d 
 |-  ( r = b -> ( ( w .x. a ) .+ ( w .x. r ) ) = ( ( w .x. a ) .+ ( w .x. b ) ) )
157 154 156 eqeq12d 
 |-  ( r = b -> ( ( w .x. ( a .+^ r ) ) = ( ( w .x. a ) .+ ( w .x. r ) ) <-> ( w .x. ( a .+^ b ) ) = ( ( w .x. a ) .+ ( w .x. b ) ) ) )
158 oveq1 
 |-  ( w = c -> ( w .x. ( a .+^ b ) ) = ( c .x. ( a .+^ b ) ) )
159 oveq1 
 |-  ( w = c -> ( w .x. a ) = ( c .x. a ) )
160 oveq1 
 |-  ( w = c -> ( w .x. b ) = ( c .x. b ) )
161 159 160 oveq12d 
 |-  ( w = c -> ( ( w .x. a ) .+ ( w .x. b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) )
162 158 161 eqeq12d 
 |-  ( w = c -> ( ( w .x. ( a .+^ b ) ) = ( ( w .x. a ) .+ ( w .x. b ) ) <-> ( c .x. ( a .+^ b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) ) )
163 152 157 162 rspc3v 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( A. q e. K A. r e. K A. w e. V ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) -> ( c .x. ( a .+^ b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) ) )
164 147 163 syl5com 
 |-  ( A. x e. V A. q e. K A. r e. K A. w e. V ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) -> ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( a .+^ b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) ) )
165 145 164 sylbi 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) -> ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( a .+^ b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) ) )
166 144 165 syl 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( a .+^ b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) ) )
167 166 3ad2ant3 
 |-  ( ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) ) -> ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( a .+^ b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) ) )
168 9 167 ax-mp 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( a .+^ b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) )
169 10 a1i 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
170 oveq12 
 |-  ( ( v = c /\ s = ( a .+^ b ) ) -> ( v .x. s ) = ( c .x. ( a .+^ b ) ) )
171 170 ancoms 
 |-  ( ( s = ( a .+^ b ) /\ v = c ) -> ( v .x. s ) = ( c .x. ( a .+^ b ) ) )
172 171 adantl 
 |-  ( ( ( a e. K /\ b e. K /\ c e. V ) /\ ( s = ( a .+^ b ) /\ v = c ) ) -> ( v .x. s ) = ( c .x. ( a .+^ b ) ) )
173 5 6 grpcl 
 |-  ( ( F e. Grp /\ a e. K /\ b e. K ) -> ( a .+^ b ) e. K )
174 173 3expib 
 |-  ( F e. Grp -> ( ( a e. K /\ b e. K ) -> ( a .+^ b ) e. K ) )
175 68 174 syl 
 |-  ( F e. Ring -> ( ( a e. K /\ b e. K ) -> ( a .+^ b ) e. K ) )
176 175 3ad2ant2 
 |-  ( ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) ) -> ( ( a e. K /\ b e. K ) -> ( a .+^ b ) e. K ) )
177 9 176 ax-mp 
 |-  ( ( a e. K /\ b e. K ) -> ( a .+^ b ) e. K )
178 177 3adant3 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .+^ b ) e. K )
179 simp3 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> c e. V )
180 ovexd 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( a .+^ b ) ) e. _V )
181 169 172 178 179 180 ovmpod 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( a .+^ b ) .* c ) = ( c .x. ( a .+^ b ) ) )
182 134 adantl 
 |-  ( ( ( a e. K /\ b e. K /\ c e. V ) /\ ( s = a /\ v = c ) ) -> ( v .x. s ) = ( c .x. a ) )
183 simp1 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> a e. K )
184 ovexd 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. a ) e. _V )
185 169 182 183 179 184 ovmpod 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
186 oveq12 
 |-  ( ( v = c /\ s = b ) -> ( v .x. s ) = ( c .x. b ) )
187 186 ancoms 
 |-  ( ( s = b /\ v = c ) -> ( v .x. s ) = ( c .x. b ) )
188 187 adantl 
 |-  ( ( ( a e. K /\ b e. K /\ c e. V ) /\ ( s = b /\ v = c ) ) -> ( v .x. s ) = ( c .x. b ) )
189 simp2 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> b e. K )
190 ovexd 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. b ) e. _V )
191 169 188 189 179 190 ovmpod 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( b .* c ) = ( c .x. b ) )
192 185 191 oveq12d 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( a .* c ) .+ ( b .* c ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) )
193 168 181 192 3eqtr4d 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( a .+^ b ) .* c ) = ( ( a .* c ) .+ ( b .* c ) ) )
194 193 adantl 
 |-  ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( ( a .+^ b ) .* c ) = ( ( a .* c ) .+ ( b .* c ) ) )
195 1 2 3 4 5 6 7 8 9 10 11 rmodislmodlem 
 |-  ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( ( a .X. b ) .* c ) = ( a .* ( b .* c ) ) )
196 10 a1i 
 |-  ( ( F e. CRing /\ a e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
197 oveq12 
 |-  ( ( v = a /\ s = .1. ) -> ( v .x. s ) = ( a .x. .1. ) )
198 197 ancoms 
 |-  ( ( s = .1. /\ v = a ) -> ( v .x. s ) = ( a .x. .1. ) )
199 198 adantl 
 |-  ( ( ( F e. CRing /\ a e. V ) /\ ( s = .1. /\ v = a ) ) -> ( v .x. s ) = ( a .x. .1. ) )
200 5 8 ringidcl 
 |-  ( F e. Ring -> .1. e. K )
201 50 200 syl 
 |-  ( F e. CRing -> .1. e. K )
202 201 adantr 
 |-  ( ( F e. CRing /\ a e. V ) -> .1. e. K )
203 simpr 
 |-  ( ( F e. CRing /\ a e. V ) -> a e. V )
204 ovexd 
 |-  ( ( F e. CRing /\ a e. V ) -> ( a .x. .1. ) e. _V )
205 196 199 202 203 204 ovmpod 
 |-  ( ( F e. CRing /\ a e. V ) -> ( .1. .* a ) = ( a .x. .1. ) )
206 simprr 
 |-  ( ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> ( w .x. .1. ) = w )
207 206 2ralimi 
 |-  ( A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> A. x e. V A. w e. V ( w .x. .1. ) = w )
208 207 2ralimi 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w )
209 rspn0 
 |-  ( K =/= (/) -> ( A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w -> A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w ) )
210 72 209 ax-mp 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w -> A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w )
211 rspn0 
 |-  ( K =/= (/) -> ( A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w -> A. x e. V A. w e. V ( w .x. .1. ) = w ) )
212 72 211 ax-mp 
 |-  ( A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w -> A. x e. V A. w e. V ( w .x. .1. ) = w )
213 rspn0 
 |-  ( V =/= (/) -> ( A. x e. V A. w e. V ( w .x. .1. ) = w -> A. w e. V ( w .x. .1. ) = w ) )
214 78 213 ax-mp 
 |-  ( A. x e. V A. w e. V ( w .x. .1. ) = w -> A. w e. V ( w .x. .1. ) = w )
215 oveq1 
 |-  ( w = a -> ( w .x. .1. ) = ( a .x. .1. ) )
216 id 
 |-  ( w = a -> w = a )
217 215 216 eqeq12d 
 |-  ( w = a -> ( ( w .x. .1. ) = w <-> ( a .x. .1. ) = a ) )
218 217 rspcv 
 |-  ( a e. V -> ( A. w e. V ( w .x. .1. ) = w -> ( a .x. .1. ) = a ) )
219 218 adantl 
 |-  ( ( F e. CRing /\ a e. V ) -> ( A. w e. V ( w .x. .1. ) = w -> ( a .x. .1. ) = a ) )
220 214 219 syl5com 
 |-  ( A. x e. V A. w e. V ( w .x. .1. ) = w -> ( ( F e. CRing /\ a e. V ) -> ( a .x. .1. ) = a ) )
221 208 210 212 220 4syl 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> ( ( F e. CRing /\ a e. V ) -> ( a .x. .1. ) = a ) )
222 221 3ad2ant3 
 |-  ( ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) ) -> ( ( F e. CRing /\ a e. V ) -> ( a .x. .1. ) = a ) )
223 9 222 ax-mp 
 |-  ( ( F e. CRing /\ a e. V ) -> ( a .x. .1. ) = a )
224 205 223 eqtrd 
 |-  ( ( F e. CRing /\ a e. V ) -> ( .1. .* a ) = a )
225 20 27 34 45 46 47 48 49 50 56 92 141 194 195 224 islmodd 
 |-  ( F e. CRing -> L e. LMod )