Theorem isslmd 29755

Description: The predicate "is a semimodule". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)

Hypotheses

Ref	Expression
isslmd.v	|- V = ( Base ` W )
isslmd.a	|- .+ = ( +g ` W )
isslmd.s	|- .x. = ( .s ` W )
isslmd.0	|- .0. = ( 0g ` W )
isslmd.f	|- F = (Scalar ` W )
isslmd.k	|- K = ( Base ` F )
isslmd.p	|- .+^ = ( +g ` F )
isslmd.t	|- .X. = ( .r ` F )
isslmd.u	|- .1. = ( 1r ` F )
isslmd.o	|- O = ( 0g ` F )

Assertion

Ref	Expression
isslmd	|- ( W e. SLMod <-> ( W e. CMnd /\ F e. SRing /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )

Distinct variable groups:   r, q, w, x, .X.   .+ , q, r, w, x   .+^ , q, r, w, x   .1. , q, r, w, x   .x. , q, r, w, x   F, q, r, w, x   K, q, r, w, x   V, q, r, w, x   W, q, r, w, x   .0. , q, r, w, x   O, q, r, w, x

Proof of Theorem isslmd

Dummy variables f a g k p s t v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvex 6201	. . . . 5 |- ( Base ` g ) e. _V
2		fvex 6201	. . . . 5 |- ( +g ` g ) e. _V
3		fvex 6201	. . . . . . 7 |- ( .s ` g ) e. _V
4		fvex 6201	. . . . . . 7 |- (Scalar ` g ) e. _V
5		fvex 6201	. . . . . . . . 9 |- ( Base ` f ) e. _V
6		fvex 6201	. . . . . . . . 9 |- ( +g ` f ) e. _V
7		fvex 6201	. . . . . . . . 9 |- ( .r ` f ) e. _V
8		simp1 1061	. . . . . . . . . . 11 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> k = ( Base ` f ) )
9		simp2 1062	. . . . . . . . . . . . . . . . . 18 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> p = ( +g ` f ) )
10	9	oveqd 6667	. . . . . . . . . . . . . . . . 17 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( q p r ) = ( q ( +g ` f ) r ) )
11	10	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( ( q p r ) s w ) = ( ( q ( +g ` f ) r ) s w ) )
12	11	eqeq1d 2624	. . . . . . . . . . . . . . 15 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) <-> ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) )
13	12	3anbi3d 1405	. . . . . . . . . . . . . 14 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) <-> ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) ) )
14		simp3 1063	. . . . . . . . . . . . . . . . . 18 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> t = ( .r ` f ) )
15	14	oveqd 6667	. . . . . . . . . . . . . . . . 17 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( q t r ) = ( q ( .r ` f ) r ) )
16	15	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( ( q t r ) s w ) = ( ( q ( .r ` f ) r ) s w ) )
17	16	eqeq1d 2624	. . . . . . . . . . . . . . 15 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( ( ( q t r ) s w ) = ( q s ( r s w ) ) <-> ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) ) )
18	17	3anbi1d 1403	. . . . . . . . . . . . . 14 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) <-> ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) )
19	13, 18	anbi12d 747	. . . . . . . . . . . . 13 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) <-> ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) )
20	19	2ralbidv 2989	. . . . . . . . . . . 12 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) <-> A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) )
21	8, 20	raleqbidv 3152	. . . . . . . . . . 11 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) <-> A. r e. ( Base ` f ) A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) )
22	8, 21	raleqbidv 3152	. . . . . . . . . 10 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) <-> A. q e. ( Base ` f ) A. r e. ( Base ` f ) A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) )
23	22	anbi2d 740	. . . . . . . . 9 |- ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( ( f e. SRing /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) <-> ( f e. SRing /\ A. q e. ( Base ` f ) A. r e. ( Base ` f ) A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) ) )
24	5, 6, 7, 23	sbc3ie 3507	. . . . . . . 8 |- ( [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) <-> ( f e. SRing /\ A. q e. ( Base ` f ) A. r e. ( Base ` f ) A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) )
25		simpr 477	. . . . . . . . . 10 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> f = (Scalar ` g ) )
26	25	eleq1d 2686	. . . . . . . . 9 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( f e. SRing <-> (Scalar ` g ) e. SRing ) )
27	25	fveq2d 6195	. . . . . . . . . 10 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( Base ` f ) = ( Base ` (Scalar ` g ) ) )
28		simpl 473	. . . . . . . . . . . . . . . 16 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> s = ( .s ` g ) )
29	28	oveqd 6667	. . . . . . . . . . . . . . 15 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( r s w ) = ( r ( .s ` g ) w ) )
30	29	eleq1d 2686	. . . . . . . . . . . . . 14 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( r s w ) e. v <-> ( r ( .s ` g ) w ) e. v ) )
31	28	oveqd 6667	. . . . . . . . . . . . . . 15 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( r s ( w a x ) ) = ( r ( .s ` g ) ( w a x ) ) )
32	28	oveqd 6667	. . . . . . . . . . . . . . . 16 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( r s x ) = ( r ( .s ` g ) x ) )
33	29, 32	oveq12d 6668	. . . . . . . . . . . . . . 15 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( r s w ) a ( r s x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) )
34	31, 33	eqeq12d 2637	. . . . . . . . . . . . . 14 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) <-> ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) ) )
35	25	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( +g ` f ) = ( +g ` (Scalar ` g ) ) )
36	35	oveqd 6667	. . . . . . . . . . . . . . . 16 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( q ( +g ` f ) r ) = ( q ( +g ` (Scalar ` g ) ) r ) )
37		eqidd 2623	. . . . . . . . . . . . . . . 16 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> w = w )
38	28, 36, 37	oveq123d 6671	. . . . . . . . . . . . . . 15 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( q ( +g ` f ) r ) s w ) = ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) )
39	28	oveqd 6667	. . . . . . . . . . . . . . . 16 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( q s w ) = ( q ( .s ` g ) w ) )
40	39, 29	oveq12d 6668	. . . . . . . . . . . . . . 15 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( q s w ) a ( r s w ) ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) )
41	38, 40	eqeq12d 2637	. . . . . . . . . . . . . 14 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) <-> ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) )
42	30, 34, 41	3anbi123d 1399	. . . . . . . . . . . . 13 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) <-> ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) ) )
43	25	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( .r ` f ) = ( .r ` (Scalar ` g ) ) )
44	43	oveqd 6667	. . . . . . . . . . . . . . . 16 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( q ( .r ` f ) r ) = ( q ( .r ` (Scalar ` g ) ) r ) )
45	28, 44, 37	oveq123d 6671	. . . . . . . . . . . . . . 15 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( q ( .r ` f ) r ) s w ) = ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) )
46		eqidd 2623	. . . . . . . . . . . . . . . 16 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> q = q )
47	28, 46, 29	oveq123d 6671	. . . . . . . . . . . . . . 15 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( q s ( r s w ) ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) )
48	45, 47	eqeq12d 2637	. . . . . . . . . . . . . 14 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) <-> ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) ) )
49	25	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( 1r ` f ) = ( 1r ` (Scalar ` g ) ) )
50	28, 49, 37	oveq123d 6671	. . . . . . . . . . . . . . 15 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( 1r ` f ) s w ) = ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) )
51	50	eqeq1d 2624	. . . . . . . . . . . . . 14 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( ( 1r ` f ) s w ) = w <-> ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w ) )
52	25	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( 0g ` f ) = ( 0g ` (Scalar ` g ) ) )
53	28, 52, 37	oveq123d 6671	. . . . . . . . . . . . . . 15 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( 0g ` f ) s w ) = ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) )
54	53	eqeq1d 2624	. . . . . . . . . . . . . 14 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( ( 0g ` f ) s w ) = ( 0g ` g ) <-> ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) )
55	48, 51, 54	3anbi123d 1399	. . . . . . . . . . . . 13 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) <-> ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) )
56	42, 55	anbi12d 747	. . . . . . . . . . . 12 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) <-> ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) )
57	56	2ralbidv 2989	. . . . . . . . . . 11 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) <-> A. x e. v A. w e. v ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) )
58	27, 57	raleqbidv 3152	. . . . . . . . . 10 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( A. r e. ( Base ` f ) A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) <-> A. r e. ( Base ` (Scalar ` g ) ) A. x e. v A. w e. v ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) )
59	27, 58	raleqbidv 3152	. . . . . . . . 9 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( A. q e. ( Base ` f ) A. r e. ( Base ` f ) A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) <-> A. q e. ( Base ` (Scalar ` g ) ) A. r e. ( Base ` (Scalar ` g ) ) A. x e. v A. w e. v ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) )
60	26, 59	anbi12d 747	. . . . . . . 8 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( ( f e. SRing /\ A. q e. ( Base ` f ) A. r e. ( Base ` f ) A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q ( +g ` f ) r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q ( .r ` f ) r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) <-> ( (Scalar ` g ) e. SRing /\ A. q e. ( Base ` (Scalar ` g ) ) A. r e. ( Base ` (Scalar ` g ) ) A. x e. v A. w e. v ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) ) )
61	24, 60	syl5bb 272	. . . . . . 7 |- ( ( s = ( .s ` g ) /\ f = (Scalar ` g ) ) -> ( [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) <-> ( (Scalar ` g ) e. SRing /\ A. q e. ( Base ` (Scalar ` g ) ) A. r e. ( Base ` (Scalar ` g ) ) A. x e. v A. w e. v ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) ) )
62	3, 4, 61	sbc2ie 3505	. . . . . 6 |- ( [. ( .s ` g ) / s ]. [. (Scalar ` g ) / f ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) <-> ( (Scalar ` g ) e. SRing /\ A. q e. ( Base ` (Scalar ` g ) ) A. r e. ( Base ` (Scalar ` g ) ) A. x e. v A. w e. v ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) )
63		simpl 473	. . . . . . . . 9 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> v = ( Base ` g ) )
64	63	eleq2d 2687	. . . . . . . . . . . 12 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( ( r ( .s ` g ) w ) e. v <-> ( r ( .s ` g ) w ) e. ( Base ` g ) ) )
65		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> a = ( +g ` g ) )
66	65	oveqd 6667	. . . . . . . . . . . . . 14 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( w a x ) = ( w ( +g ` g ) x ) )
67	66	oveq2d 6666	. . . . . . . . . . . . 13 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( r ( .s ` g ) ( w a x ) ) = ( r ( .s ` g ) ( w ( +g ` g ) x ) ) )
68	65	oveqd 6667	. . . . . . . . . . . . 13 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) )
69	67, 68	eqeq12d 2637	. . . . . . . . . . . 12 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) <-> ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) ) )
70	65	oveqd 6667	. . . . . . . . . . . . 13 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) )
71	70	eqeq2d 2632	. . . . . . . . . . . 12 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) <-> ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) )
72	64, 69, 71	3anbi123d 1399	. . . . . . . . . . 11 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) <-> ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) ) )
73	72	anbi1d 741	. . . . . . . . . 10 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) <-> ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) )
74	63, 73	raleqbidv 3152	. . . . . . . . 9 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( A. w e. v ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) <-> A. w e. ( Base ` g ) ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) )
75	63, 74	raleqbidv 3152	. . . . . . . 8 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( A. x e. v A. w e. v ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) <-> A. x e. ( Base ` g ) A. w e. ( Base ` g ) ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) )
76	75	2ralbidv 2989	. . . . . . 7 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( A. q e. ( Base ` (Scalar ` g ) ) A. r e. ( Base ` (Scalar ` g ) ) A. x e. v A. w e. v ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) <-> A. q e. ( Base ` (Scalar ` g ) ) A. r e. ( Base ` (Scalar ` g ) ) A. x e. ( Base ` g ) A. w e. ( Base ` g ) ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) )
77	76	anbi2d 740	. . . . . 6 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( ( (Scalar ` g ) e. SRing /\ A. q e. ( Base ` (Scalar ` g ) ) A. r e. ( Base ` (Scalar ` g ) ) A. x e. v A. w e. v ( ( ( r ( .s ` g ) w ) e. v /\ ( r ( .s ` g ) ( w a x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) <-> ( (Scalar ` g ) e. SRing /\ A. q e. ( Base ` (Scalar ` g ) ) A. r e. ( Base ` (Scalar ` g ) ) A. x e. ( Base ` g ) A. w e. ( Base ` g ) ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) ) )
78	62, 77	syl5bb 272	. . . . 5 |- ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( [. ( .s ` g ) / s ]. [. (Scalar ` g ) / f ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) <-> ( (Scalar ` g ) e. SRing /\ A. q e. ( Base ` (Scalar ` g ) ) A. r e. ( Base ` (Scalar ` g ) ) A. x e. ( Base ` g ) A. w e. ( Base ` g ) ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) ) )
79	1, 2, 78	sbc2ie 3505	. . . 4 |- ( [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. ( .s ` g ) / s ]. [. (Scalar ` g ) / f ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) <-> ( (Scalar ` g ) e. SRing /\ A. q e. ( Base ` (Scalar ` g ) ) A. r e. ( Base ` (Scalar ` g ) ) A. x e. ( Base ` g ) A. w e. ( Base ` g ) ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) )
80		fveq2 6191	. . . . . . 7 |- ( g = W -> (Scalar ` g ) = (Scalar ` W ) )
81		isslmd.f	. . . . . . 7 |- F = (Scalar ` W )
82	80, 81	syl6eqr 2674	. . . . . 6 |- ( g = W -> (Scalar ` g ) = F )
83	82	eleq1d 2686	. . . . 5 |- ( g = W -> ( (Scalar ` g ) e. SRing <-> F e. SRing ) )
84	82	fveq2d 6195	. . . . . . 7 |- ( g = W -> ( Base ` (Scalar ` g ) ) = ( Base ` F ) )
85		isslmd.k	. . . . . . 7 |- K = ( Base ` F )
86	84, 85	syl6eqr 2674	. . . . . 6 |- ( g = W -> ( Base ` (Scalar ` g ) ) = K )
87		fveq2 6191	. . . . . . . . 9 |- ( g = W -> ( Base ` g ) = ( Base ` W ) )
88		isslmd.v	. . . . . . . . 9 |- V = ( Base ` W )
89	87, 88	syl6eqr 2674	. . . . . . . 8 |- ( g = W -> ( Base ` g ) = V )
90		fveq2 6191	. . . . . . . . . . . . . 14 |- ( g = W -> ( .s ` g ) = ( .s ` W ) )
91		isslmd.s	. . . . . . . . . . . . . 14 |- .x. = ( .s ` W )
92	90, 91	syl6eqr 2674	. . . . . . . . . . . . 13 |- ( g = W -> ( .s ` g ) = .x. )
93	92	oveqd 6667	. . . . . . . . . . . 12 |- ( g = W -> ( r ( .s ` g ) w ) = ( r .x. w ) )
94	93, 89	eleq12d 2695	. . . . . . . . . . 11 |- ( g = W -> ( ( r ( .s ` g ) w ) e. ( Base ` g ) <-> ( r .x. w ) e. V ) )
95		eqidd 2623	. . . . . . . . . . . . 13 |- ( g = W -> r = r )
96		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( g = W -> ( +g ` g ) = ( +g ` W ) )
97		isslmd.a	. . . . . . . . . . . . . . 15 |- .+ = ( +g ` W )
98	96, 97	syl6eqr 2674	. . . . . . . . . . . . . 14 |- ( g = W -> ( +g ` g ) = .+ )
99	98	oveqd 6667	. . . . . . . . . . . . 13 |- ( g = W -> ( w ( +g ` g ) x ) = ( w .+ x ) )
100	92, 95, 99	oveq123d 6671	. . . . . . . . . . . 12 |- ( g = W -> ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( r .x. ( w .+ x ) ) )
101	92	oveqd 6667	. . . . . . . . . . . . 13 |- ( g = W -> ( r ( .s ` g ) x ) = ( r .x. x ) )
102	98, 93, 101	oveq123d 6671	. . . . . . . . . . . 12 |- ( g = W -> ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) )
103	100, 102	eqeq12d 2637	. . . . . . . . . . 11 |- ( g = W -> ( ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) <-> ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) ) )
104	82	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( g = W -> ( +g ` (Scalar ` g ) ) = ( +g ` F ) )
105		isslmd.p	. . . . . . . . . . . . . . 15 |- .+^ = ( +g ` F )
106	104, 105	syl6eqr 2674	. . . . . . . . . . . . . 14 |- ( g = W -> ( +g ` (Scalar ` g ) ) = .+^ )
107	106	oveqd 6667	. . . . . . . . . . . . 13 |- ( g = W -> ( q ( +g ` (Scalar ` g ) ) r ) = ( q .+^ r ) )
108		eqidd 2623	. . . . . . . . . . . . 13 |- ( g = W -> w = w )
109	92, 107, 108	oveq123d 6671	. . . . . . . . . . . 12 |- ( g = W -> ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q .+^ r ) .x. w ) )
110	92	oveqd 6667	. . . . . . . . . . . . 13 |- ( g = W -> ( q ( .s ` g ) w ) = ( q .x. w ) )
111	98, 110, 93	oveq123d 6671	. . . . . . . . . . . 12 |- ( g = W -> ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) = ( ( q .x. w ) .+ ( r .x. w ) ) )
112	109, 111	eqeq12d 2637	. . . . . . . . . . 11 |- ( g = W -> ( ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) <-> ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) )
113	94, 103, 112	3anbi123d 1399	. . . . . . . . . 10 |- ( g = W -> ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) <-> ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) ) )
114	82	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( g = W -> ( .r ` (Scalar ` g ) ) = ( .r ` F ) )
115		isslmd.t	. . . . . . . . . . . . . . 15 |- .X. = ( .r ` F )
116	114, 115	syl6eqr 2674	. . . . . . . . . . . . . 14 |- ( g = W -> ( .r ` (Scalar ` g ) ) = .X. )
117	116	oveqd 6667	. . . . . . . . . . . . 13 |- ( g = W -> ( q ( .r ` (Scalar ` g ) ) r ) = ( q .X. r ) )
118	92, 117, 108	oveq123d 6671	. . . . . . . . . . . 12 |- ( g = W -> ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q .X. r ) .x. w ) )
119		eqidd 2623	. . . . . . . . . . . . 13 |- ( g = W -> q = q )
120	92, 119, 93	oveq123d 6671	. . . . . . . . . . . 12 |- ( g = W -> ( q ( .s ` g ) ( r ( .s ` g ) w ) ) = ( q .x. ( r .x. w ) ) )
121	118, 120	eqeq12d 2637	. . . . . . . . . . 11 |- ( g = W -> ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) <-> ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) ) )
122	82	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( g = W -> ( 1r ` (Scalar ` g ) ) = ( 1r ` F ) )
123		isslmd.u	. . . . . . . . . . . . . 14 |- .1. = ( 1r ` F )
124	122, 123	syl6eqr 2674	. . . . . . . . . . . . 13 |- ( g = W -> ( 1r ` (Scalar ` g ) ) = .1. )
125	92, 124, 108	oveq123d 6671	. . . . . . . . . . . 12 |- ( g = W -> ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = ( .1. .x. w ) )
126	125	eqeq1d 2624	. . . . . . . . . . 11 |- ( g = W -> ( ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w <-> ( .1. .x. w ) = w ) )
127	82	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( g = W -> ( 0g ` (Scalar ` g ) ) = ( 0g ` F ) )
128		isslmd.o	. . . . . . . . . . . . . 14 |- O = ( 0g ` F )
129	127, 128	syl6eqr 2674	. . . . . . . . . . . . 13 |- ( g = W -> ( 0g ` (Scalar ` g ) ) = O )
130	92, 129, 108	oveq123d 6671	. . . . . . . . . . . 12 |- ( g = W -> ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( O .x. w ) )
131		fveq2 6191	. . . . . . . . . . . . 13 |- ( g = W -> ( 0g ` g ) = ( 0g ` W ) )
132		isslmd.0	. . . . . . . . . . . . 13 |- .0. = ( 0g ` W )
133	131, 132	syl6eqr 2674	. . . . . . . . . . . 12 |- ( g = W -> ( 0g ` g ) = .0. )
134	130, 133	eqeq12d 2637	. . . . . . . . . . 11 |- ( g = W -> ( ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) <-> ( O .x. w ) = .0. ) )
135	121, 126, 134	3anbi123d 1399	. . . . . . . . . 10 |- ( g = W -> ( ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) <-> ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) )
136	113, 135	anbi12d 747	. . . . . . . . 9 |- ( g = W -> ( ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) <-> ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )
137	89, 136	raleqbidv 3152	. . . . . . . 8 |- ( g = W -> ( A. w e. ( Base ` g ) ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) <-> A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )
138	89, 137	raleqbidv 3152	. . . . . . 7 |- ( g = W -> ( A. x e. ( Base ` g ) A. w e. ( Base ` g ) ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) <-> A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )
139	86, 138	raleqbidv 3152	. . . . . 6 |- ( g = W -> ( A. r e. ( Base ` (Scalar ` g ) ) A. x e. ( Base ` g ) A. w e. ( Base ` g ) ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) <-> A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )
140	86, 139	raleqbidv 3152	. . . . 5 |- ( g = W -> ( A. q e. ( Base ` (Scalar ` g ) ) A. r e. ( Base ` (Scalar ` g ) ) A. x e. ( Base ` g ) A. w e. ( Base ` g ) ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) <-> A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )
141	83, 140	anbi12d 747	. . . 4 |- ( g = W -> ( ( (Scalar ` g ) e. SRing /\ A. q e. ( Base ` (Scalar ` g ) ) A. r e. ( Base ` (Scalar ` g ) ) A. x e. ( Base ` g ) A. w e. ( Base ` g ) ( ( ( r ( .s ` g ) w ) e. ( Base ` g ) /\ ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) /\ ( ( q ( +g ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) ) /\ ( ( ( q ( .r ` (Scalar ` g ) ) r ) ( .s ` g ) w ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) /\ ( ( 1r ` (Scalar ` g ) ) ( .s ` g ) w ) = w /\ ( ( 0g ` (Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) ) ) <-> ( F e. SRing /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) ) )
142	79, 141	syl5bb 272	. . 3 |- ( g = W -> ( [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. ( .s ` g ) / s ]. [. (Scalar ` g ) / f ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) <-> ( F e. SRing /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) ) )
143		df-slmd 29754	. . 3 |- SLMod = { g e. CMnd | [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. ( .s ` g ) / s ]. [. (Scalar ` g ) / f ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) }
144	142, 143	elrab2 3366	. 2 |- ( W e. SLMod <-> ( W e. CMnd /\ ( F e. SRing /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) ) )
145		3anass 1042	. 2 |- ( ( W e. CMnd /\ F e. SRing /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) <-> ( W e. CMnd /\ ( F e. SRing /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) ) )
146	144, 145	bitr4i 267	1 |- ( W e. SLMod <-> ( W e. CMnd /\ F e. SRing /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   [.wsbc 3435   ` cfv 5888  (class class class)co 6650   Basecbs 15857   +g cplusg 15941   .rcmulr 15942  Scalarcsca 15944   .scvsca 15945   0gc0g 16100  CMndccmn 18193   1rcur 18501  SRingcsrg 18505  SLModcslmd 29753

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-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-slmd 29754

This theorem is referenced by:  slmdlema  29756  lmodslmd  29757  slmdcmn  29758  slmdsrg  29760  xrge0slmod  29844