Theorem rmodislmod 13847

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 13785 of a left module, see also islmod 13787. (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 1008	. . . . . 6 |- R e. Grp
4		rmodislmod.k	. . . . . . . 8 |- K = ( Base ` F )
5		basfn 12676	. . . . . . . . 9 |- Base Fn _V
6	2	simp2i 1009	. . . . . . . . . 10 |- F e. Ring
7	6	elexi 2772	. . . . . . . . 9 |- F e. _V
8		funfvex 5571	. . . . . . . . . 10 |- ( ( Fun Base /\ F e. dom Base ) -> ( Base ` F ) e. _V )
9	8	funfni 5354	. . . . . . . . 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 2266	. . . . . . 7 |- K e. _V
12	3	elexi 2772	. . . . . . . . 9 |- R e. _V
13		funfvex 5571	. . . . . . . . . 10 |- ( ( Fun Base /\ R e. dom Base ) -> ( Base ` R ) e. _V )
14	13	funfni 5354	. . . . . . . . 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 2266	. . . . . . 7 |- V e. _V
17		rmodislmod.m	. . . . . . . 8 |- .* = ( s e. K , v e. V |-> ( v .x. s ) )
18	17	mpoexg 6264	. . . . . . 7 |- ( ( K e. _V /\ V e. _V ) -> .* e. _V )
19	11, 16, 18	mp2an 426	. . . . . 6 |- .* e. _V
20		baseslid 12675	. . . . . . 7 |- ( Base = Slot ( Base ` ndx ) /\ ( Base ` ndx ) e. NN )
21		vscandxnbasendx 12776	. . . . . . . 8 |- ( .s ` ndx ) =/= ( Base ` ndx )
22	21	necomi 2449	. . . . . . 7 |- ( Base ` ndx ) =/= ( .s ` ndx )
23		vscaslid 12780	. . . . . . . 8 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
24	23	simpri 113	. . . . . . 7 |- ( .s ` ndx ) e. NN
25	20, 22, 24	setsslnid 12670	. . . . . 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 2214	. . . 4 |- V = ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
28		rmodislmod.l	. . . . . 6 |- L = ( R sSet <. ( .s ` ndx ) , .* >. )
29	28	eqcomi 2197	. . . . 5 |- ( R sSet <. ( .s ` ndx ) , .* >. ) = L
30	29	fveq2i 5557	. . . 4 |- ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) = ( Base ` L )
31	27, 30	eqtri 2214	. . 3 |- V = ( Base ` L )
32	31	a1i 9	. 2 |- ( F e. CRing -> V = ( Base ` L ) )
33		plusgslid 12730	. . . . . 6 |- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )
34		vscandxnplusgndx 12777	. . . . . . 7 |- ( .s ` ndx ) =/= ( +g ` ndx )
35	34	necomi 2449	. . . . . 6 |- ( +g ` ndx ) =/= ( .s ` ndx )
36	33, 35, 24	setsslnid 12670	. . . . 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 5557	. . . 4 |- ( +g ` L ) = ( +g ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
40	37, 38, 39	3eqtr4i 2224	. . 3 |- .+ = ( +g ` L )
41	40	a1i 9	. 2 |- ( F e. CRing -> .+ = ( +g ` L ) )
42		scaslid 12770	. . . . . 6 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
43		vscandxnscandx 12779	. . . . . . 7 |- ( .s ` ndx ) =/= (Scalar ` ndx )
44	43	necomi 2449	. . . . . 6 |- (Scalar ` ndx ) =/= ( .s ` ndx )
45	42, 44, 24	setsslnid 12670	. . . . 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 5557	. . . 4 |- (Scalar ` L ) = (Scalar ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
49	46, 47, 48	3eqtr4i 2224	. . 3 |- F = (Scalar ` L )
50	49	a1i 9	. 2 |- ( F e. CRing -> F = (Scalar ` L ) )
51	23	setsslid 12669	. . . . 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 5557	. . . 4 |- ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) = ( .s ` L )
54	52, 53	eqtri 2214	. . 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 13504	. 2 |- ( F e. CRing -> F e. Ring )
64	1	eqcomi 2197	. . . . . 6 |- ( Base ` R ) = V
65	64, 31	eqtri 2214	. . . . 5 |- ( Base ` R ) = ( Base ` L )
66	37, 39	eqtr4i 2217	. . . . 5 |- ( +g ` R ) = ( +g ` L )
67	65, 66	grpprop 13090	. . . 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 5927	. . . . . 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 1000	. . . 4 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> a e. K )
75		simp3 1001	. . . 4 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> b e. V )
76		vex 2763	. . . . . 6 |- b e. _V
77		rmodislmod.s	. . . . . . 7 |- .x. = ( .s ` R )
78	23	slotex 12645	. . . . . . . 8 |- ( R e. Grp -> ( .s ` R ) e. _V )
79	3, 78	ax-mp 5	. . . . . . 7 |- ( .s ` R ) e. _V
80	77, 79	eqeltri 2266	. . . . . 6 |- .x. e. _V
81		vex 2763	. . . . . 6 |- a e. _V
82		ovexg 5952	. . . . . 6 |- ( ( b e. _V /\ .x. e. _V /\ a e. _V ) -> ( b .x. a ) e. _V )
83	76, 80, 81, 82	mp3an 1348	. . . . 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 6046	. . 3 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( a .* b ) = ( b .x. a ) )
86		simpl1 1002	. . . . . . . 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 2558	. . . . . . 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 2558	. . . . . 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 13516	. . . . . . . . . 10 |- ( F e. Ring -> .1. e. K )
90		elex2 2776	. . . . . . . . . 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 3537	. . . . . . . 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 2657	. . . . . . 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 2193	. . . . . . . . . . . . 13 |- ( 0g ` R ) = ( 0g ` R )
98	1, 97	grpidcl 13101	. . . . . . . . . . . 12 |- ( R e. Grp -> ( 0g ` R ) e. V )
99	3, 98	ax-mp 5	. . . . . . . . . . 11 |- ( 0g ` R ) e. V
100		elex2 2776	. . . . . . . . . . 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 3537	. . . . . . . . . 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 5926	. . . . . . . . . . 11 |- ( r = a -> ( w .x. r ) = ( w .x. a ) )
106	105	eleq1d 2262	. . . . . . . . . 10 |- ( r = a -> ( ( w .x. r ) e. V <-> ( w .x. a ) e. V ) )
107		oveq1 5925	. . . . . . . . . . 11 |- ( w = b -> ( w .x. a ) = ( b .x. a ) )
108	107	eleq1d 2262	. . . . . . . . . 10 |- ( w = b -> ( ( w .x. a ) e. V <-> ( b .x. a ) e. V ) )
109	106, 108	rspc2v 2877	. . . . . . . . 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 1017	. . . . . . . 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 1022	. . . 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 2270	. 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 5927	. . . . . . . 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 999	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> a e. K )
122	1, 38	grpcl 13080	. . . . . . . 8 |- ( ( R e. Grp /\ b e. V /\ c e. V ) -> ( b .+ c ) e. V )
123	3, 122	mp3an1 1335	. . . . . . 7 |- ( ( b e. V /\ c e. V ) -> ( b .+ c ) e. V )
124	123	3adant1 1017	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( b .+ c ) e. V )
125	33	slotex 12645	. . . . . . . . . . 11 |- ( R e. Grp -> ( +g ` R ) e. _V )
126	3, 125	ax-mp 5	. . . . . . . . . 10 |- ( +g ` R ) e. _V
127	38, 126	eqeltri 2266	. . . . . . . . 9 |- .+ e. _V
128		vex 2763	. . . . . . . . 9 |- c e. _V
129		ovexg 5952	. . . . . . . . 9 |- ( ( b e. _V /\ .+ e. _V /\ c e. _V ) -> ( b .+ c ) e. _V )
130	76, 127, 128, 129	mp3an 1348	. . . . . . . 8 |- ( b .+ c ) e. _V
131		ovexg 5952	. . . . . . . 8 |- ( ( ( b .+ c ) e. _V /\ .x. e. _V /\ a e. _V ) -> ( ( b .+ c ) .x. a ) e. _V )
132	130, 80, 81, 131	mp3an 1348	. . . . . . 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 6046	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* ( b .+ c ) ) = ( ( b .+ c ) .x. a ) )
135		simpl2 1003	. . . . . . . . . 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 2558	. . . . . . . . 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 2558	. . . . . . . 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 3537	. . . . . . . . . . 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 5926	. . . . . . . . . . . 12 |- ( r = a -> ( ( w .+ x ) .x. r ) = ( ( w .+ x ) .x. a ) )
142		oveq2 5926	. . . . . . . . . . . . 13 |- ( r = a -> ( x .x. r ) = ( x .x. a ) )
143	105, 142	oveq12d 5936	. . . . . . . . . . . 12 |- ( r = a -> ( ( w .x. r ) .+ ( x .x. r ) ) = ( ( w .x. a ) .+ ( x .x. a ) ) )
144	141, 143	eqeq12d 2208	. . . . . . . . . . 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 5926	. . . . . . . . . . . . 13 |- ( x = c -> ( w .+ x ) = ( w .+ c ) )
146	145	oveq1d 5933	. . . . . . . . . . . 12 |- ( x = c -> ( ( w .+ x ) .x. a ) = ( ( w .+ c ) .x. a ) )
147		oveq1 5925	. . . . . . . . . . . . 13 |- ( x = c -> ( x .x. a ) = ( c .x. a ) )
148	147	oveq2d 5934	. . . . . . . . . . . 12 |- ( x = c -> ( ( w .x. a ) .+ ( x .x. a ) ) = ( ( w .x. a ) .+ ( c .x. a ) ) )
149	146, 148	eqeq12d 2208	. . . . . . . . . . 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 5925	. . . . . . . . . . . . 13 |- ( w = b -> ( w .+ c ) = ( b .+ c ) )
151	150	oveq1d 5933	. . . . . . . . . . . 12 |- ( w = b -> ( ( w .+ c ) .x. a ) = ( ( b .+ c ) .x. a ) )
152	107	oveq1d 5933	. . . . . . . . . . . 12 |- ( w = b -> ( ( w .x. a ) .+ ( c .x. a ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
153	151, 152	eqeq12d 2208	. . . . . . . . . . 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 2880	. . . . . . . . . 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 1211	. . . . . . . . 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 1022	. . . . . 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 2226	. . . 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 1000	. . . . . 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 6046	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* b ) = ( b .x. a ) )
166		oveq12 5927	. . . . . . . 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 1001	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> c e. V )
170		ovexg 5952	. . . . . . . 8 |- ( ( c e. _V /\ .x. e. _V /\ a e. _V ) -> ( c .x. a ) e. _V )
171	128, 80, 81, 170	mp3an 1348	. . . . . . 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 6046	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
174	165, 173	oveq12d 5936	. . . 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 2229	. 2 |- ( ( F e. CRing /\ ( a e. K /\ b e. V /\ c e. V ) ) -> ( a .* ( b .+ c ) ) = ( ( a .* b ) .+ ( a .* c ) ) )
177		simpl3 1004	. . . . . . . . 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 2558	. . . . . . . 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 2558	. . . . . . 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 2659	. . . . . . . 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 3537	. . . . . . . . . . 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 5925	. . . . . . . . . . . 12 |- ( q = a -> ( q .+^ r ) = ( a .+^ r ) )
185	184	oveq2d 5934	. . . . . . . . . . 11 |- ( q = a -> ( w .x. ( q .+^ r ) ) = ( w .x. ( a .+^ r ) ) )
186		oveq2 5926	. . . . . . . . . . . 12 |- ( q = a -> ( w .x. q ) = ( w .x. a ) )
187	186	oveq1d 5933	. . . . . . . . . . 11 |- ( q = a -> ( ( w .x. q ) .+ ( w .x. r ) ) = ( ( w .x. a ) .+ ( w .x. r ) ) )
188	185, 187	eqeq12d 2208	. . . . . . . . . 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 5926	. . . . . . . . . . . 12 |- ( r = b -> ( a .+^ r ) = ( a .+^ b ) )
190	189	oveq2d 5934	. . . . . . . . . . 11 |- ( r = b -> ( w .x. ( a .+^ r ) ) = ( w .x. ( a .+^ b ) ) )
191		oveq2 5926	. . . . . . . . . . . 12 |- ( r = b -> ( w .x. r ) = ( w .x. b ) )
192	191	oveq2d 5934	. . . . . . . . . . 11 |- ( r = b -> ( ( w .x. a ) .+ ( w .x. r ) ) = ( ( w .x. a ) .+ ( w .x. b ) ) )
193	190, 192	eqeq12d 2208	. . . . . . . . . 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 5925	. . . . . . . . . . 11 |- ( w = c -> ( w .x. ( a .+^ b ) ) = ( c .x. ( a .+^ b ) ) )
195		oveq1 5925	. . . . . . . . . . . 12 |- ( w = c -> ( w .x. a ) = ( c .x. a ) )
196		oveq1 5925	. . . . . . . . . . . 12 |- ( w = c -> ( w .x. b ) = ( c .x. b ) )
197	195, 196	oveq12d 5936	. . . . . . . . . . 11 |- ( w = c -> ( ( w .x. a ) .+ ( w .x. b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) )
198	194, 197	eqeq12d 2208	. . . . . . . . . 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 2880	. . . . . . . . 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 1022	. . . . 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 5927	. . . . . . 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 13497	. . . . . . . . 9 |- ( F e. Ring -> F e. Grp )
210	4, 57	grpcl 13080	. . . . . . . . . 10 |- ( ( F e. Grp /\ a e. K /\ b e. K ) -> ( a .+^ b ) e. K )
211	210	3expib 1208	. . . . . . . . 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 1021	. . . . . . 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 1019	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .+^ b ) e. K )
216		simp3 1001	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> c e. V )
217	33	slotex 12645	. . . . . . . . . 10 |- ( F e. Ring -> ( +g ` F ) e. _V )
218	6, 217	ax-mp 5	. . . . . . . . 9 |- ( +g ` F ) e. _V
219	57, 218	eqeltri 2266	. . . . . . . 8 |- .+^ e. _V
220		ovexg 5952	. . . . . . . 8 |- ( ( a e. _V /\ .+^ e. _V /\ b e. _V ) -> ( a .+^ b ) e. _V )
221	81, 219, 76, 220	mp3an 1348	. . . . . . 7 |- ( a .+^ b ) e. _V
222		ovexg 5952	. . . . . . 7 |- ( ( c e. _V /\ .x. e. _V /\ ( a .+^ b ) e. _V ) -> ( c .x. ( a .+^ b ) ) e. _V )
223	128, 80, 221, 222	mp3an 1348	. . . . . 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 6046	. . . 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 999	. . . . . 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 6046	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
230		oveq12 5927	. . . . . . . 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 1000	. . . . . 6 |- ( ( a e. K /\ b e. K /\ c e. V ) -> b e. K )
234		ovexg 5952	. . . . . . . 8 |- ( ( c e. _V /\ .x. e. _V /\ b e. _V ) -> ( c .x. b ) e. _V )
235	128, 80, 76, 234	mp3an 1348	. . . . . . 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 6046	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( b .* c ) = ( c .x. b ) )
238	229, 237	oveq12d 5936	. . . 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 2236	. . 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 13846	. 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 5927	. . . . . 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 5952	. . . . . 6 |- ( ( a e. _V /\ .x. e. _V /\ .1. e. K ) -> ( a .x. .1. ) e. _V )
251	81, 80, 249, 250	mp3an 1348	. . . . 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 6046	. . 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 2558	. . . . . . 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 2558	. . . . . 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 3537	. . . . . . . 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 3537	. . . . . . . 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 3537	. . . . . . . . . 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 5925	. . . . . . . . . . 11 |- ( w = a -> ( w .x. .1. ) = ( a .x. .1. ) )
266		id 19	. . . . . . . . . . 11 |- ( w = a -> w = a )
267	265, 266	eqeq12d 2208	. . . . . . . . . 10 |- ( w = a -> ( ( w .x. .1. ) = w <-> ( a .x. .1. ) = a ) )
268	267	rspcv 2860	. . . . . . . . 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 1022	. . . 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 2226	. 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 13789	1 |- ( F e. CRing -> L e. LMod )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 980   = wceq 1364   E.wex 1503   e. wcel 2164   A.wral 2472   _Vcvv 2760   <.cop 3621   Fn wfn 5249   ` cfv 5254  (class class class)co 5918   e. cmpo 5920   NNcn 8982   ndxcnx 12615   sSet csts 12616  Slot cslot 12617   Basecbs 12618   +g cplusg 12695   .rcmulr 12696  Scalarcsca 12698   .scvsca 12699   0gc0g 12867   Grpcgrp 13072   1rcur 13455   Ringcrg 13492   CRingccrg 13493   LModclmod 13783

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-addcom 7972  ax-addass 7974  ax-i2m1 7977  ax-0lt1 7978  ax-0id 7980  ax-rnegex 7981  ax-pre-ltirr 7984  ax-pre-lttrn 7986  ax-pre-ltadd 7988

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-1st 6193  df-2nd 6194  df-pnf 8056  df-mnf 8057  df-ltxr 8059  df-inn 8983  df-2 9041  df-3 9042  df-4 9043  df-5 9044  df-6 9045  df-ndx 12621  df-slot 12622  df-base 12624  df-sets 12625  df-plusg 12708  df-mulr 12709  df-sca 12711  df-vsca 12712  df-0g 12869  df-mgm 12939  df-sgrp 12985  df-mnd 12998  df-grp 13075  df-cmn 13356  df-mgp 13417  df-ur 13456  df-ring 13494  df-cring 13495  df-lmod 13785

This theorem is referenced by: (None)