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)

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