Metamath Proof Explorer

Theorem isslmd

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)

Ref Expression
Hypotheses 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 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. ) ) ) )

Proof

Step Hyp Ref Expression
1 isslmd.v 
 |-  V = ( Base ` W )
2 isslmd.a 
 |-  .+ = ( +g ` W )
3 isslmd.s 
 |-  .x. = ( .s ` W )
4 isslmd.0 
 |-  .0. = ( 0g ` W )
5 isslmd.f 
 |-  F = ( Scalar ` W )
6 isslmd.k 
 |-  K = ( Base ` F )
7 isslmd.p 
 |-  .+^ = ( +g ` F )
8 isslmd.t 
 |-  .X. = ( .r ` F )
9 isslmd.u 
 |-  .1. = ( 1r ` F )
10 isslmd.o 
 |-  O = ( 0g ` F )
11 fvex 
 |-  ( Base ` g ) e. _V
12 fvex 
 |-  ( +g ` g ) e. _V
13 fvex 
 |-  ( .s ` g ) e. _V
14 fvex 
 |-  ( Scalar ` g ) e. _V
15 fvex 
 |-  ( Base ` f ) e. _V
16 fvex 
 |-  ( +g ` f ) e. _V
17 fvex 
 |-  ( .r ` f ) e. _V
18 simp1 
 |-  ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> k = ( Base ` f ) )
19 simp2 
 |-  ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> p = ( +g ` f ) )
20 19 oveqd 
 |-  ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( q p r ) = ( q ( +g ` f ) r ) )
21 20 oveq1d 
 |-  ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( ( q p r ) s w ) = ( ( q ( +g ` f ) r ) s w ) )
22 21 eqeq1d 
 |-  ( ( 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 ) ) ) )
23 22 3anbi3d 
 |-  ( ( 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 ) ) ) ) )
24 simp3 
 |-  ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> t = ( .r ` f ) )
25 24 oveqd 
 |-  ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( q t r ) = ( q ( .r ` f ) r ) )
26 25 oveq1d 
 |-  ( ( k = ( Base ` f ) /\ p = ( +g ` f ) /\ t = ( .r ` f ) ) -> ( ( q t r ) s w ) = ( ( q ( .r ` f ) r ) s w ) )
27 26 eqeq1d 
 |-  ( ( 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 ) ) ) )
28 27 3anbi1d 
 |-  ( ( 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 ) ) ) )
29 23 28 anbi12d 
 |-  ( ( 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 ) ) ) ) )
30 29 2ralbidv 
 |-  ( ( 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 ) ) ) ) )
31 18 30 raleqbidv 
 |-  ( ( 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 ) ) ) ) )
32 18 31 raleqbidv 
 |-  ( ( 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 ) ) ) ) )
33 32 anbi2d 
 |-  ( ( 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 ) ) ) ) ) )
34 15 16 17 33 sbc3ie 
 |-  ( [. ( 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 ) ) ) ) )
35 simpr 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> f = ( Scalar ` g ) )
36 35 eleq1d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( f e. SRing <-> ( Scalar ` g ) e. SRing ) )
37 35 fveq2d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( Base ` f ) = ( Base ` ( Scalar ` g ) ) )
38 simpl 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> s = ( .s ` g ) )
39 38 oveqd 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( r s w ) = ( r ( .s ` g ) w ) )
40 39 eleq1d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( ( r s w ) e. v <-> ( r ( .s ` g ) w ) e. v ) )
41 38 oveqd 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( r s ( w a x ) ) = ( r ( .s ` g ) ( w a x ) ) )
42 38 oveqd 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( r s x ) = ( r ( .s ` g ) x ) )
43 39 42 oveq12d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( ( r s w ) a ( r s x ) ) = ( ( r ( .s ` g ) w ) a ( r ( .s ` g ) x ) ) )
44 41 43 eqeq12d 
 |-  ( ( 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 ) ) ) )
45 35 fveq2d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( +g ` f ) = ( +g ` ( Scalar ` g ) ) )
46 45 oveqd 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( q ( +g ` f ) r ) = ( q ( +g ` ( Scalar ` g ) ) r ) )
47 eqidd 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> w = w )
48 38 46 47 oveq123d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( ( q ( +g ` f ) r ) s w ) = ( ( q ( +g ` ( Scalar ` g ) ) r ) ( .s ` g ) w ) )
49 38 oveqd 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( q s w ) = ( q ( .s ` g ) w ) )
50 49 39 oveq12d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( ( q s w ) a ( r s w ) ) = ( ( q ( .s ` g ) w ) a ( r ( .s ` g ) w ) ) )
51 48 50 eqeq12d 
 |-  ( ( 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 ) ) ) )
52 40 44 51 3anbi123d 
 |-  ( ( 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 ) ) ) ) )
53 35 fveq2d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( .r ` f ) = ( .r ` ( Scalar ` g ) ) )
54 53 oveqd 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( q ( .r ` f ) r ) = ( q ( .r ` ( Scalar ` g ) ) r ) )
55 38 54 47 oveq123d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( ( q ( .r ` f ) r ) s w ) = ( ( q ( .r ` ( Scalar ` g ) ) r ) ( .s ` g ) w ) )
56 eqidd 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> q = q )
57 38 56 39 oveq123d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( q s ( r s w ) ) = ( q ( .s ` g ) ( r ( .s ` g ) w ) ) )
58 55 57 eqeq12d 
 |-  ( ( 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 ) ) ) )
59 35 fveq2d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( 1r ` f ) = ( 1r ` ( Scalar ` g ) ) )
60 38 59 47 oveq123d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( ( 1r ` f ) s w ) = ( ( 1r ` ( Scalar ` g ) ) ( .s ` g ) w ) )
61 60 eqeq1d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( ( ( 1r ` f ) s w ) = w <-> ( ( 1r ` ( Scalar ` g ) ) ( .s ` g ) w ) = w ) )
62 35 fveq2d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( 0g ` f ) = ( 0g ` ( Scalar ` g ) ) )
63 38 62 47 oveq123d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( ( 0g ` f ) s w ) = ( ( 0g ` ( Scalar ` g ) ) ( .s ` g ) w ) )
64 63 eqeq1d 
 |-  ( ( s = ( .s ` g ) /\ f = ( Scalar ` g ) ) -> ( ( ( 0g ` f ) s w ) = ( 0g ` g ) <-> ( ( 0g ` ( Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) ) )
65 58 61 64 3anbi123d 
 |-  ( ( 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 ) ) ) )
66 52 65 anbi12d 
 |-  ( ( 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 ) ) ) ) )
67 66 2ralbidv 
 |-  ( ( 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 ) ) ) ) )
68 37 67 raleqbidv 
 |-  ( ( 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 ) ) ) ) )
69 37 68 raleqbidv 
 |-  ( ( 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 ) ) ) ) )
70 36 69 anbi12d 
 |-  ( ( 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 ) ) ) ) ) )
71 34 70 syl5bb 
 |-  ( ( 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 ) ) ) ) ) )
72 13 14 71 sbc2ie 
 |-  ( [. ( .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 ) ) ) ) )
73 simpl 
 |-  ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> v = ( Base ` g ) )
74 73 eleq2d 
 |-  ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( ( r ( .s ` g ) w ) e. v <-> ( r ( .s ` g ) w ) e. ( Base ` g ) ) )
75 simpr 
 |-  ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> a = ( +g ` g ) )
76 75 oveqd 
 |-  ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( w a x ) = ( w ( +g ` g ) x ) )
77 76 oveq2d 
 |-  ( ( v = ( Base ` g ) /\ a = ( +g ` g ) ) -> ( r ( .s ` g ) ( w a x ) ) = ( r ( .s ` g ) ( w ( +g ` g ) x ) ) )
78 75 oveqd 
 |-  ( ( 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 ) ) )
79 77 78 eqeq12d 
 |-  ( ( 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 ) ) ) )
80 75 oveqd 
 |-  ( ( 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 ) ) )
81 80 eqeq2d 
 |-  ( ( 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 ) ) ) )
82 74 79 81 3anbi123d 
 |-  ( ( 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 ) ) ) ) )
83 82 anbi1d 
 |-  ( ( 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 ) ) ) ) )
84 73 83 raleqbidv 
 |-  ( ( 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 ) ) ) ) )
85 73 84 raleqbidv 
 |-  ( ( 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 ) ) ) ) )
86 85 2ralbidv 
 |-  ( ( 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 ) ) ) ) )
87 86 anbi2d 
 |-  ( ( 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 ) ) ) ) ) )
88 72 87 syl5bb 
 |-  ( ( 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 ) ) ) ) ) )
89 11 12 88 sbc2ie 
 |-  ( [. ( 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 ) ) ) ) )
90 fveq2 
 |-  ( g = W -> ( Scalar ` g ) = ( Scalar ` W ) )
91 90 5 eqtr4di 
 |-  ( g = W -> ( Scalar ` g ) = F )
92 91 eleq1d 
 |-  ( g = W -> ( ( Scalar ` g ) e. SRing <-> F e. SRing ) )
93 91 fveq2d 
 |-  ( g = W -> ( Base ` ( Scalar ` g ) ) = ( Base ` F ) )
94 93 6 eqtr4di 
 |-  ( g = W -> ( Base ` ( Scalar ` g ) ) = K )
95 fveq2 
 |-  ( g = W -> ( Base ` g ) = ( Base ` W ) )
96 95 1 eqtr4di 
 |-  ( g = W -> ( Base ` g ) = V )
97 fveq2 
 |-  ( g = W -> ( .s ` g ) = ( .s ` W ) )
98 97 3 eqtr4di 
 |-  ( g = W -> ( .s ` g ) = .x. )
99 98 oveqd 
 |-  ( g = W -> ( r ( .s ` g ) w ) = ( r .x. w ) )
100 99 96 eleq12d 
 |-  ( g = W -> ( ( r ( .s ` g ) w ) e. ( Base ` g ) <-> ( r .x. w ) e. V ) )
101 eqidd 
 |-  ( g = W -> r = r )
102 fveq2 
 |-  ( g = W -> ( +g ` g ) = ( +g ` W ) )
103 102 2 eqtr4di 
 |-  ( g = W -> ( +g ` g ) = .+ )
104 103 oveqd 
 |-  ( g = W -> ( w ( +g ` g ) x ) = ( w .+ x ) )
105 98 101 104 oveq123d 
 |-  ( g = W -> ( r ( .s ` g ) ( w ( +g ` g ) x ) ) = ( r .x. ( w .+ x ) ) )
106 98 oveqd 
 |-  ( g = W -> ( r ( .s ` g ) x ) = ( r .x. x ) )
107 103 99 106 oveq123d 
 |-  ( g = W -> ( ( r ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) )
108 105 107 eqeq12d 
 |-  ( 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 ) ) ) )
109 91 fveq2d 
 |-  ( g = W -> ( +g ` ( Scalar ` g ) ) = ( +g ` F ) )
110 109 7 eqtr4di 
 |-  ( g = W -> ( +g ` ( Scalar ` g ) ) = .+^ )
111 110 oveqd 
 |-  ( g = W -> ( q ( +g ` ( Scalar ` g ) ) r ) = ( q .+^ r ) )
112 eqidd 
 |-  ( g = W -> w = w )
113 98 111 112 oveq123d 
 |-  ( g = W -> ( ( q ( +g ` ( Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q .+^ r ) .x. w ) )
114 98 oveqd 
 |-  ( g = W -> ( q ( .s ` g ) w ) = ( q .x. w ) )
115 103 114 99 oveq123d 
 |-  ( g = W -> ( ( q ( .s ` g ) w ) ( +g ` g ) ( r ( .s ` g ) w ) ) = ( ( q .x. w ) .+ ( r .x. w ) ) )
116 113 115 eqeq12d 
 |-  ( 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 ) ) ) )
117 100 108 116 3anbi123d 
 |-  ( 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 ) ) ) ) )
118 91 fveq2d 
 |-  ( g = W -> ( .r ` ( Scalar ` g ) ) = ( .r ` F ) )
119 118 8 eqtr4di 
 |-  ( g = W -> ( .r ` ( Scalar ` g ) ) = .X. )
120 119 oveqd 
 |-  ( g = W -> ( q ( .r ` ( Scalar ` g ) ) r ) = ( q .X. r ) )
121 98 120 112 oveq123d 
 |-  ( g = W -> ( ( q ( .r ` ( Scalar ` g ) ) r ) ( .s ` g ) w ) = ( ( q .X. r ) .x. w ) )
122 eqidd 
 |-  ( g = W -> q = q )
123 98 122 99 oveq123d 
 |-  ( g = W -> ( q ( .s ` g ) ( r ( .s ` g ) w ) ) = ( q .x. ( r .x. w ) ) )
124 121 123 eqeq12d 
 |-  ( 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 ) ) ) )
125 91 fveq2d 
 |-  ( g = W -> ( 1r ` ( Scalar ` g ) ) = ( 1r ` F ) )
126 125 9 eqtr4di 
 |-  ( g = W -> ( 1r ` ( Scalar ` g ) ) = .1. )
127 98 126 112 oveq123d 
 |-  ( g = W -> ( ( 1r ` ( Scalar ` g ) ) ( .s ` g ) w ) = ( .1. .x. w ) )
128 127 eqeq1d 
 |-  ( g = W -> ( ( ( 1r ` ( Scalar ` g ) ) ( .s ` g ) w ) = w <-> ( .1. .x. w ) = w ) )
129 91 fveq2d 
 |-  ( g = W -> ( 0g ` ( Scalar ` g ) ) = ( 0g ` F ) )
130 129 10 eqtr4di 
 |-  ( g = W -> ( 0g ` ( Scalar ` g ) ) = O )
131 98 130 112 oveq123d 
 |-  ( g = W -> ( ( 0g ` ( Scalar ` g ) ) ( .s ` g ) w ) = ( O .x. w ) )
132 fveq2 
 |-  ( g = W -> ( 0g ` g ) = ( 0g ` W ) )
133 132 4 eqtr4di 
 |-  ( g = W -> ( 0g ` g ) = .0. )
134 131 133 eqeq12d 
 |-  ( g = W -> ( ( ( 0g ` ( Scalar ` g ) ) ( .s ` g ) w ) = ( 0g ` g ) <-> ( O .x. w ) = .0. ) )
135 124 128 134 3anbi123d 
 |-  ( 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 117 135 anbi12d 
 |-  ( 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 96 136 raleqbidv 
 |-  ( 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 96 137 raleqbidv 
 |-  ( 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 94 138 raleqbidv 
 |-  ( 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 94 139 raleqbidv 
 |-  ( 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 92 140 anbi12d 
 |-  ( 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 89 141 syl5bb 
 |-  ( 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 
 |-  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 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( 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. ) ) ) )