Theorem rmodislmod 18931

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 the definition df-lmod 18865 of a left module, see also islmod 18867. (Contributed by AV, 3-Dec-2021.)

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 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rmodislmod.v	. . . . 5 |- V = ( Base ` R )
2		baseid 15919	. . . . . 6 |- Base = Slot ( Base ` ndx )
3		df-base 15863	. . . . . . . 8 |- Base = Slot 1
4		1nn 11031	. . . . . . . 8 |- 1 e. NN
5	3, 4	ndxarg 15882	. . . . . . 7 |- ( Base ` ndx ) = 1
6		1re 10039	. . . . . . . . 9 |- 1 e. RR
7		1lt6 11208	. . . . . . . . 9 |- 1 < 6
8	6, 7	ltneii 10150	. . . . . . . 8 |- 1 =/= 6
9		vscandx 16015	. . . . . . . 8 |- ( .s ` ndx ) = 6
10	8, 9	neeqtrri 2867	. . . . . . 7 |- 1 =/= ( .s ` ndx )
11	5, 10	eqnetri 2864	. . . . . 6 |- ( Base ` ndx ) =/= ( .s ` ndx )
12	2, 11	setsnid 15915	. . . . 5 |- ( Base ` R ) = ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
13	1, 12	eqtri 2644	. . . 4 |- V = ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
14		rmodislmod.l	. . . . . 6 |- L = ( R sSet <. ( .s ` ndx ) , .* >. )
15	14	eqcomi 2631	. . . . 5 |- ( R sSet <. ( .s ` ndx ) , .* >. ) = L
16	15	fveq2i 6194	. . . 4 |- ( Base ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) = ( Base ` L )
17	13, 16	eqtri 2644	. . 3 |- V = ( Base ` L )
18	17	a1i 11	. 2 |- ( F e. CRing -> V = ( Base ` L ) )
19		plusgid 15977	. . . . 5 |- +g = Slot ( +g ` ndx )
20		plusgndx 15976	. . . . . 6 |- ( +g ` ndx ) = 2
21		2re 11090	. . . . . . . 8 |- 2 e. RR
22		2lt6 11207	. . . . . . . 8 |- 2 < 6
23	21, 22	ltneii 10150	. . . . . . 7 |- 2 =/= 6
24	23, 9	neeqtrri 2867	. . . . . 6 |- 2 =/= ( .s ` ndx )
25	20, 24	eqnetri 2864	. . . . 5 |- ( +g ` ndx ) =/= ( .s ` ndx )
26	19, 25	setsnid 15915	. . . 4 |- ( +g ` R ) = ( +g ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
27		rmodislmod.a	. . . 4 |- .+ = ( +g ` R )
28	14	fveq2i 6194	. . . 4 |- ( +g ` L ) = ( +g ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
29	26, 27, 28	3eqtr4i 2654	. . 3 |- .+ = ( +g ` L )
30	29	a1i 11	. 2 |- ( F e. CRing -> .+ = ( +g ` L ) )
31		scaid 16014	. . . . 5 |- Scalar = Slot (Scalar ` ndx )
32		scandx 16013	. . . . . 6 |- (Scalar ` ndx ) = 5
33		5re 11099	. . . . . . . 8 |- 5 e. RR
34		5lt6 11204	. . . . . . . 8 |- 5 < 6
35	33, 34	ltneii 10150	. . . . . . 7 |- 5 =/= 6
36	35, 9	neeqtrri 2867	. . . . . 6 |- 5 =/= ( .s ` ndx )
37	32, 36	eqnetri 2864	. . . . 5 |- (Scalar ` ndx ) =/= ( .s ` ndx )
38	31, 37	setsnid 15915	. . . 4 |- (Scalar ` R ) = (Scalar ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
39		rmodislmod.f	. . . 4 |- F = (Scalar ` R )
40	14	fveq2i 6194	. . . 4 |- (Scalar ` L ) = (Scalar ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
41	38, 39, 40	3eqtr4i 2654	. . 3 |- F = (Scalar ` L )
42	41	a1i 11	. 2 |- ( F e. CRing -> F = (Scalar ` L ) )
43		rmodislmod.r	. . . . . 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 ) ) )
44	43	simp1i 1070	. . . . 5 |- R e. Grp
45		rmodislmod.k	. . . . . . 7 |- K = ( Base ` F )
46	45	fvexi 6202	. . . . . 6 |- K e. _V
47	1	fvexi 6202	. . . . . 6 |- V e. _V
48		rmodislmod.m	. . . . . . 7 |- .* = ( s e. K , v e. V |-> ( v .x. s ) )
49	48	mpt2exg 7245	. . . . . 6 |- ( ( K e. _V /\ V e. _V ) -> .* e. _V )
50	46, 47, 49	mp2an 708	. . . . 5 |- .* e. _V
51		vscaid 16016	. . . . . 6 |- .s = Slot ( .s ` ndx )
52	51	setsid 15914	. . . . 5 |- ( ( R e. Grp /\ .* e. _V ) -> .* = ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) )
53	44, 50, 52	mp2an 708	. . . 4 |- .* = ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) )
54	15	fveq2i 6194	. . . 4 |- ( .s ` ( R sSet <. ( .s ` ndx ) , .* >. ) ) = ( .s ` L )
55	53, 54	eqtri 2644	. . 3 |- .* = ( .s ` L )
56	55	a1i 11	. 2 |- ( F e. CRing -> .* = ( .s ` L ) )
57	45	a1i 11	. 2 |- ( F e. CRing -> K = ( Base ` F ) )
58		rmodislmod.p	. . 3 |- .+^ = ( +g ` F )
59	58	a1i 11	. 2 |- ( F e. CRing -> .+^ = ( +g ` F ) )
60		rmodislmod.t	. . 3 |- .X. = ( .r ` F )
61	60	a1i 11	. 2 |- ( F e. CRing -> .X. = ( .r ` F ) )
62		rmodislmod.u	. . 3 |- .1. = ( 1r ` F )
63	62	a1i 11	. 2 |- ( F e. CRing -> .1. = ( 1r ` F ) )
64		crngring 18558	. 2 |- ( F e. CRing -> F e. Ring )
65	1	eqcomi 2631	. . . . . 6 |- ( Base ` R ) = V
66	65, 17	eqtri 2644	. . . . 5 |- ( Base ` R ) = ( Base ` L )
67	26, 28	eqtr4i 2647	. . . . 5 |- ( +g ` R ) = ( +g ` L )
68	66, 67	grpprop 17438	. . . 4 |- ( R e. Grp <-> L e. Grp )
69	44, 68	mpbi 220	. . 3 |- L e. Grp
70	69	a1i 11	. 2 |- ( F e. CRing -> L e. Grp )
71	48	a1i 11	. . . 4 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
72		oveq12 6659	. . . . . 6 |- ( ( v = b /\ s = a ) -> ( v .x. s ) = ( b .x. a ) )
73	72	ancoms 469	. . . . 5 |- ( ( s = a /\ v = b ) -> ( v .x. s ) = ( b .x. a ) )
74	73	adantl 482	. . . 4 |- ( ( ( F e. CRing /\ a e. K /\ b e. V ) /\ ( s = a /\ v = b ) ) -> ( v .x. s ) = ( b .x. a ) )
75		simp2 1062	. . . 4 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> a e. K )
76		simp3 1063	. . . 4 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> b e. V )
77		ovexd 6680	. . . 4 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( b .x. a ) e. _V )
78	71, 74, 75, 76, 77	ovmpt2d 6788	. . 3 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( a .* b ) = ( b .x. a ) )
79		simpl1 1064	. . . . . . . 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 )
80	79	2ralimi 2953	. . . . . . 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 )
81	80	2ralimi 2953	. . . . . 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 )
82		ringgrp 18552	. . . . . . . . . 10 |- ( F e. Ring -> F e. Grp )
83	45	grpbn0 17451	. . . . . . . . . 10 |- ( F e. Grp -> K =/= (/) )
84	82, 83	syl 17	. . . . . . . . 9 |- ( F e. Ring -> K =/= (/) )
85	84	3ad2ant2 1083	. . . . . . . 8 |- ( ( 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 ) ) ) -> K =/= (/) )
86	43, 85	ax-mp 5	. . . . . . 7 |- K =/= (/)
87		rspn0 3934	. . . . . . 7 |- ( K =/= (/) -> ( 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 ) )
88	86, 87	ax-mp 5	. . . . . 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 )
89		ralcom 3098	. . . . . . 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 )
90	1	grpbn0 17451	. . . . . . . . . . 11 |- ( R e. Grp -> V =/= (/) )
91	90	3ad2ant1 1082	. . . . . . . . . 10 |- ( ( 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 ) ) ) -> V =/= (/) )
92	43, 91	ax-mp 5	. . . . . . . . 9 |- V =/= (/)
93		rspn0 3934	. . . . . . . . 9 |- ( V =/= (/) -> ( 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 ) )
94	92, 93	ax-mp 5	. . . . . . . 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 )
95		oveq2 6658	. . . . . . . . . . 11 |- ( r = a -> ( w .x. r ) = ( w .x. a ) )
96	95	eleq1d 2686	. . . . . . . . . 10 |- ( r = a -> ( ( w .x. r ) e. V <-> ( w .x. a ) e. V ) )
97		oveq1 6657	. . . . . . . . . . 11 |- ( w = b -> ( w .x. a ) = ( b .x. a ) )
98	97	eleq1d 2686	. . . . . . . . . 10 |- ( w = b -> ( ( w .x. a ) e. V <-> ( b .x. a ) e. V ) )
99	96, 98	rspc2v 3322	. . . . . . . . 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 ) )
100	99	3adant1 1079	. . . . . . . 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 ) )
101	94, 100	syl5com 31	. . . . . . 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 ) )
102	89, 101	sylbi 207	. . . . . 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 ) )
103	81, 88, 102	3syl 18	. . . . 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 ) )
104	103	3ad2ant3 1084	. . . 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 ) )
105	43, 104	ax-mp 5	. . 3 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( b .x. a ) e. V )
106	78, 105	eqeltrd 2701	. 2 |- ( ( F e. CRing /\ a e. K /\ b e. V ) -> ( a .* b ) e. V )
107	48	a1i 11	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
108		oveq12 6659	. . . . . . . 8 |- ( ( v = ( b .+ c ) /\ s = a ) -> ( v .x. s ) = ( ( b .+ c ) .x. a ) )
109	108	ancoms 469	. . . . . . 7 |- ( ( s = a /\ v = ( b .+ c ) ) -> ( v .x. s ) = ( ( b .+ c ) .x. a ) )
110	109	adantl 482	. . . . . 6 |- ( ( ( a e. K /\ b e. V /\ c e. V ) /\ ( s = a /\ v = ( b .+ c ) ) ) -> ( v .x. s ) = ( ( b .+ c ) .x. a ) )
111		simp1 1061	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> a e. K )
112	1, 27	grpcl 17430	. . . . . . . 8 |- ( ( R e. Grp /\ b e. V /\ c e. V ) -> ( b .+ c ) e. V )
113	44, 112	mp3an1 1411	. . . . . . 7 |- ( ( b e. V /\ c e. V ) -> ( b .+ c ) e. V )
114	113	3adant1 1079	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( b .+ c ) e. V )
115		ovexd 6680	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( ( b .+ c ) .x. a ) e. _V )
116	107, 110, 111, 114, 115	ovmpt2d 6788	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* ( b .+ c ) ) = ( ( b .+ c ) .x. a ) )
117		simpl2 1065	. . . . . . . . . 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 ) ) )
118	117	2ralimi 2953	. . . . . . . . 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 ) ) )
119	118	2ralimi 2953	. . . . . . . 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 ) ) )
120		rspn0 3934	. . . . . . . . . 10 |- ( K =/= (/) -> ( 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 ) ) ) )
121	86, 120	ax-mp 5	. . . . . . . . 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 ) ) )
122		oveq2 6658	. . . . . . . . . . . 12 |- ( r = a -> ( ( w .+ x ) .x. r ) = ( ( w .+ x ) .x. a ) )
123		oveq2 6658	. . . . . . . . . . . . 13 |- ( r = a -> ( x .x. r ) = ( x .x. a ) )
124	95, 123	oveq12d 6668	. . . . . . . . . . . 12 |- ( r = a -> ( ( w .x. r ) .+ ( x .x. r ) ) = ( ( w .x. a ) .+ ( x .x. a ) ) )
125	122, 124	eqeq12d 2637	. . . . . . . . . . 11 |- ( r = a -> ( ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) <-> ( ( w .+ x ) .x. a ) = ( ( w .x. a ) .+ ( x .x. a ) ) ) )
126		oveq2 6658	. . . . . . . . . . . . 13 |- ( x = c -> ( w .+ x ) = ( w .+ c ) )
127	126	oveq1d 6665	. . . . . . . . . . . 12 |- ( x = c -> ( ( w .+ x ) .x. a ) = ( ( w .+ c ) .x. a ) )
128		oveq1 6657	. . . . . . . . . . . . 13 |- ( x = c -> ( x .x. a ) = ( c .x. a ) )
129	128	oveq2d 6666	. . . . . . . . . . . 12 |- ( x = c -> ( ( w .x. a ) .+ ( x .x. a ) ) = ( ( w .x. a ) .+ ( c .x. a ) ) )
130	127, 129	eqeq12d 2637	. . . . . . . . . . 11 |- ( x = c -> ( ( ( w .+ x ) .x. a ) = ( ( w .x. a ) .+ ( x .x. a ) ) <-> ( ( w .+ c ) .x. a ) = ( ( w .x. a ) .+ ( c .x. a ) ) ) )
131		oveq1 6657	. . . . . . . . . . . . 13 |- ( w = b -> ( w .+ c ) = ( b .+ c ) )
132	131	oveq1d 6665	. . . . . . . . . . . 12 |- ( w = b -> ( ( w .+ c ) .x. a ) = ( ( b .+ c ) .x. a ) )
133	97	oveq1d 6665	. . . . . . . . . . . 12 |- ( w = b -> ( ( w .x. a ) .+ ( c .x. a ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
134	132, 133	eqeq12d 2637	. . . . . . . . . . 11 |- ( w = b -> ( ( ( w .+ c ) .x. a ) = ( ( w .x. a ) .+ ( c .x. a ) ) <-> ( ( b .+ c ) .x. a ) = ( ( b .x. a ) .+ ( c .x. a ) ) ) )
135	125, 130, 134	rspc3v 3325	. . . . . . . . . 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 ) ) ) )
136	135	3com23 1271	. . . . . . . . 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 ) ) ) )
137	121, 136	syl5com 31	. . . . . . . 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 ) ) ) )
138	119, 137	syl 17	. . . . . . 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 ) ) ) )
139	138	3ad2ant3 1084	. . . . . 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 ) ) ) )
140	43, 139	ax-mp 5	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( ( b .+ c ) .x. a ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
141	116, 140	eqtrd 2656	. . . 4 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* ( b .+ c ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
142	141	adantl 482	. . 3 |- ( ( F e. CRing /\ ( a e. K /\ b e. V /\ c e. V ) ) -> ( a .* ( b .+ c ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
143	73	adantl 482	. . . . . 6 |- ( ( ( a e. K /\ b e. V /\ c e. V ) /\ ( s = a /\ v = b ) ) -> ( v .x. s ) = ( b .x. a ) )
144		simp2 1062	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> b e. V )
145		ovexd 6680	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( b .x. a ) e. _V )
146	107, 143, 111, 144, 145	ovmpt2d 6788	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* b ) = ( b .x. a ) )
147		oveq12 6659	. . . . . . . 8 |- ( ( v = c /\ s = a ) -> ( v .x. s ) = ( c .x. a ) )
148	147	ancoms 469	. . . . . . 7 |- ( ( s = a /\ v = c ) -> ( v .x. s ) = ( c .x. a ) )
149	148	adantl 482	. . . . . 6 |- ( ( ( a e. K /\ b e. V /\ c e. V ) /\ ( s = a /\ v = c ) ) -> ( v .x. s ) = ( c .x. a ) )
150		simp3 1063	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> c e. V )
151		ovexd 6680	. . . . . 6 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( c .x. a ) e. _V )
152	107, 149, 111, 150, 151	ovmpt2d 6788	. . . . 5 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
153	146, 152	oveq12d 6668	. . . 4 |- ( ( a e. K /\ b e. V /\ c e. V ) -> ( ( a .* b ) .+ ( a .* c ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
154	153	adantl 482	. . 3 |- ( ( F e. CRing /\ ( a e. K /\ b e. V /\ c e. V ) ) -> ( ( a .* b ) .+ ( a .* c ) ) = ( ( b .x. a ) .+ ( c .x. a ) ) )
155	142, 154	eqtr4d 2659	. 2 |- ( ( F e. CRing /\ ( a e. K /\ b e. V /\ c e. V ) ) -> ( a .* ( b .+ c ) ) = ( ( a .* b ) .+ ( a .* c ) ) )
156		simpl3 1066	. . . . . . . . 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 ) ) )
157	156	2ralimi 2953	. . . . . . . 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 ) ) )
158	157	2ralimi 2953	. . . . . . 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 ) ) )
159		ralrot3 3102	. . . . . . . 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 ) ) )
160		rspn0 3934	. . . . . . . . . 10 |- ( V =/= (/) -> ( 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 ) ) ) )
161	92, 160	ax-mp 5	. . . . . . . . 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 ) ) )
162		oveq1 6657	. . . . . . . . . . . 12 |- ( q = a -> ( q .+^ r ) = ( a .+^ r ) )
163	162	oveq2d 6666	. . . . . . . . . . 11 |- ( q = a -> ( w .x. ( q .+^ r ) ) = ( w .x. ( a .+^ r ) ) )
164		oveq2 6658	. . . . . . . . . . . 12 |- ( q = a -> ( w .x. q ) = ( w .x. a ) )
165	164	oveq1d 6665	. . . . . . . . . . 11 |- ( q = a -> ( ( w .x. q ) .+ ( w .x. r ) ) = ( ( w .x. a ) .+ ( w .x. r ) ) )
166	163, 165	eqeq12d 2637	. . . . . . . . . 10 |- ( q = a -> ( ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) <-> ( w .x. ( a .+^ r ) ) = ( ( w .x. a ) .+ ( w .x. r ) ) ) )
167		oveq2 6658	. . . . . . . . . . . 12 |- ( r = b -> ( a .+^ r ) = ( a .+^ b ) )
168	167	oveq2d 6666	. . . . . . . . . . 11 |- ( r = b -> ( w .x. ( a .+^ r ) ) = ( w .x. ( a .+^ b ) ) )
169		oveq2 6658	. . . . . . . . . . . 12 |- ( r = b -> ( w .x. r ) = ( w .x. b ) )
170	169	oveq2d 6666	. . . . . . . . . . 11 |- ( r = b -> ( ( w .x. a ) .+ ( w .x. r ) ) = ( ( w .x. a ) .+ ( w .x. b ) ) )
171	168, 170	eqeq12d 2637	. . . . . . . . . 10 |- ( r = b -> ( ( w .x. ( a .+^ r ) ) = ( ( w .x. a ) .+ ( w .x. r ) ) <-> ( w .x. ( a .+^ b ) ) = ( ( w .x. a ) .+ ( w .x. b ) ) ) )
172		oveq1 6657	. . . . . . . . . . 11 |- ( w = c -> ( w .x. ( a .+^ b ) ) = ( c .x. ( a .+^ b ) ) )
173		oveq1 6657	. . . . . . . . . . . 12 |- ( w = c -> ( w .x. a ) = ( c .x. a ) )
174		oveq1 6657	. . . . . . . . . . . 12 |- ( w = c -> ( w .x. b ) = ( c .x. b ) )
175	173, 174	oveq12d 6668	. . . . . . . . . . 11 |- ( w = c -> ( ( w .x. a ) .+ ( w .x. b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) )
176	172, 175	eqeq12d 2637	. . . . . . . . . 10 |- ( w = c -> ( ( w .x. ( a .+^ b ) ) = ( ( w .x. a ) .+ ( w .x. b ) ) <-> ( c .x. ( a .+^ b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) ) )
177	166, 171, 176	rspc3v 3325	. . . . . . . . 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 ) ) ) )
178	161, 177	syl5com 31	. . . . . . . 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 ) ) ) )
179	159, 178	sylbi 207	. . . . . . 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 ) ) ) )
180	158, 179	syl 17	. . . . . 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 ) ) ) )
181	180	3ad2ant3 1084	. . . . 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 ) ) ) )
182	43, 181	ax-mp 5	. . . 4 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( a .+^ b ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) )
183	48	a1i 11	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
184		oveq12 6659	. . . . . . 7 |- ( ( v = c /\ s = ( a .+^ b ) ) -> ( v .x. s ) = ( c .x. ( a .+^ b ) ) )
185	184	ancoms 469	. . . . . 6 |- ( ( s = ( a .+^ b ) /\ v = c ) -> ( v .x. s ) = ( c .x. ( a .+^ b ) ) )
186	185	adantl 482	. . . . 5 |- ( ( ( a e. K /\ b e. K /\ c e. V ) /\ ( s = ( a .+^ b ) /\ v = c ) ) -> ( v .x. s ) = ( c .x. ( a .+^ b ) ) )
187	45, 58	grpcl 17430	. . . . . . . . . 10 |- ( ( F e. Grp /\ a e. K /\ b e. K ) -> ( a .+^ b ) e. K )
188	187	3expib 1268	. . . . . . . . 9 |- ( F e. Grp -> ( ( a e. K /\ b e. K ) -> ( a .+^ b ) e. K ) )
189	82, 188	syl 17	. . . . . . . 8 |- ( F e. Ring -> ( ( a e. K /\ b e. K ) -> ( a .+^ b ) e. K ) )
190	189	3ad2ant2 1083	. . . . . . 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 ) )
191	43, 190	ax-mp 5	. . . . . 6 |- ( ( a e. K /\ b e. K ) -> ( a .+^ b ) e. K )
192	191	3adant3 1081	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .+^ b ) e. K )
193		simp3 1063	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> c e. V )
194		ovexd 6680	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( a .+^ b ) ) e. _V )
195	183, 186, 192, 193, 194	ovmpt2d 6788	. . . 4 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( a .+^ b ) .* c ) = ( c .x. ( a .+^ b ) ) )
196	148	adantl 482	. . . . . 6 |- ( ( ( a e. K /\ b e. K /\ c e. V ) /\ ( s = a /\ v = c ) ) -> ( v .x. s ) = ( c .x. a ) )
197		simp1 1061	. . . . . 6 |- ( ( a e. K /\ b e. K /\ c e. V ) -> a e. K )
198		ovexd 6680	. . . . . 6 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. a ) e. _V )
199	183, 196, 197, 193, 198	ovmpt2d 6788	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .* c ) = ( c .x. a ) )
200		oveq12 6659	. . . . . . . 8 |- ( ( v = c /\ s = b ) -> ( v .x. s ) = ( c .x. b ) )
201	200	ancoms 469	. . . . . . 7 |- ( ( s = b /\ v = c ) -> ( v .x. s ) = ( c .x. b ) )
202	201	adantl 482	. . . . . 6 |- ( ( ( a e. K /\ b e. K /\ c e. V ) /\ ( s = b /\ v = c ) ) -> ( v .x. s ) = ( c .x. b ) )
203		simp2 1062	. . . . . 6 |- ( ( a e. K /\ b e. K /\ c e. V ) -> b e. K )
204		ovexd 6680	. . . . . 6 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. b ) e. _V )
205	183, 202, 203, 193, 204	ovmpt2d 6788	. . . . 5 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( b .* c ) = ( c .x. b ) )
206	199, 205	oveq12d 6668	. . . 4 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( a .* c ) .+ ( b .* c ) ) = ( ( c .x. a ) .+ ( c .x. b ) ) )
207	182, 195, 206	3eqtr4d 2666	. . 3 |- ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( a .+^ b ) .* c ) = ( ( a .* c ) .+ ( b .* c ) ) )
208	207	adantl 482	. 2 |- ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( ( a .+^ b ) .* c ) = ( ( a .* c ) .+ ( b .* c ) ) )
209		rmodislmod.s	. . 3 |- .x. = ( .s ` R )
210	1, 27, 209, 39, 45, 58, 60, 62, 43, 48, 14	rmodislmodlem 18930	. 2 |- ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( ( a .X. b ) .* c ) = ( a .* ( b .* c ) ) )
211	48	a1i 11	. . . 4 |- ( ( F e. CRing /\ a e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
212		oveq12 6659	. . . . . 6 |- ( ( v = a /\ s = .1. ) -> ( v .x. s ) = ( a .x. .1. ) )
213	212	ancoms 469	. . . . 5 |- ( ( s = .1. /\ v = a ) -> ( v .x. s ) = ( a .x. .1. ) )
214	213	adantl 482	. . . 4 |- ( ( ( F e. CRing /\ a e. V ) /\ ( s = .1. /\ v = a ) ) -> ( v .x. s ) = ( a .x. .1. ) )
215	45, 62	ringidcl 18568	. . . . . 6 |- ( F e. Ring -> .1. e. K )
216	64, 215	syl 17	. . . . 5 |- ( F e. CRing -> .1. e. K )
217	216	adantr 481	. . . 4 |- ( ( F e. CRing /\ a e. V ) -> .1. e. K )
218		simpr 477	. . . 4 |- ( ( F e. CRing /\ a e. V ) -> a e. V )
219		ovexd 6680	. . . 4 |- ( ( F e. CRing /\ a e. V ) -> ( a .x. .1. ) e. _V )
220	211, 214, 217, 218, 219	ovmpt2d 6788	. . 3 |- ( ( F e. CRing /\ a e. V ) -> ( .1. .* a ) = ( a .x. .1. ) )
221		simprr 796	. . . . . . . 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 )
222	221	2ralimi 2953	. . . . . . 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 )
223	222	2ralimi 2953	. . . . . 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 )
224		rspn0 3934	. . . . . . 7 |- ( K =/= (/) -> ( 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 ) )
225	86, 224	ax-mp 5	. . . . . 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 )
226		rspn0 3934	. . . . . . . 8 |- ( K =/= (/) -> ( A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w -> A. x e. V A. w e. V ( w .x. .1. ) = w ) )
227	86, 226	ax-mp 5	. . . . . . 7 |- ( A. r e. K A. x e. V A. w e. V ( w .x. .1. ) = w -> A. x e. V A. w e. V ( w .x. .1. ) = w )
228		rspn0 3934	. . . . . . . . 9 |- ( V =/= (/) -> ( A. x e. V A. w e. V ( w .x. .1. ) = w -> A. w e. V ( w .x. .1. ) = w ) )
229	92, 228	ax-mp 5	. . . . . . . 8 |- ( A. x e. V A. w e. V ( w .x. .1. ) = w -> A. w e. V ( w .x. .1. ) = w )
230		oveq1 6657	. . . . . . . . . . 11 |- ( w = a -> ( w .x. .1. ) = ( a .x. .1. ) )
231		id 22	. . . . . . . . . . 11 |- ( w = a -> w = a )
232	230, 231	eqeq12d 2637	. . . . . . . . . 10 |- ( w = a -> ( ( w .x. .1. ) = w <-> ( a .x. .1. ) = a ) )
233	232	rspcv 3305	. . . . . . . . 9 |- ( a e. V -> ( A. w e. V ( w .x. .1. ) = w -> ( a .x. .1. ) = a ) )
234	233	adantl 482	. . . . . . . 8 |- ( ( F e. CRing /\ a e. V ) -> ( A. w e. V ( w .x. .1. ) = w -> ( a .x. .1. ) = a ) )
235	229, 234	syl5com 31	. . . . . . 7 |- ( A. x e. V A. w e. V ( w .x. .1. ) = w -> ( ( F e. CRing /\ a e. V ) -> ( a .x. .1. ) = a ) )
236	227, 235	syl 17	. . . . . 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 ) )
237	223, 225, 236	3syl 18	. . . . 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 ) )
238	237	3ad2ant3 1084	. . . 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 ) )
239	43, 238	ax-mp 5	. . 3 |- ( ( F e. CRing /\ a e. V ) -> ( a .x. .1. ) = a )
240	220, 239	eqtrd 2656	. 2 |- ( ( F e. CRing /\ a e. V ) -> ( .1. .* a ) = a )
241	18, 30, 42, 56, 57, 59, 61, 63, 64, 70, 106, 155, 208, 210, 240	islmodd 18869	1 |- ( F e. CRing -> L e. LMod )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   _Vcvv 3200   (/)c0 3915   <.cop 4183   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   1c1 9937   2c2 11070   5c5 11073   6c6 11074   ndxcnx 15854   sSet csts 15855   Basecbs 15857   +g cplusg 15941   .rcmulr 15942  Scalarcsca 15944   .scvsca 15945   Grpcgrp 17422   1rcur 18501   Ringcrg 18547   CRingccrg 18548   LModclmod 18863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-plusg 15954  df-sca 15957  df-vsca 15958  df-0g 16102  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-grp 17425  df-cmn 18195  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-lmod 18865

This theorem is referenced by: (None)