Theorem rmodislmod 13446

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 13384 of a left module, see also islmod 13386. (Contributed by AV, 3-Dec-2021.) (Proof shortened by AV, 18-Oct-2024.)

Hypotheses

Ref	Expression
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

Ref	Expression
rmodislmod	|- ( F e. CRing -> L e. LMod )

Distinct variable groups:   .X. , q, r, w, x   .X. , s, v   .x. , q, r, w, x   .x. , s, v   K, q, r, x   K, s, v   V, q, r, w, x   V, s, v   F, s, v   .1. , s, v   .1. , q, r, w, x   .+ , q, r, w, x   .+ , s, v   .+^ , q, r, w, x   .+^ , s, v

Allowed substitution hints:   R( x, w, v, s, r, q)   F( x, w, r, q)   .* ( x, w, v, s, r, q)   K( w)   L( x, w, v, s, r, q)

Proof of Theorem rmodislmod

Dummy variables a b c j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rmodislmod.v	. . . . 5 |- V = ( Base ` R )
2		rmodislmod.r	. . . . . . 7 |- ( 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 ) ) )
3	2	simp1i 1006	. . . . . 6 |- R e. Grp
4		rmodislmod.k	. . . . . . . 8 |- K = ( Base ` F )
5		basfn 12522	. . . . . . . . 9 |- Base Fn _V
6	2	simp2i 1007	. . . . . . . . . 10 |- F e. Ring
7	6	elexi 2751	. . . . . . . . 9 |- F e. _V
8		funfvex 5534	. . . . . . . . . 10 |- ( ( Fun Base /\ F e. dom Base ) -> ( Base ` F ) e. _V )
9	8	funfni 5318	. . . . . . . . 9 |- ( ( Base Fn _V /\ F e. _V ) -> ( Base ` F ) e. _V )
10	5, 7, 9	mp2an 426	. . . . . . . 8 |- ( Base ` F ) e. _V
11	4, 10	eqeltri 2250	. . . . . . 7 |- K e. _V
12	3	elexi 2751	. . . . . . . . 9 |- R e. _V
13		funfvex 5534	. . . . . . . . . 10 |- ( ( Fun Base /\ R e. dom Base ) -> ( Base ` R ) e. _V )
14	13	funfni 5318	. . . . . . . . 9 |- ( ( Base Fn _V /\ R e. _V ) -> ( Base ` R ) e. _V )
15	5, 12, 14	mp2an 426	. . . . . . . 8 |- ( Base ` R ) e. _V
16	1, 15	eqeltri 2250	. . . . . . 7 |- V e. _V
17		rmodislmod.m	. . . . . . . 8 |- .* = ( s e. K , v e. V |-> ( v .x. s ) )
18	17	mpoexg 6214	. . . . . . 7 |- ( ( K e. _V /\ V e. _V ) -> .* e. _V )
19	11, 16, 18	mp2an 426	. . . . . 6 |- .* e. _V
20		baseslid 12521	. . . . . . 7 |- ( Base = Slot ( Base ` ndx ) /\ ( Base ` ndx ) e. NN )
21		vscandxnbasendx 12619	. . . . . . . 8 |- ( .s ` ndx ) =/= ( Base ` ndx )
22	21	necomi 2432	. . . . . . 7 |- ( Base ` ndx ) =/= ( .s ` ndx )
23		vscaslid 12623	. . . . . . . 8 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
24	23	simpri 113	. . . . . . 7 |- ( .s ` ndx ) e. NN
25	20, 22, 24	setsslnid 12516	. . . . . 6 |- ( ( R e. Grp /\ .* e. _V ) -> ( Base ` R ) = ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) )
26	3, 19, 25	mp2an 426	. . . . 5 |- ( Base ` R ) = ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
27	1, 26	eqtri 2198	. . . 4 |- V = ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
28		rmodislmod.l	. . . . . 6 |- L = ( R sSet <. ( .s ` ndx ) , .* >. )
29	28	eqcomi 2181	. . . . 5 |- ( R sSet <. ( .s ` ndx ) , .* >. ) = L
30	29	fveq2i 5520	. . . 4 |- ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) = ( Base ` L )
31	27, 30	eqtri 2198	. . 3 |- V = ( Base ` L )
32	31	a1i 9	. 2 |- ( F e. CRing -> V = ( Base ` L ) )
33		plusgslid 12573	. . . . . 6 |- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )
34		vscandxnplusgndx 12620	. . . . . . 7 |- ( .s ` ndx ) =/= ( +g ` ndx )
35	34	necomi 2432	. . . . . 6 |- ( +g ` ndx ) =/= ( .s ` ndx )
36	33, 35, 24	setsslnid 12516	. . . . 5 |- ( ( R e. Grp /\ .* e. _V ) -> ( +g ` R ) = ( +g ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) )
37	3, 19, 36	mp2an 426	. . . 4 |- ( +g ` R ) = ( +g ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
38		rmodislmod.a	. . . 4 |- .+ = ( +g ` R )
39	28	fveq2i 5520	. . . 4 |- ( +g ` L ) = ( +g ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
40	37, 38, 39	3eqtr4i 2208	. . 3 |- .+ = ( +g ` L )
41	40	a1i 9	. 2 |- ( F e. CRing -> .+ = ( +g ` L ) )
42		scaslid 12613	. . . . . 6 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
43		vscandxnscandx 12622	. . . . . . 7 |- ( .s ` ndx ) =/= (Scalar ` ndx )
44	43	necomi 2432	. . . . . 6 |- (Scalar ` ndx ) =/= ( .s ` ndx )
45	42, 44, 24	setsslnid 12516	. . . . 5 |- ( ( R e. Grp /\ .* e. _V ) -> (Scalar ` R ) = (Scalar ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) )
46	3, 19, 45	mp2an 426	. . . 4 |- (Scalar ` R ) = (Scalar ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
47		rmodislmod.f	. . . 4 |- F = (Scalar ` R )
48	28	fveq2i 5520	. . . 4 |- (Scalar ` L ) = (Scalar ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
49	46, 47, 48	3eqtr4i 2208	. . 3 |- F = (Scalar ` L )
50	49	a1i 9	. 2 |- ( F e. CRing -> F = (Scalar ` L ) )
51	23	setsslid 12515	. . . . 5 |- ( ( R e. Grp /\ .* e. _V ) -> .* = ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) )
52	3, 19, 51	mp2an 426	. . . 4 |- .* = ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
53	29	fveq2i 5520	. . . 4 |- ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) = ( .s ` L )
54	52, 53	eqtri 2198	. . 3 |- .* = ( .s ` L )
55	54	a1i 9	. 2 |- ( F e. CRing -> .* = ( .s ` L ) )
56	4	a1i 9	. 2 |- ( F e. CRing -> K = ( Base ` F ) )
57		rmodislmod.p	. . 3 |- .+^ = ( +g ` F )
58	57	a1i 9	. 2 |- ( F e. CRing -> .+^ = ( +g ` F ) )
59		rmodislmod.t	. . 3 |- .X. = ( .r ` F )
60	59	a1i 9	. 2 |- ( F e. CRing -> .X. = ( .r ` F ) )
61		rmodislmod.u	. . 3 |- .1. = ( 1r ` F )
62	61	a1i 9	. 2 |- ( F e. CRing -> .1. = ( 1r ` F ) )
63		crngring 13196	. 2 |- ( F e. CRing -> F e. Ring )
64	1	eqcomi 2181	. . . . . 6 |- ( Base ` R ) = V
65	64, 31	eqtri 2198	. . . . 5 |- ( Base ` R ) = ( Base ` L )
66	37, 39	eqtr4i 2201	. . . . 5 |- ( +g ` R ) = ( +g ` L )
67	65, 66	grpprop 12899	. . . 4 |- ( R e. Grp <-> L e. Grp )
68	3, 67	mpbi 145	. . 3 |- L e. Grp
69	68	a1i 9	. 2 |- ( F e. CRing -> L e. Grp )
70	17	a1i 9	. . . 4 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
71		oveq12 5886	. . . . . 6 |- ( ( v = b /\ s = a ) -> ( v .x. s ) = ( b .x. a ) )
72	71	ancoms 268	. . . . 5 |- ( ( s = a /\ v = b ) -> ( v .x. s ) = ( b .x. a ) )
73	72	adantl 277	. . . 4 |- ( ( ( F e. CRing /\ a e. K /\ b e. V ) /\ ( s = a /\ v = b ) ) -> ( v .x. s ) = ( b .x. a ) )
74		simp2 998	. . . 4 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> a e. K )
75		simp3 999	. . . 4 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> b e. V )
76		vex 2742	. . . . . 6 |- b e. _V
77		rmodislmod.s	. . . . . . 7 |- .x. = ( .s ` R )
78	23	slotex 12491	. . . . . . . 8 |- ( R e. Grp -> ( .s ` R ) e. _V )
79	3, 78	ax-mp 5	. . . . . . 7 |- ( .s ` R ) e. _V
80	77, 79	eqeltri 2250	. . . . . 6 |- .x. e. _V
81		vex 2742	. . . . . 6 |- a e. _V
82		ovexg 5911	. . . . . 6 |- ( ( b e. _V /\ .x. e. _V /\ a e. _V ) -> ( b .x. a ) e. _V )
83	76, 80, 81, 82	mp3an 1337	. . . . 5 |- ( b .x. a ) e. _V
84	83	a1i 9	. . . 4 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( b .x. a ) e. _V )
85	70, 73, 74, 75, 84	ovmpod 6004	. . 3 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( a .* b ) = ( b .x. a ) )
86		simpl1 1000	. . . . . . . 8 |- ( ( ( ( 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 )
87	86	2ralimi 2541	. . . . . . 7 |- ( 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 )
88	87	2ralimi 2541	. . . . . 6 |- ( 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 )
89	4, 61	ringidcl 13208	. . . . . . . . . 10 |- ( F e. Ring -> .1. e. K )
90		elex2 2755	. . . . . . . . . 10 |- ( .1. e. K -> E. j j e. K )
91	89, 90	syl 14	. . . . . . . . 9 |- ( F e. Ring -> E. j j e. K )
92	6, 91	ax-mp 5	. . . . . . . 8 |- E. j j e. K
93		r19.3rmv 3515	. . . . . . . 8 |- ( E. j j e. K -> ( A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V <-> A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V ) )
94	92, 93	ax-mp 5	. . . . . . 7 |- ( A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V <-> A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V )
95	94	biimpri 133	. . . . . 6 |- ( 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 )
96		ralcom 2640	. . . . . . 7 |- ( 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 )
97		eqid 2177	. . . . . . . . . . . . 13 |- ( 0g ` R ) = ( 0g ` R )
98	1, 97	grpidcl 12909	. . . . . . . . . . . 12 |- ( R e. Grp -> ( 0g ` R ) e. V )
99	3, 98	ax-mp 5	. . . . . . . . . . 11 |- ( 0g ` R ) e. V
100		elex2 2755	. . . . . . . . . . 11 |- ( ( 0g ` R ) e. V -> E. j j e. V )
101	99, 100	ax-mp 5	. . . . . . . . . 10 |- E. j j e. V
102		r19.3rmv 3515	. . . . . . . . . 10 |- ( E. j j e. V -> ( A. r e. K 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 ) )
103	101, 102	ax-mp 5	. . . . . . . . 9 |- ( A. r e. K 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 )
104	103	biimpri 133	. . . . . . . 8 |- ( 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 )
105		oveq2 5885	. . . . . . . . . . 11 |- ( r = a -> ( w .x. r ) = ( w .x. a ) )
106	105	eleq1d 2246	. . . . . . . . . 10 |- ( r = a -> ( ( w .x. r ) e. V <-> ( w .x. a ) e. V ) )
107		oveq1 5884	. . . . . . . . . . 11 |- ( w = b -> ( w .x. a ) = ( b .x. a ) )
108	107	eleq1d 2246	. . . . . . . . . 10 |- ( w = b -> ( ( w .x. a ) e. V <-> ( b .x. a ) e. V ) )
109	106, 108	rspc2v 2856	. . . . . . . . 9 |- ( ( a e. K /\ b e. V ) -> ( A. r e. K A. w e. V ( w .x. r ) e. V -> ( b .x. a ) e. V ) )
110	109	3adant1 1015	. . . . . . . 8 |- ( ( 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 ) )
111	104, 110	syl5com 29	. . . . . . 7 |- ( 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 ) )
112	96, 111	sylbi 121	. . . . . 6 |- ( 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 ) )
113	88, 95, 112	3syl 17	. . . . 5 |- ( 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 ) )
114	113	3ad2ant3 1020	. . . 4 |- ( ( 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 ) )
115	2, 114	ax-mp 5	. . 3 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( b .x. a ) e. V )
116	85, 115	eqeltrd 2254	. 2 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( a .* b ) e. V )
117	17	a1i 9	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
118		oveq12 5886	. . . . . . . 8 |- ( ( v = ( b .+ c ) /\ s = a ) -> ( v .x. s ) = ( ( b .+ c ) .x. a ) )
119	118	ancoms 268	. . . . . . 7 |- ( ( s = a /\ v = ( b .+ c ) ) -> ( v .x. s ) = ( ( b .+ c ) .x. a ) )
120	119	adantl 277	. . . . . 6 |- ( ( ( a e. K /\ b e. V /\ c e. V ) /\ ( s = a /\ v = ( b .+ c ) ) ) -> ( v .x. s ) = ( ( b .+ c ) .x. a ) )
121		simp1 997	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> a e. K )
122	1, 38	grpcl 12890	. . . . . . . 8 |- ( ( R e. Grp /\ b e. V /\ c e. V ) -> ( b .+ c ) e. V )
123	3, 122	mp3an1 1324	. . . . . . 7 |- ( ( b e. V /\ c e. V ) -> ( b .+ c ) e. V )
124	123	3adant1 1015	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( b .+ c ) e. V )
125	33	slotex 12491	. . . . . . . . . . 11 |- ( R e. Grp -> ( +g ` R ) e. _V )
126	3, 125	ax-mp 5	. . . . . . . . . 10 |- ( +g ` R ) e. _V
127	38, 126	eqeltri 2250	. . . . . . . . 9 |- .+ e. _V
128		vex 2742	. . . . . . . . 9 |- c e. _V
129		ovexg 5911	. . . . . . . . 9 |- ( ( b e. _V /\ .+ e. _V /\ c e. _V ) -> ( b .+ c ) e. _V )
130	76, 127, 128, 129	mp3an 1337	. . . . . . . 8 |- ( b .+ c ) e. _V
131		ovexg 5911	. . . . . . . 8 |- ( ( ( b .+ c ) e. _V /\ .x. e. _V /\ a e. _V ) -> ( ( b .+ c ) .x. a ) e. _V )
132	130, 80, 81, 131	mp3an 1337	. . . . . . 7 |- ( ( b .+ c ) .x. a ) e. _V
133	132	a1i 9	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( ( b .+ c ) .x. a ) e. _V )
134	117, 120, 121, 124, 133	ovmpod 6004	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* ( b .+ c ) ) = ( ( b .+ c ) .x. a ) )
135		simpl2 1001	. . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
136	135	2ralimi 2541	. . . . . . . . 9 |- ( 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 ) ) )
137	136	2ralimi 2541	. . . . . . . 8 |- ( 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 ) ) )
138		r19.3rmv 3515	. . . . . . . . . . 11 |- ( E. j j 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. 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 ) ) ) )
139	92, 138	ax-mp 5	. . . . . . . . . 10 |- ( A. r e. K A. x e. V A. w e. V ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) <-> 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 ) ) )
140	139	biimpri 133	. . . . . . . . 9 |- ( 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 ) ) )
141		oveq2 5885	. . . . . . . . . . . 12 |- ( r = a -> ( ( w .+ x ) .x. r ) = ( ( w .+ x ) .x. a ) )
142		oveq2 5885	. . . . . . . . . . . . 13 |- ( r = a -> ( x .x. r ) = ( x .x. a ) )
143	105, 142	oveq12d 5895	. . . . . . . . . . . 12 |- ( r = a -> ( ( w .x. r ) .+ ( x .x. r ) ) = ( ( w .x. a ) .+ ( x .x. a ) ) )
144	141, 143	eqeq12d 2192	. . . . . . . . . . 11 |- ( r = a -> ( ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) <-> ( ( w .+ x ) .x. a ) = ( ( w .x. a ) .+ ( x .x. a ) ) ) )
145		oveq2 5885	. . . . . . . . . . . . 13 |- ( x = c -> ( w .+ x ) = ( w .+ c ) )
146	145	oveq1d 5892	. . . . . . . . . . . 12 |- ( x = c -> ( ( w .+ x ) .x. a ) = ( ( w .+ c ) .x. a ) )
147		oveq1 5884	. . . . . . . . . . . . 13 |- ( x = c -> ( x .x. a ) = ( c .x. a ) )
148	147	oveq2d 5893	. . . . . . . . . . . 12 |- ( x = c -> ( ( w .x. a ) .+ ( x .x. a ) ) = ( ( w .x. a ) .+ ( c .x. a ) ) )
149	146, 148	eqeq12d 2192	. . . . . . . . . . 11 |- ( x = c -> ( ( ( w .+ x ) .x. a ) = ( ( w .x. a ) .+ ( x .x. a ) ) <-> ( ( w .+ c ) .x. a ) = ( ( w .x. a ) .+ ( c .x. a ) ) ) )
150		oveq1 5884	. . . . . . . . . . . . 13 |- ( w = b -> ( w .+ c ) = ( b .+ c ) )
151	150	oveq1d 5892	. . . . . . . . . . . 12 |- ( w = b -> ( ( w .+ c ) .x. a ) = ( ( b .+ c ) .x. a ) )
152	107	oveq1d 5892	. . . . . . . . . . . 12 |- ( w = b -> ( ( w .x. a ) .+ ( c .x. a ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
153	151, 152	eqeq12d 2192	. . . . . . . . . . 11 |- ( w = b -> ( ( ( w .+ c ) .x. a ) = ( ( w .x. a ) .+ ( c .x. a ) ) <-> ( ( b .+ c ) .x. a ) = ( ( b .x. a ) .+ ( c .x. a ) ) ) )
154	144, 149, 153	rspc3v 2859	. . . . . . . . . 10 |- ( ( 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 ) ) ) )
155	154	3com23 1209	. . . . . . . . 9 |- ( ( 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 ) ) ) )
156	140, 155	syl5com 29	. . . . . . . 8 |- ( 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 ) ) ) )
157	137, 156	syl 14	. . . . . . 7 |- ( 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 ) ) ) )
158	157	3ad2ant3 1020	. . . . . 6 |- ( ( 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 ) ) ) )
159	2, 158	ax-mp 5	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( ( b .+ c ) .x. a ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
160	134, 159	eqtrd 2210	. . . 4 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* ( b .+ c ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
161	160	adantl 277	. . 3 |- ( ( F e. CRing /\ ( a e. K /\ b e. V /\ c e. V ) ) -> ( a .* ( b .+ c ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
162	72	adantl 277	. . . . . 6 |- ( ( ( a e. K /\ b e. V /\ c e. V ) /\ ( s = a /\ v = b ) ) -> ( v .x. s ) = ( b .x. a ) )
163		simp2 998	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> b e. V )
164	83	a1i 9	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( b .x. a ) e. _V )
165	117, 162, 121, 163, 164	ovmpod 6004	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* b ) = ( b .x. a ) )
166		oveq12 5886	. . . . . . . 8 |- ( ( v = c /\ s = a ) -> ( v .x. s ) = ( c .x. a ) )
167	166	ancoms 268	. . . . . . 7 |- ( ( s = a /\ v = c ) -> ( v .x. s ) = ( c .x. a ) )
168	167	adantl 277	. . . . . 6 |- ( ( ( a e. K /\ b e. V /\ c e. V ) /\ ( s = a /\ v = c ) ) -> ( v .x. s ) = ( c .x. a ) )
169		simp3 999	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> c e. V )
170		ovexg 5911	. . . . . . . 8 |- ( ( c e. _V /\ .x. e. _V /\ a e. _V ) -> ( c .x. a ) e. _V )
171	128, 80, 81, 170	mp3an 1337	. . . . . . 7 |- ( c .x. a ) e. _V
172	171	a1i 9	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( c .x. a ) e. _V )
173	117, 168, 121, 169, 172	ovmpod 6004	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
174	165, 173	oveq12d 5895	. . . 4 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( ( a .* b ) .+ ( a .* c ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
175	174	adantl 277	. . 3 |- ( ( F e. CRing /\ ( a e. K /\ b e. V /\ c e. V ) ) -> ( ( a .* b ) .+ ( a .* c ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
176	161, 175	eqtr4d 2213	. 2 |- ( ( F e. CRing /\ ( a e. K /\ b e. V /\ c e. V ) ) -> ( a .* ( b .+ c ) ) = ( ( a .* b ) .+ ( a .* c ) ) )
177		simpl3 1002	. . . . . . . . 9 |- ( ( ( ( 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 ) ) )
178	177	2ralimi 2541	. . . . . . . 8 |- ( 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 ) ) )
179	178	2ralimi 2541	. . . . . . 7 |- ( 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 ) ) )
180		ralrot3 2642	. . . . . . . 8 |- ( 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 ) ) )
181		r19.3rmv 3515	. . . . . . . . . . 11 |- ( E. j j 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. 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 ) ) ) )
182	101, 181	ax-mp 5	. . . . . . . . . 10 |- ( A. q e. K A. r e. K 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 ) ) )
183	182	biimpri 133	. . . . . . . . 9 |- ( 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 ) ) )
184		oveq1 5884	. . . . . . . . . . . 12 |- ( q = a -> ( q .+^ r ) = ( a .+^ r ) )
185	184	oveq2d 5893	. . . . . . . . . . 11 |- ( q = a -> ( w .x. ( q .+^ r ) ) = ( w .x. ( a .+^ r ) ) )
186		oveq2 5885	. . . . . . . . . . . 12 |- ( q = a -> ( w .x. q ) = ( w .x. a ) )
187	186	oveq1d 5892	. . . . . . . . . . 11 |- ( q = a -> ( ( w .x. q ) .+ ( w .x. r ) ) = ( ( w .x. a ) .+ ( w .x. r ) ) )
188	185, 187	eqeq12d 2192	. . . . . . . . . 10 |- ( q = a -> ( ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) <-> ( w .x. ( a .+^ r ) ) = ( ( w .x. a ) .+ ( w .x. r ) ) ) )
189		oveq2 5885	. . . . . . . . . . . 12 |- ( r = b -> ( a .+^ r ) = ( a .+^ b ) )
190	189	oveq2d 5893	. . . . . . . . . . 11 |- ( r = b -> ( w .x. ( a .+^ r ) ) = ( w .x. ( a .+^ b ) ) )
191		oveq2 5885	. . . . . . . . . . . 12 |- ( r = b -> ( w .x. r ) = ( w .x. b ) )
192	191	oveq2d 5893	. . . . . . . . . . 11 |- ( r = b -> ( ( w .x. a ) .+ ( w .x. r ) ) = ( ( w .x. a ) .+ ( w .x. b ) ) )
193	190, 192	eqeq12d 2192	. . . . . . . . . 10 |- ( r = b -> ( ( w .x. ( a .+^ r ) ) = ( ( w .x. a ) .+ ( w .x. r ) ) <-> ( w .x. ( a .+^ b ) ) = ( ( w .x. a ) .+ ( w .x. b ) ) ) )
194		oveq1 5884	. . . . . . . . . . 11 |- ( w = c -> ( w .x. ( a .+^ b ) ) = ( c .x. ( a .+^ b ) ) )
195		oveq1 5884	. . . . . . . . . . . 12 |- ( w = c -> ( w .x. a ) = ( c .x. a ) )
196		oveq1 5884	. . . . . . . . . . . 12 |- ( w = c -> ( w .x. b ) = ( c .x. b ) )
197	195, 196	oveq12d 5895	. . . . . . . . . . 11 |- ( w = c -> ( ( w .x. a ) .+ ( w .x. b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) )
198	194, 197	eqeq12d 2192	. . . . . . . . . 10 |- ( w = c -> ( ( w .x. ( a .+^ b ) ) = ( ( w .x. a ) .+ ( w .x. b ) ) <-> ( c .x. ( a .+^ b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) ) )
199	188, 193, 198	rspc3v 2859	. . . . . . . . 9 |- ( ( 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 ) ) ) )
200	183, 199	syl5com 29	. . . . . . . 8 |- ( 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 ) ) ) )
201	180, 200	sylbi 121	. . . . . . 7 |- ( 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 ) ) ) )
202	179, 201	syl 14	. . . . . 6 |- ( 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 ) ) ) )
203	202	3ad2ant3 1020	. . . . 5 |- ( ( 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 ) ) ) )
204	2, 203	ax-mp 5	. . . 4 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( a .+^ b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) )
205	17	a1i 9	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
206		oveq12 5886	. . . . . . 7 |- ( ( v = c /\ s = ( a .+^ b ) ) -> ( v .x. s ) = ( c .x. ( a .+^ b ) ) )
207	206	ancoms 268	. . . . . 6 |- ( ( s = ( a .+^ b ) /\ v = c ) -> ( v .x. s ) = ( c .x. ( a .+^ b ) ) )
208	207	adantl 277	. . . . 5 |- ( ( ( a e. K /\ b e. K /\ c e. V ) /\ ( s = ( a .+^ b ) /\ v = c ) ) -> ( v .x. s ) = ( c .x. ( a .+^ b ) ) )
209		ringgrp 13189	. . . . . . . . 9 |- ( F e. Ring -> F e. Grp )
210	4, 57	grpcl 12890	. . . . . . . . . 10 |- ( ( F e. Grp /\ a e. K /\ b e. K ) -> ( a .+^ b ) e. K )
211	210	3expib 1206	. . . . . . . . 9 |- ( F e. Grp -> ( ( a e. K /\ b e. K ) -> ( a .+^ b ) e. K ) )
212	209, 211	syl 14	. . . . . . . 8 |- ( F e. Ring -> ( ( a e. K /\ b e. K ) -> ( a .+^ b ) e. K ) )
213	212	3ad2ant2 1019	. . . . . . 7 |- ( ( 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 ) )
214	2, 213	ax-mp 5	. . . . . 6 |- ( ( a e. K /\ b e. K ) -> ( a .+^ b ) e. K )
215	214	3adant3 1017	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .+^ b ) e. K )
216		simp3 999	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> c e. V )
217	33	slotex 12491	. . . . . . . . . 10 |- ( F e. Ring -> ( +g ` F ) e. _V )
218	6, 217	ax-mp 5	. . . . . . . . 9 |- ( +g ` F ) e. _V
219	57, 218	eqeltri 2250	. . . . . . . 8 |- .+^ e. _V
220		ovexg 5911	. . . . . . . 8 |- ( ( a e. _V /\ .+^ e. _V /\ b e. _V ) -> ( a .+^ b ) e. _V )
221	81, 219, 76, 220	mp3an 1337	. . . . . . 7 |- ( a .+^ b ) e. _V
222		ovexg 5911	. . . . . . 7 |- ( ( c e. _V /\ .x. e. _V /\ ( a .+^ b ) e. _V ) -> ( c .x. ( a .+^ b ) ) e. _V )
223	128, 80, 221, 222	mp3an 1337	. . . . . 6 |- ( c .x. ( a .+^ b ) ) e. _V
224	223	a1i 9	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( a .+^ b ) ) e. _V )
225	205, 208, 215, 216, 224	ovmpod 6004	. . . 4 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( a .+^ b ) .* c ) = ( c .x. ( a .+^ b ) ) )
226	167	adantl 277	. . . . . 6 |- ( ( ( a e. K /\ b e. K /\ c e. V ) /\ ( s = a /\ v = c ) ) -> ( v .x. s ) = ( c .x. a ) )
227		simp1 997	. . . . . 6 |- ( ( a e. K /\ b e. K /\ c e. V ) -> a e. K )
228	171	a1i 9	. . . . . 6 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. a ) e. _V )
229	205, 226, 227, 216, 228	ovmpod 6004	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
230		oveq12 5886	. . . . . . . 8 |- ( ( v = c /\ s = b ) -> ( v .x. s ) = ( c .x. b ) )
231	230	ancoms 268	. . . . . . 7 |- ( ( s = b /\ v = c ) -> ( v .x. s ) = ( c .x. b ) )
232	231	adantl 277	. . . . . 6 |- ( ( ( a e. K /\ b e. K /\ c e. V ) /\ ( s = b /\ v = c ) ) -> ( v .x. s ) = ( c .x. b ) )
233		simp2 998	. . . . . 6 |- ( ( a e. K /\ b e. K /\ c e. V ) -> b e. K )
234		ovexg 5911	. . . . . . . 8 |- ( ( c e. _V /\ .x. e. _V /\ b e. _V ) -> ( c .x. b ) e. _V )
235	128, 80, 76, 234	mp3an 1337	. . . . . . 7 |- ( c .x. b ) e. _V
236	235	a1i 9	. . . . . 6 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. b ) e. _V )
237	205, 232, 233, 216, 236	ovmpod 6004	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( b .* c ) = ( c .x. b ) )
238	229, 237	oveq12d 5895	. . . 4 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( a .* c ) .+ ( b .* c ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) )
239	204, 225, 238	3eqtr4d 2220	. . 3 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( a .+^ b ) .* c ) = ( ( a .* c ) .+ ( b .* c ) ) )
240	239	adantl 277	. 2 |- ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( ( a .+^ b ) .* c ) = ( ( a .* c ) .+ ( b .* c ) ) )
241	1, 38, 77, 47, 4, 57, 59, 61, 2, 17, 28	rmodislmodlem 13445	. 2 |- ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( ( a .X. b ) .* c ) = ( a .* ( b .* c ) ) )
242	17	a1i 9	. . . 4 |- ( ( F e. CRing /\ a e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
243		oveq12 5886	. . . . . 6 |- ( ( v = a /\ s = .1. ) -> ( v .x. s ) = ( a .x. .1. ) )
244	243	ancoms 268	. . . . 5 |- ( ( s = .1. /\ v = a ) -> ( v .x. s ) = ( a .x. .1. ) )
245	244	adantl 277	. . . 4 |- ( ( ( F e. CRing /\ a e. V ) /\ ( s = .1. /\ v = a ) ) -> ( v .x. s ) = ( a .x. .1. ) )
246	63, 89	syl 14	. . . . 5 |- ( F e. CRing -> .1. e. K )
247	246	adantr 276	. . . 4 |- ( ( F e. CRing /\ a e. V ) -> .1. e. K )
248		simpr 110	. . . 4 |- ( ( F e. CRing /\ a e. V ) -> a e. V )
249	6, 89	ax-mp 5	. . . . . 6 |- .1. e. K
250		ovexg 5911	. . . . . 6 |- ( ( a e. _V /\ .x. e. _V /\ .1. e. K ) -> ( a .x. .1. ) e. _V )
251	81, 80, 249, 250	mp3an 1337	. . . . 5 |- ( a .x. .1. ) e. _V
252	251	a1i 9	. . . 4 |- ( ( F e. CRing /\ a e. V ) -> ( a .x. .1. ) e. _V )
253	242, 245, 247, 248, 252	ovmpod 6004	. . 3 |- ( ( F e. CRing /\ a e. V ) -> ( .1. .* a ) = ( a .x. .1. ) )
254		simprr 531	. . . . . . . 8 |- ( ( ( ( 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 )
255	254	2ralimi 2541	. . . . . . 7 |- ( 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 )
256	255	2ralimi 2541	. . . . . 6 |- ( 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 )
257		r19.3rmv 3515	. . . . . . . 8 |- ( E. j j e. K -> ( A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w <-> A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w ) )
258	92, 257	ax-mp 5	. . . . . . 7 |- ( A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w <-> A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w )
259	258	biimpri 133	. . . . . 6 |- ( 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 )
260		r19.3rmv 3515	. . . . . . . 8 |- ( E. j j 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 ) )
261	92, 260	ax-mp 5	. . . . . . 7 |- ( 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 )
262		r19.3rmv 3515	. . . . . . . . . 10 |- ( E. j j e. V -> ( A. w e. V ( w .x. .1. ) = w <-> A. x e. V A. w e. V ( w .x. .1. ) = w ) )
263	101, 262	ax-mp 5	. . . . . . . . 9 |- ( A. w e. V ( w .x. .1. ) = w <-> A. x e. V A. w e. V ( w .x. .1. ) = w )
264	263	biimpri 133	. . . . . . . 8 |- ( A. x e. V A. w e. V ( w .x. .1. ) = w -> A. w e. V ( w .x. .1. ) = w )
265		oveq1 5884	. . . . . . . . . . 11 |- ( w = a -> ( w .x. .1. ) = ( a .x. .1. ) )
266		id 19	. . . . . . . . . . 11 |- ( w = a -> w = a )
267	265, 266	eqeq12d 2192	. . . . . . . . . 10 |- ( w = a -> ( ( w .x. .1. ) = w <-> ( a .x. .1. ) = a ) )
268	267	rspcv 2839	. . . . . . . . 9 |- ( a e. V -> ( A. w e. V ( w .x. .1. ) = w -> ( a .x. .1. ) = a ) )
269	268	adantl 277	. . . . . . . 8 |- ( ( F e. CRing /\ a e. V ) -> ( A. w e. V ( w .x. .1. ) = w -> ( a .x. .1. ) = a ) )
270	264, 269	syl5com 29	. . . . . . 7 |- ( A. x e. V A. w e. V ( w .x. .1. ) = w -> ( ( F e. CRing /\ a e. V ) -> ( a .x. .1. ) = a ) )
271	261, 270	sylbir 135	. . . . . 6 |- ( 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 ) )
272	256, 259, 271	3syl 17	. . . . 5 |- ( 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 ) )
273	272	3ad2ant3 1020	. . . 4 |- ( ( 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 ) )
274	2, 273	ax-mp 5	. . 3 |- ( ( F e. CRing /\ a e. V ) -> ( a .x. .1. ) = a )
275	253, 274	eqtrd 2210	. 2 |- ( ( F e. CRing /\ a e. V ) -> ( .1. .* a ) = a )
276	32, 41, 50, 55, 56, 58, 60, 62, 63, 69, 116, 176, 240, 241, 275	islmodd 13388	1 |- ( F e. CRing -> L e. LMod )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 978   = wceq 1353   E.wex 1492   e. wcel 2148   A.wral 2455   _Vcvv 2739   <.cop 3597   Fn wfn 5213   ` cfv 5218  (class class class)co 5877   e. cmpo 5879   NNcn 8921   ndxcnx 12461   sSet csts 12462  Slot cslot 12463   Basecbs 12464   +g cplusg 12538   .rcmulr 12539  Scalarcsca 12541   .scvsca 12542   0gc0g 12710   Grpcgrp 12882   1rcur 13147   Ringcrg 13184   CRingccrg 13185   LModclmod 13382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-cnex 7904  ax-resscn 7905  ax-1cn 7906  ax-1re 7907  ax-icn 7908  ax-addcl 7909  ax-addrcl 7910  ax-mulcl 7911  ax-addcom 7913  ax-addass 7915  ax-i2m1 7918  ax-0lt1 7919  ax-0id 7921  ax-rnegex 7922  ax-pre-ltirr 7925  ax-pre-lttrn 7927  ax-pre-ltadd 7929

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-riota 5833  df-ov 5880  df-oprab 5881  df-mpo 5882  df-1st 6143  df-2nd 6144  df-pnf 7996  df-mnf 7997  df-ltxr 7999  df-inn 8922  df-2 8980  df-3 8981  df-4 8982  df-5 8983  df-6 8984  df-ndx 12467  df-slot 12468  df-base 12470  df-sets 12471  df-plusg 12551  df-mulr 12552  df-sca 12554  df-vsca 12555  df-0g 12712  df-mgm 12780  df-sgrp 12813  df-mnd 12823  df-grp 12885  df-cmn 13095  df-mgp 13136  df-ur 13148  df-ring 13186  df-cring 13187  df-lmod 13384

This theorem is referenced by: (None)