Theorem rmodislmod 14671

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 14608 of a left module, see also islmod 14610. (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 1037	. . . . . 6 |- R e. Grp
4		rmodislmod.k	. . . . . . . 8 |- K = ( Base ` F )
5		basfn 13394	. . . . . . . . 9 |- Base Fn _V
6	2	simp2i 1038	. . . . . . . . . 10 |- F e. Ring
7	6	elexi 2834	. . . . . . . . 9 |- F e. _V
8		funfvex 5710	. . . . . . . . . 10 |- ( ( Fun Base /\ F e. dom Base ) -> ( Base ` F ) e. _V )
9	8	funfni 5481	. . . . . . . . 9 |- ( ( Base Fn _V /\ F e. _V ) -> ( Base ` F ) e. _V )
10	5, 7, 9	mp2an 430	. . . . . . . 8 |- ( Base ` F ) e. _V
11	4, 10	eqeltri 2311	. . . . . . 7 |- K e. _V
12	3	elexi 2834	. . . . . . . . 9 |- R e. _V
13		funfvex 5710	. . . . . . . . . 10 |- ( ( Fun Base /\ R e. dom Base ) -> ( Base ` R ) e. _V )
14	13	funfni 5481	. . . . . . . . 9 |- ( ( Base Fn _V /\ R e. _V ) -> ( Base ` R ) e. _V )
15	5, 12, 14	mp2an 430	. . . . . . . 8 |- ( Base ` R ) e. _V
16	1, 15	eqeltri 2311	. . . . . . 7 |- V e. _V
17		rmodislmod.m	. . . . . . . 8 |- .* = ( s e. K , v e. V |-> ( v .x. s ) )
18	17	mpoexg 6441	. . . . . . 7 |- ( ( K e. _V /\ V e. _V ) -> .* e. _V )
19	11, 16, 18	mp2an 430	. . . . . 6 |- .* e. _V
20		baseslid 13393	. . . . . . 7 |- ( Base = Slot ( Base ` ndx ) /\ ( Base ` ndx ) e. NN )
21		vscandxnbasendx 13496	. . . . . . . 8 |- ( .s ` ndx ) =/= ( Base ` ndx )
22	21	necomi 2505	. . . . . . 7 |- ( Base ` ndx ) =/= ( .s ` ndx )
23		vscaslid 13500	. . . . . . . 8 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
24	23	simpri 113	. . . . . . 7 |- ( .s ` ndx ) e. NN
25	20, 22, 24	setsslnid 13387	. . . . . 6 |- ( ( R e. Grp /\ .* e. _V ) -> ( Base ` R ) = ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) )
26	3, 19, 25	mp2an 430	. . . . 5 |- ( Base ` R ) = ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
27	1, 26	eqtri 2259	. . . 4 |- V = ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
28		rmodislmod.l	. . . . . 6 |- L = ( R sSet <. ( .s ` ndx ) , .* >. )
29	28	eqcomi 2242	. . . . 5 |- ( R sSet <. ( .s ` ndx ) , .* >. ) = L
30	29	fveq2i 5696	. . . 4 |- ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) = ( Base ` L )
31	27, 30	eqtri 2259	. . 3 |- V = ( Base ` L )
32	31	a1i 9	. 2 |- ( F e. CRing -> V = ( Base ` L ) )
33		plusgslid 13449	. . . . . 6 |- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )
34		vscandxnplusgndx 13497	. . . . . . 7 |- ( .s ` ndx ) =/= ( +g ` ndx )
35	34	necomi 2505	. . . . . 6 |- ( +g ` ndx ) =/= ( .s ` ndx )
36	33, 35, 24	setsslnid 13387	. . . . 5 |- ( ( R e. Grp /\ .* e. _V ) -> ( +g ` R ) = ( +g ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) )
37	3, 19, 36	mp2an 430	. . . 4 |- ( +g ` R ) = ( +g ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
38		rmodislmod.a	. . . 4 |- .+ = ( +g ` R )
39	28	fveq2i 5696	. . . 4 |- ( +g ` L ) = ( +g ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
40	37, 38, 39	3eqtr4i 2269	. . 3 |- .+ = ( +g ` L )
41	40	a1i 9	. 2 |- ( F e. CRing -> .+ = ( +g ` L ) )
42		scaslid 13490	. . . . . 6 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
43		vscandxnscandx 13499	. . . . . . 7 |- ( .s ` ndx ) =/= (Scalar ` ndx )
44	43	necomi 2505	. . . . . 6 |- (Scalar ` ndx ) =/= ( .s ` ndx )
45	42, 44, 24	setsslnid 13387	. . . . 5 |- ( ( R e. Grp /\ .* e. _V ) -> (Scalar ` R ) = (Scalar ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) )
46	3, 19, 45	mp2an 430	. . . 4 |- (Scalar ` R ) = (Scalar ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
47		rmodislmod.f	. . . 4 |- F = (Scalar ` R )
48	28	fveq2i 5696	. . . 4 |- (Scalar ` L ) = (Scalar ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
49	46, 47, 48	3eqtr4i 2269	. . 3 |- F = (Scalar ` L )
50	49	a1i 9	. 2 |- ( F e. CRing -> F = (Scalar ` L ) )
51	23	setsslid 13386	. . . . 5 |- ( ( R e. Grp /\ .* e. _V ) -> .* = ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) )
52	3, 19, 51	mp2an 430	. . . 4 |- .* = ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
53	29	fveq2i 5696	. . . 4 |- ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) = ( .s ` L )
54	52, 53	eqtri 2259	. . 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 14295	. 2 |- ( F e. CRing -> F e. Ring )
64	1	eqcomi 2242	. . . . . 6 |- ( Base ` R ) = V
65	64, 31	eqtri 2259	. . . . 5 |- ( Base ` R ) = ( Base ` L )
66	37, 39	eqtr4i 2262	. . . . 5 |- ( +g ` R ) = ( +g ` L )
67	65, 66	grpprop 13806	. . . 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 6088	. . . . . 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 1029	. . . 4 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> a e. K )
75		simp3 1030	. . . 4 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> b e. V )
76		vex 2824	. . . . . 6 |- b e. _V
77		rmodislmod.s	. . . . . . 7 |- .x. = ( .s ` R )
78	23	slotex 13362	. . . . . . . 8 |- ( R e. Grp -> ( .s ` R ) e. _V )
79	3, 78	ax-mp 5	. . . . . . 7 |- ( .s ` R ) e. _V
80	77, 79	eqeltri 2311	. . . . . 6 |- .x. e. _V
81		vex 2824	. . . . . 6 |- a e. _V
82		ovexg 6113	. . . . . 6 |- ( ( b e. _V /\ .x. e. _V /\ a e. _V ) -> ( b .x. a ) e. _V )
83	76, 80, 81, 82	mp3an 1378	. . . . 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 6210	. . 3 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( a .* b ) = ( b .x. a ) )
86		simpl1 1031	. . . . . . . 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 2614	. . . . . . 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 2614	. . . . . 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 14308	. . . . . . . . . 10 |- ( F e. Ring -> .1. e. K )
90		elex2 2838	. . . . . . . . . 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 3618	. . . . . . . 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 2714	. . . . . . 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 2238	. . . . . . . . . . . . 13 |- ( 0g ` R ) = ( 0g ` R )
98	1, 97	grpidcl 13817	. . . . . . . . . . . 12 |- ( R e. Grp -> ( 0g ` R ) e. V )
99	3, 98	ax-mp 5	. . . . . . . . . . 11 |- ( 0g ` R ) e. V
100		elex2 2838	. . . . . . . . . . 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 3618	. . . . . . . . . 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 6087	. . . . . . . . . . 11 |- ( r = a -> ( w .x. r ) = ( w .x. a ) )
106	105	eleq1d 2307	. . . . . . . . . 10 |- ( r = a -> ( ( w .x. r ) e. V <-> ( w .x. a ) e. V ) )
107		oveq1 6086	. . . . . . . . . . 11 |- ( w = b -> ( w .x. a ) = ( b .x. a ) )
108	107	eleq1d 2307	. . . . . . . . . 10 |- ( w = b -> ( ( w .x. a ) e. V <-> ( b .x. a ) e. V ) )
109	106, 108	rspc2v 2943	. . . . . . . . 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 1046	. . . . . . . 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 1051	. . . 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 2315	. 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 6088	. . . . . . . 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 1028	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> a e. K )
122	1, 38	grpcl 13796	. . . . . . . 8 |- ( ( R e. Grp /\ b e. V /\ c e. V ) -> ( b .+ c ) e. V )
123	3, 122	mp3an1 1365	. . . . . . 7 |- ( ( b e. V /\ c e. V ) -> ( b .+ c ) e. V )
124	123	3adant1 1046	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( b .+ c ) e. V )
125	33	slotex 13362	. . . . . . . . . . 11 |- ( R e. Grp -> ( +g ` R ) e. _V )
126	3, 125	ax-mp 5	. . . . . . . . . 10 |- ( +g ` R ) e. _V
127	38, 126	eqeltri 2311	. . . . . . . . 9 |- .+ e. _V
128		vex 2824	. . . . . . . . 9 |- c e. _V
129		ovexg 6113	. . . . . . . . 9 |- ( ( b e. _V /\ .+ e. _V /\ c e. _V ) -> ( b .+ c ) e. _V )
130	76, 127, 128, 129	mp3an 1378	. . . . . . . 8 |- ( b .+ c ) e. _V
131		ovexg 6113	. . . . . . . 8 |- ( ( ( b .+ c ) e. _V /\ .x. e. _V /\ a e. _V ) -> ( ( b .+ c ) .x. a ) e. _V )
132	130, 80, 81, 131	mp3an 1378	. . . . . . 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 6210	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* ( b .+ c ) ) = ( ( b .+ c ) .x. a ) )
135		simpl2 1032	. . . . . . . . . 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 2614	. . . . . . . . 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 2614	. . . . . . . 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 3618	. . . . . . . . . . 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 6087	. . . . . . . . . . . 12 |- ( r = a -> ( ( w .+ x ) .x. r ) = ( ( w .+ x ) .x. a ) )
142		oveq2 6087	. . . . . . . . . . . . 13 |- ( r = a -> ( x .x. r ) = ( x .x. a ) )
143	105, 142	oveq12d 6097	. . . . . . . . . . . 12 |- ( r = a -> ( ( w .x. r ) .+ ( x .x. r ) ) = ( ( w .x. a ) .+ ( x .x. a ) ) )
144	141, 143	eqeq12d 2253	. . . . . . . . . . 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 6087	. . . . . . . . . . . . 13 |- ( x = c -> ( w .+ x ) = ( w .+ c ) )
146	145	oveq1d 6094	. . . . . . . . . . . 12 |- ( x = c -> ( ( w .+ x ) .x. a ) = ( ( w .+ c ) .x. a ) )
147		oveq1 6086	. . . . . . . . . . . . 13 |- ( x = c -> ( x .x. a ) = ( c .x. a ) )
148	147	oveq2d 6095	. . . . . . . . . . . 12 |- ( x = c -> ( ( w .x. a ) .+ ( x .x. a ) ) = ( ( w .x. a ) .+ ( c .x. a ) ) )
149	146, 148	eqeq12d 2253	. . . . . . . . . . 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 6086	. . . . . . . . . . . . 13 |- ( w = b -> ( w .+ c ) = ( b .+ c ) )
151	150	oveq1d 6094	. . . . . . . . . . . 12 |- ( w = b -> ( ( w .+ c ) .x. a ) = ( ( b .+ c ) .x. a ) )
152	107	oveq1d 6094	. . . . . . . . . . . 12 |- ( w = b -> ( ( w .x. a ) .+ ( c .x. a ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
153	151, 152	eqeq12d 2253	. . . . . . . . . . 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 2946	. . . . . . . . . 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 1240	. . . . . . . . 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 1051	. . . . . 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 2271	. . . 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 1029	. . . . . 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 6210	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* b ) = ( b .x. a ) )
166		oveq12 6088	. . . . . . . 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 1030	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> c e. V )
170		ovexg 6113	. . . . . . . 8 |- ( ( c e. _V /\ .x. e. _V /\ a e. _V ) -> ( c .x. a ) e. _V )
171	128, 80, 81, 170	mp3an 1378	. . . . . . 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 6210	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
174	165, 173	oveq12d 6097	. . . 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 2274	. 2 |- ( ( F e. CRing /\ ( a e. K /\ b e. V /\ c e. V ) ) -> ( a .* ( b .+ c ) ) = ( ( a .* b ) .+ ( a .* c ) ) )
177		simpl3 1033	. . . . . . . . 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 2614	. . . . . . . 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 2614	. . . . . . 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 2716	. . . . . . . 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 3618	. . . . . . . . . . 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 6086	. . . . . . . . . . . 12 |- ( q = a -> ( q .+^ r ) = ( a .+^ r ) )
185	184	oveq2d 6095	. . . . . . . . . . 11 |- ( q = a -> ( w .x. ( q .+^ r ) ) = ( w .x. ( a .+^ r ) ) )
186		oveq2 6087	. . . . . . . . . . . 12 |- ( q = a -> ( w .x. q ) = ( w .x. a ) )
187	186	oveq1d 6094	. . . . . . . . . . 11 |- ( q = a -> ( ( w .x. q ) .+ ( w .x. r ) ) = ( ( w .x. a ) .+ ( w .x. r ) ) )
188	185, 187	eqeq12d 2253	. . . . . . . . . 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 6087	. . . . . . . . . . . 12 |- ( r = b -> ( a .+^ r ) = ( a .+^ b ) )
190	189	oveq2d 6095	. . . . . . . . . . 11 |- ( r = b -> ( w .x. ( a .+^ r ) ) = ( w .x. ( a .+^ b ) ) )
191		oveq2 6087	. . . . . . . . . . . 12 |- ( r = b -> ( w .x. r ) = ( w .x. b ) )
192	191	oveq2d 6095	. . . . . . . . . . 11 |- ( r = b -> ( ( w .x. a ) .+ ( w .x. r ) ) = ( ( w .x. a ) .+ ( w .x. b ) ) )
193	190, 192	eqeq12d 2253	. . . . . . . . . 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 6086	. . . . . . . . . . 11 |- ( w = c -> ( w .x. ( a .+^ b ) ) = ( c .x. ( a .+^ b ) ) )
195		oveq1 6086	. . . . . . . . . . . 12 |- ( w = c -> ( w .x. a ) = ( c .x. a ) )
196		oveq1 6086	. . . . . . . . . . . 12 |- ( w = c -> ( w .x. b ) = ( c .x. b ) )
197	195, 196	oveq12d 6097	. . . . . . . . . . 11 |- ( w = c -> ( ( w .x. a ) .+ ( w .x. b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) )
198	194, 197	eqeq12d 2253	. . . . . . . . . 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 2946	. . . . . . . . 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 1051	. . . . 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 6088	. . . . . . 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 14288	. . . . . . . . 9 |- ( F e. Ring -> F e. Grp )
210	4, 57	grpcl 13796	. . . . . . . . . 10 |- ( ( F e. Grp /\ a e. K /\ b e. K ) -> ( a .+^ b ) e. K )
211	210	3expib 1237	. . . . . . . . 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 1050	. . . . . . 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 1048	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .+^ b ) e. K )
216		simp3 1030	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> c e. V )
217	33	slotex 13362	. . . . . . . . . 10 |- ( F e. Ring -> ( +g ` F ) e. _V )
218	6, 217	ax-mp 5	. . . . . . . . 9 |- ( +g ` F ) e. _V
219	57, 218	eqeltri 2311	. . . . . . . 8 |- .+^ e. _V
220		ovexg 6113	. . . . . . . 8 |- ( ( a e. _V /\ .+^ e. _V /\ b e. _V ) -> ( a .+^ b ) e. _V )
221	81, 219, 76, 220	mp3an 1378	. . . . . . 7 |- ( a .+^ b ) e. _V
222		ovexg 6113	. . . . . . 7 |- ( ( c e. _V /\ .x. e. _V /\ ( a .+^ b ) e. _V ) -> ( c .x. ( a .+^ b ) ) e. _V )
223	128, 80, 221, 222	mp3an 1378	. . . . . 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 6210	. . . 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 1028	. . . . . 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 6210	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
230		oveq12 6088	. . . . . . . 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 1029	. . . . . 6 |- ( ( a e. K /\ b e. K /\ c e. V ) -> b e. K )
234		ovexg 6113	. . . . . . . 8 |- ( ( c e. _V /\ .x. e. _V /\ b e. _V ) -> ( c .x. b ) e. _V )
235	128, 80, 76, 234	mp3an 1378	. . . . . . 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 6210	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( b .* c ) = ( c .x. b ) )
238	229, 237	oveq12d 6097	. . . 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 2281	. . 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 14670	. 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 6088	. . . . . 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 6113	. . . . . 6 |- ( ( a e. _V /\ .x. e. _V /\ .1. e. K ) -> ( a .x. .1. ) e. _V )
251	81, 80, 249, 250	mp3an 1378	. . . . 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 6210	. . 3 |- ( ( F e. CRing /\ a e. V ) -> ( .1. .* a ) = ( a .x. .1. ) )
254		simprr 537	. . . . . . . 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 2614	. . . . . . 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 2614	. . . . . 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 3618	. . . . . . . 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 3618	. . . . . . . 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 3618	. . . . . . . . . 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 6086	. . . . . . . . . . 11 |- ( w = a -> ( w .x. .1. ) = ( a .x. .1. ) )
266		id 19	. . . . . . . . . . 11 |- ( w = a -> w = a )
267	265, 266	eqeq12d 2253	. . . . . . . . . 10 |- ( w = a -> ( ( w .x. .1. ) = w <-> ( a .x. .1. ) = a ) )
268	267	rspcv 2925	. . . . . . . . 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 1051	. . . 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 2271	. 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 14612	1 |- ( F e. CRing -> L e. LMod )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1009   = wceq 1402   E.wex 1545   e. wcel 2209   A.wral 2528   _Vcvv 2821   <.cop 3711   Fn wfn 5370   ` cfv 5375  (class class class)co 6079   e. cmpo 6081   NNcn 9287   ndxcnx 13332   sSet csts 13333  Slot cslot 13334   Basecbs 13335   +g cplusg 13414   .rcmulr 13415  Scalarcsca 13417   .scvsca 13418   0gc0g 13593   Grpcgrp 13788   1rcur 14245   Ringcrg 14283   CRingccrg 14284   LModclmod 14606

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4244  ax-sep 4247  ax-pow 4309  ax-pr 4344  ax-un 4576  ax-setind 4682  ax-cnex 8264  ax-resscn 8265  ax-1cn 8266  ax-1re 8267  ax-icn 8268  ax-addcl 8269  ax-addrcl 8270  ax-mulcl 8271  ax-addcom 8273  ax-addass 8275  ax-i2m1 8278  ax-0lt1 8279  ax-0id 8281  ax-rnegex 8282  ax-pre-ltirr 8285  ax-pre-lttrn 8287  ax-pre-ltadd 8289

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-int 3969  df-iun 4012  df-br 4129  df-opab 4191  df-mpt 4192  df-id 4436  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-rn 4783  df-res 4784  df-ima 4785  df-iota 5335  df-fun 5377  df-fn 5378  df-f 5379  df-f1 5380  df-fo 5381  df-f1o 5382  df-fv 5383  df-riota 6032  df-ov 6082  df-oprab 6083  df-mpo 6084  df-1st 6368  df-2nd 6369  df-pnf 8356  df-mnf 8357  df-ltxr 8359  df-inn 9288  df-2 9346  df-3 9347  df-4 9348  df-5 9349  df-6 9350  df-ndx 13338  df-slot 13339  df-base 13341  df-sets 13342  df-plusg 13427  df-mulr 13428  df-sca 13430  df-vsca 13431  df-0g 13595  df-mgm 13659  df-sgrp 13700  df-mnd 13713  df-grp 13791  df-cmn 14072  df-mgp 14201  df-ur 14246  df-ring 14285  df-cring 14286  df-lmod 14608

This theorem is referenced by: (None)