Theorem rmodislmod 13907

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 13845 of a left module, see also islmod 13847. (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 12736	. . . . . . . . 9 |- Base Fn _V
6	2	simp2i 1009	. . . . . . . . . 10 |- F e. Ring
7	6	elexi 2775	. . . . . . . . 9 |- F e. _V
8		funfvex 5575	. . . . . . . . . 10 |- ( ( Fun Base /\ F e. dom Base ) -> ( Base ` F ) e. _V )
9	8	funfni 5358	. . . . . . . . 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 2269	. . . . . . 7 |- K e. _V
12	3	elexi 2775	. . . . . . . . 9 |- R e. _V
13		funfvex 5575	. . . . . . . . . 10 |- ( ( Fun Base /\ R e. dom Base ) -> ( Base ` R ) e. _V )
14	13	funfni 5358	. . . . . . . . 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 2269	. . . . . . 7 |- V e. _V
17		rmodislmod.m	. . . . . . . 8 |- .* = ( s e. K , v e. V |-> ( v .x. s ) )
18	17	mpoexg 6269	. . . . . . 7 |- ( ( K e. _V /\ V e. _V ) -> .* e. _V )
19	11, 16, 18	mp2an 426	. . . . . 6 |- .* e. _V
20		baseslid 12735	. . . . . . 7 |- ( Base = Slot ( Base ` ndx ) /\ ( Base ` ndx ) e. NN )
21		vscandxnbasendx 12836	. . . . . . . 8 |- ( .s ` ndx ) =/= ( Base ` ndx )
22	21	necomi 2452	. . . . . . 7 |- ( Base ` ndx ) =/= ( .s ` ndx )
23		vscaslid 12840	. . . . . . . 8 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
24	23	simpri 113	. . . . . . 7 |- ( .s ` ndx ) e. NN
25	20, 22, 24	setsslnid 12730	. . . . . 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 2217	. . . 4 |- V = ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
28		rmodislmod.l	. . . . . 6 |- L = ( R sSet <. ( .s ` ndx ) , .* >. )
29	28	eqcomi 2200	. . . . 5 |- ( R sSet <. ( .s ` ndx ) , .* >. ) = L
30	29	fveq2i 5561	. . . 4 |- ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) = ( Base ` L )
31	27, 30	eqtri 2217	. . 3 |- V = ( Base ` L )
32	31	a1i 9	. 2 |- ( F e. CRing -> V = ( Base ` L ) )
33		plusgslid 12790	. . . . . 6 |- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )
34		vscandxnplusgndx 12837	. . . . . . 7 |- ( .s ` ndx ) =/= ( +g ` ndx )
35	34	necomi 2452	. . . . . 6 |- ( +g ` ndx ) =/= ( .s ` ndx )
36	33, 35, 24	setsslnid 12730	. . . . 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 5561	. . . 4 |- ( +g ` L ) = ( +g ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
40	37, 38, 39	3eqtr4i 2227	. . 3 |- .+ = ( +g ` L )
41	40	a1i 9	. 2 |- ( F e. CRing -> .+ = ( +g ` L ) )
42		scaslid 12830	. . . . . 6 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
43		vscandxnscandx 12839	. . . . . . 7 |- ( .s ` ndx ) =/= (Scalar ` ndx )
44	43	necomi 2452	. . . . . 6 |- (Scalar ` ndx ) =/= ( .s ` ndx )
45	42, 44, 24	setsslnid 12730	. . . . 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 5561	. . . 4 |- (Scalar ` L ) = (Scalar ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
49	46, 47, 48	3eqtr4i 2227	. . 3 |- F = (Scalar ` L )
50	49	a1i 9	. 2 |- ( F e. CRing -> F = (Scalar ` L ) )
51	23	setsslid 12729	. . . . 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 5561	. . . 4 |- ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) = ( .s ` L )
54	52, 53	eqtri 2217	. . 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 13564	. 2 |- ( F e. CRing -> F e. Ring )
64	1	eqcomi 2200	. . . . . 6 |- ( Base ` R ) = V
65	64, 31	eqtri 2217	. . . . 5 |- ( Base ` R ) = ( Base ` L )
66	37, 39	eqtr4i 2220	. . . . 5 |- ( +g ` R ) = ( +g ` L )
67	65, 66	grpprop 13150	. . . 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 5931	. . . . . 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 2766	. . . . . 6 |- b e. _V
77		rmodislmod.s	. . . . . . 7 |- .x. = ( .s ` R )
78	23	slotex 12705	. . . . . . . 8 |- ( R e. Grp -> ( .s ` R ) e. _V )
79	3, 78	ax-mp 5	. . . . . . 7 |- ( .s ` R ) e. _V
80	77, 79	eqeltri 2269	. . . . . 6 |- .x. e. _V
81		vex 2766	. . . . . 6 |- a e. _V
82		ovexg 5956	. . . . . 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 6050	. . 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 2561	. . . . . . 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 2561	. . . . . 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 13576	. . . . . . . . . 10 |- ( F e. Ring -> .1. e. K )
90		elex2 2779	. . . . . . . . . 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 3541	. . . . . . . 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 2660	. . . . . . 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 2196	. . . . . . . . . . . . 13 |- ( 0g ` R ) = ( 0g ` R )
98	1, 97	grpidcl 13161	. . . . . . . . . . . 12 |- ( R e. Grp -> ( 0g ` R ) e. V )
99	3, 98	ax-mp 5	. . . . . . . . . . 11 |- ( 0g ` R ) e. V
100		elex2 2779	. . . . . . . . . . 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 3541	. . . . . . . . . 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 5930	. . . . . . . . . . 11 |- ( r = a -> ( w .x. r ) = ( w .x. a ) )
106	105	eleq1d 2265	. . . . . . . . . 10 |- ( r = a -> ( ( w .x. r ) e. V <-> ( w .x. a ) e. V ) )
107		oveq1 5929	. . . . . . . . . . 11 |- ( w = b -> ( w .x. a ) = ( b .x. a ) )
108	107	eleq1d 2265	. . . . . . . . . 10 |- ( w = b -> ( ( w .x. a ) e. V <-> ( b .x. a ) e. V ) )
109	106, 108	rspc2v 2881	. . . . . . . . 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 2273	. 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 5931	. . . . . . . 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 13140	. . . . . . . 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 12705	. . . . . . . . . . 11 |- ( R e. Grp -> ( +g ` R ) e. _V )
126	3, 125	ax-mp 5	. . . . . . . . . 10 |- ( +g ` R ) e. _V
127	38, 126	eqeltri 2269	. . . . . . . . 9 |- .+ e. _V
128		vex 2766	. . . . . . . . 9 |- c e. _V
129		ovexg 5956	. . . . . . . . 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 5956	. . . . . . . 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 6050	. . . . 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 2561	. . . . . . . . 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 2561	. . . . . . . 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 3541	. . . . . . . . . . 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 5930	. . . . . . . . . . . 12 |- ( r = a -> ( ( w .+ x ) .x. r ) = ( ( w .+ x ) .x. a ) )
142		oveq2 5930	. . . . . . . . . . . . 13 |- ( r = a -> ( x .x. r ) = ( x .x. a ) )
143	105, 142	oveq12d 5940	. . . . . . . . . . . 12 |- ( r = a -> ( ( w .x. r ) .+ ( x .x. r ) ) = ( ( w .x. a ) .+ ( x .x. a ) ) )
144	141, 143	eqeq12d 2211	. . . . . . . . . . 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 5930	. . . . . . . . . . . . 13 |- ( x = c -> ( w .+ x ) = ( w .+ c ) )
146	145	oveq1d 5937	. . . . . . . . . . . 12 |- ( x = c -> ( ( w .+ x ) .x. a ) = ( ( w .+ c ) .x. a ) )
147		oveq1 5929	. . . . . . . . . . . . 13 |- ( x = c -> ( x .x. a ) = ( c .x. a ) )
148	147	oveq2d 5938	. . . . . . . . . . . 12 |- ( x = c -> ( ( w .x. a ) .+ ( x .x. a ) ) = ( ( w .x. a ) .+ ( c .x. a ) ) )
149	146, 148	eqeq12d 2211	. . . . . . . . . . 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 5929	. . . . . . . . . . . . 13 |- ( w = b -> ( w .+ c ) = ( b .+ c ) )
151	150	oveq1d 5937	. . . . . . . . . . . 12 |- ( w = b -> ( ( w .+ c ) .x. a ) = ( ( b .+ c ) .x. a ) )
152	107	oveq1d 5937	. . . . . . . . . . . 12 |- ( w = b -> ( ( w .x. a ) .+ ( c .x. a ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
153	151, 152	eqeq12d 2211	. . . . . . . . . . 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 2884	. . . . . . . . . 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 2229	. . . 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 6050	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* b ) = ( b .x. a ) )
166		oveq12 5931	. . . . . . . 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 5956	. . . . . . . 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 6050	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
174	165, 173	oveq12d 5940	. . . 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 2232	. 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 2561	. . . . . . . 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 2561	. . . . . . 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 2662	. . . . . . . 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 3541	. . . . . . . . . . 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 5929	. . . . . . . . . . . 12 |- ( q = a -> ( q .+^ r ) = ( a .+^ r ) )
185	184	oveq2d 5938	. . . . . . . . . . 11 |- ( q = a -> ( w .x. ( q .+^ r ) ) = ( w .x. ( a .+^ r ) ) )
186		oveq2 5930	. . . . . . . . . . . 12 |- ( q = a -> ( w .x. q ) = ( w .x. a ) )
187	186	oveq1d 5937	. . . . . . . . . . 11 |- ( q = a -> ( ( w .x. q ) .+ ( w .x. r ) ) = ( ( w .x. a ) .+ ( w .x. r ) ) )
188	185, 187	eqeq12d 2211	. . . . . . . . . 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 5930	. . . . . . . . . . . 12 |- ( r = b -> ( a .+^ r ) = ( a .+^ b ) )
190	189	oveq2d 5938	. . . . . . . . . . 11 |- ( r = b -> ( w .x. ( a .+^ r ) ) = ( w .x. ( a .+^ b ) ) )
191		oveq2 5930	. . . . . . . . . . . 12 |- ( r = b -> ( w .x. r ) = ( w .x. b ) )
192	191	oveq2d 5938	. . . . . . . . . . 11 |- ( r = b -> ( ( w .x. a ) .+ ( w .x. r ) ) = ( ( w .x. a ) .+ ( w .x. b ) ) )
193	190, 192	eqeq12d 2211	. . . . . . . . . 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 5929	. . . . . . . . . . 11 |- ( w = c -> ( w .x. ( a .+^ b ) ) = ( c .x. ( a .+^ b ) ) )
195		oveq1 5929	. . . . . . . . . . . 12 |- ( w = c -> ( w .x. a ) = ( c .x. a ) )
196		oveq1 5929	. . . . . . . . . . . 12 |- ( w = c -> ( w .x. b ) = ( c .x. b ) )
197	195, 196	oveq12d 5940	. . . . . . . . . . 11 |- ( w = c -> ( ( w .x. a ) .+ ( w .x. b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) )
198	194, 197	eqeq12d 2211	. . . . . . . . . 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 2884	. . . . . . . . 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 5931	. . . . . . 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 13557	. . . . . . . . 9 |- ( F e. Ring -> F e. Grp )
210	4, 57	grpcl 13140	. . . . . . . . . 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 12705	. . . . . . . . . 10 |- ( F e. Ring -> ( +g ` F ) e. _V )
218	6, 217	ax-mp 5	. . . . . . . . 9 |- ( +g ` F ) e. _V
219	57, 218	eqeltri 2269	. . . . . . . 8 |- .+^ e. _V
220		ovexg 5956	. . . . . . . 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 5956	. . . . . . 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 6050	. . . 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 6050	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
230		oveq12 5931	. . . . . . . 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 5956	. . . . . . . 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 6050	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( b .* c ) = ( c .x. b ) )
238	229, 237	oveq12d 5940	. . . 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 2239	. . 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 13906	. 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 5931	. . . . . 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 5956	. . . . . 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 6050	. . 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 2561	. . . . . . 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 2561	. . . . . 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 3541	. . . . . . . 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 3541	. . . . . . . 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 3541	. . . . . . . . . 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 5929	. . . . . . . . . . 11 |- ( w = a -> ( w .x. .1. ) = ( a .x. .1. ) )
266		id 19	. . . . . . . . . . 11 |- ( w = a -> w = a )
267	265, 266	eqeq12d 2211	. . . . . . . . . 10 |- ( w = a -> ( ( w .x. .1. ) = w <-> ( a .x. .1. ) = a ) )
268	267	rspcv 2864	. . . . . . . . 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 2229	. 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 13849	1 |- ( F e. CRing -> L e. LMod )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 980   = wceq 1364   E.wex 1506   e. wcel 2167   A.wral 2475   _Vcvv 2763   <.cop 3625   Fn wfn 5253   ` cfv 5258  (class class class)co 5922   e. cmpo 5924   NNcn 8990   ndxcnx 12675   sSet csts 12676  Slot cslot 12677   Basecbs 12678   +g cplusg 12755   .rcmulr 12756  Scalarcsca 12758   .scvsca 12759   0gc0g 12927   Grpcgrp 13132   1rcur 13515   Ringcrg 13552   CRingccrg 13553   LModclmod 13843

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-addcom 7979  ax-addass 7981  ax-i2m1 7984  ax-0lt1 7985  ax-0id 7987  ax-rnegex 7988  ax-pre-ltirr 7991  ax-pre-lttrn 7993  ax-pre-ltadd 7995

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rmo 2483  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-id 4328  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-1st 6198  df-2nd 6199  df-pnf 8063  df-mnf 8064  df-ltxr 8066  df-inn 8991  df-2 9049  df-3 9050  df-4 9051  df-5 9052  df-6 9053  df-ndx 12681  df-slot 12682  df-base 12684  df-sets 12685  df-plusg 12768  df-mulr 12769  df-sca 12771  df-vsca 12772  df-0g 12929  df-mgm 12999  df-sgrp 13045  df-mnd 13058  df-grp 13135  df-cmn 13416  df-mgp 13477  df-ur 13516  df-ring 13554  df-cring 13555  df-lmod 13845

This theorem is referenced by: (None)