Theorem rmodislmod 13983

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 13921 of a left module, see also islmod 13923. (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 12761	. . . . . . . . 9 |- Base Fn _V
6	2	simp2i 1009	. . . . . . . . . 10 |- F e. Ring
7	6	elexi 2775	. . . . . . . . 9 |- F e. _V
8		funfvex 5578	. . . . . . . . . 10 |- ( ( Fun Base /\ F e. dom Base ) -> ( Base ` F ) e. _V )
9	8	funfni 5361	. . . . . . . . 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 5578	. . . . . . . . . 10 |- ( ( Fun Base /\ R e. dom Base ) -> ( Base ` R ) e. _V )
14	13	funfni 5361	. . . . . . . . 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 6278	. . . . . . 7 |- ( ( K e. _V /\ V e. _V ) -> .* e. _V )
19	11, 16, 18	mp2an 426	. . . . . 6 |- .* e. _V
20		baseslid 12760	. . . . . . 7 |- ( Base = Slot ( Base ` ndx ) /\ ( Base ` ndx ) e. NN )
21		vscandxnbasendx 12861	. . . . . . . 8 |- ( .s ` ndx ) =/= ( Base ` ndx )
22	21	necomi 2452	. . . . . . 7 |- ( Base ` ndx ) =/= ( .s ` ndx )
23		vscaslid 12865	. . . . . . . 8 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
24	23	simpri 113	. . . . . . 7 |- ( .s ` ndx ) e. NN
25	20, 22, 24	setsslnid 12755	. . . . . 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 5564	. . . 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 12815	. . . . . 6 |- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )
34		vscandxnplusgndx 12862	. . . . . . 7 |- ( .s ` ndx ) =/= ( +g ` ndx )
35	34	necomi 2452	. . . . . 6 |- ( +g ` ndx ) =/= ( .s ` ndx )
36	33, 35, 24	setsslnid 12755	. . . . 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 5564	. . . 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 12855	. . . . . 6 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
43		vscandxnscandx 12864	. . . . . . 7 |- ( .s ` ndx ) =/= (Scalar ` ndx )
44	43	necomi 2452	. . . . . 6 |- (Scalar ` ndx ) =/= ( .s ` ndx )
45	42, 44, 24	setsslnid 12755	. . . . 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 5564	. . . 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 12754	. . . . 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 5564	. . . 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 13640	. 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 13220	. . . 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 5934	. . . . . 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 12730	. . . . . . . 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 5959	. . . . . 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 6054	. . 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 13652	. . . . . . . . . 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 3542	. . . . . . . 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 13231	. . . . . . . . . . . 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 3542	. . . . . . . . . 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 5933	. . . . . . . . . . 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 5932	. . . . . . . . . . 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 5934	. . . . . . . 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 13210	. . . . . . . 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 12730	. . . . . . . . . . 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 5959	. . . . . . . . 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 5959	. . . . . . . 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 6054	. . . . 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 3542	. . . . . . . . . . 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 5933	. . . . . . . . . . . 12 |- ( r = a -> ( ( w .+ x ) .x. r ) = ( ( w .+ x ) .x. a ) )
142		oveq2 5933	. . . . . . . . . . . . 13 |- ( r = a -> ( x .x. r ) = ( x .x. a ) )
143	105, 142	oveq12d 5943	. . . . . . . . . . . 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 5933	. . . . . . . . . . . . 13 |- ( x = c -> ( w .+ x ) = ( w .+ c ) )
146	145	oveq1d 5940	. . . . . . . . . . . 12 |- ( x = c -> ( ( w .+ x ) .x. a ) = ( ( w .+ c ) .x. a ) )
147		oveq1 5932	. . . . . . . . . . . . 13 |- ( x = c -> ( x .x. a ) = ( c .x. a ) )
148	147	oveq2d 5941	. . . . . . . . . . . 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 5932	. . . . . . . . . . . . 13 |- ( w = b -> ( w .+ c ) = ( b .+ c ) )
151	150	oveq1d 5940	. . . . . . . . . . . 12 |- ( w = b -> ( ( w .+ c ) .x. a ) = ( ( b .+ c ) .x. a ) )
152	107	oveq1d 5940	. . . . . . . . . . . 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 6054	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* b ) = ( b .x. a ) )
166		oveq12 5934	. . . . . . . 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 5959	. . . . . . . 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 6054	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
174	165, 173	oveq12d 5943	. . . 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 3542	. . . . . . . . . . 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 5932	. . . . . . . . . . . 12 |- ( q = a -> ( q .+^ r ) = ( a .+^ r ) )
185	184	oveq2d 5941	. . . . . . . . . . 11 |- ( q = a -> ( w .x. ( q .+^ r ) ) = ( w .x. ( a .+^ r ) ) )
186		oveq2 5933	. . . . . . . . . . . 12 |- ( q = a -> ( w .x. q ) = ( w .x. a ) )
187	186	oveq1d 5940	. . . . . . . . . . 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 5933	. . . . . . . . . . . 12 |- ( r = b -> ( a .+^ r ) = ( a .+^ b ) )
190	189	oveq2d 5941	. . . . . . . . . . 11 |- ( r = b -> ( w .x. ( a .+^ r ) ) = ( w .x. ( a .+^ b ) ) )
191		oveq2 5933	. . . . . . . . . . . 12 |- ( r = b -> ( w .x. r ) = ( w .x. b ) )
192	191	oveq2d 5941	. . . . . . . . . . 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 5932	. . . . . . . . . . 11 |- ( w = c -> ( w .x. ( a .+^ b ) ) = ( c .x. ( a .+^ b ) ) )
195		oveq1 5932	. . . . . . . . . . . 12 |- ( w = c -> ( w .x. a ) = ( c .x. a ) )
196		oveq1 5932	. . . . . . . . . . . 12 |- ( w = c -> ( w .x. b ) = ( c .x. b ) )
197	195, 196	oveq12d 5943	. . . . . . . . . . 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 5934	. . . . . . 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 13633	. . . . . . . . 9 |- ( F e. Ring -> F e. Grp )
210	4, 57	grpcl 13210	. . . . . . . . . 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 12730	. . . . . . . . . 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 5959	. . . . . . . 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 5959	. . . . . . 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 6054	. . . 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 6054	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
230		oveq12 5934	. . . . . . . 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 5959	. . . . . . . 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 6054	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( b .* c ) = ( c .x. b ) )
238	229, 237	oveq12d 5943	. . . 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 13982	. 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 5934	. . . . . 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 5959	. . . . . 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 6054	. . 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 3542	. . . . . . . 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 3542	. . . . . . . 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 3542	. . . . . . . . . 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 5932	. . . . . . . . . . 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 13925	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 3626   Fn wfn 5254   ` cfv 5259  (class class class)co 5925   e. cmpo 5927   NNcn 9007   ndxcnx 12700   sSet csts 12701  Slot cslot 12702   Basecbs 12703   +g cplusg 12780   .rcmulr 12781  Scalarcsca 12783   .scvsca 12784   0gc0g 12958   Grpcgrp 13202   1rcur 13591   Ringcrg 13628   CRingccrg 13629   LModclmod 13919

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 4149  ax-sep 4152  ax-pow 4208  ax-pr 4243  ax-un 4469  ax-setind 4574  ax-cnex 7987  ax-resscn 7988  ax-1cn 7989  ax-1re 7990  ax-icn 7991  ax-addcl 7992  ax-addrcl 7993  ax-mulcl 7994  ax-addcom 7996  ax-addass 7998  ax-i2m1 8001  ax-0lt1 8002  ax-0id 8004  ax-rnegex 8005  ax-pre-ltirr 8008  ax-pre-lttrn 8010  ax-pre-ltadd 8012

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 3452  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-int 3876  df-iun 3919  df-br 4035  df-opab 4096  df-mpt 4097  df-id 4329  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-rn 4675  df-res 4676  df-ima 4677  df-iota 5220  df-fun 5261  df-fn 5262  df-f 5263  df-f1 5264  df-fo 5265  df-f1o 5266  df-fv 5267  df-riota 5880  df-ov 5928  df-oprab 5929  df-mpo 5930  df-1st 6207  df-2nd 6208  df-pnf 8080  df-mnf 8081  df-ltxr 8083  df-inn 9008  df-2 9066  df-3 9067  df-4 9068  df-5 9069  df-6 9070  df-ndx 12706  df-slot 12707  df-base 12709  df-sets 12710  df-plusg 12793  df-mulr 12794  df-sca 12796  df-vsca 12797  df-0g 12960  df-mgm 13058  df-sgrp 13104  df-mnd 13119  df-grp 13205  df-cmn 13492  df-mgp 13553  df-ur 13592  df-ring 13630  df-cring 13631  df-lmod 13921

This theorem is referenced by: (None)