Metamath Proof Explorer

Theorem islmodd

Description: Properties that determine a left module. See note in isgrpd2 regarding the ph on hypotheses that name structure components. (Contributed by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses islmodd.v 
|- ( ph -> V = ( Base ` W ) )
islmodd.a 
|- ( ph -> .+ = ( +g ` W ) )
islmodd.f 
|- ( ph -> F = ( Scalar ` W ) )
islmodd.s 
|- ( ph -> .x. = ( .s ` W ) )
islmodd.b 
|- ( ph -> B = ( Base ` F ) )
islmodd.p 
|- ( ph -> .+^ = ( +g ` F ) )
islmodd.t 
|- ( ph -> .X. = ( .r ` F ) )
islmodd.u 
|- ( ph -> .1. = ( 1r ` F ) )
islmodd.r 
|- ( ph -> F e. Ring )
islmodd.l 
|- ( ph -> W e. Grp )
islmodd.w 
|- ( ( ph /\ x e. B /\ y e. V ) -> ( x .x. y ) e. V )
islmodd.c 
|- ( ( ph /\ ( x e. B /\ y e. V /\ z e. V ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
islmodd.d 
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. V ) ) -> ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
islmodd.e 
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. V ) ) -> ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
islmodd.g 
|- ( ( ph /\ x e. V ) -> ( .1. .x. x ) = x )
Assertion islmodd 
|- ( ph -> W e. LMod )

Proof

Step Hyp Ref Expression
1 islmodd.v 
 |-  ( ph -> V = ( Base ` W ) )
2 islmodd.a 
 |-  ( ph -> .+ = ( +g ` W ) )
3 islmodd.f 
 |-  ( ph -> F = ( Scalar ` W ) )
4 islmodd.s 
 |-  ( ph -> .x. = ( .s ` W ) )
5 islmodd.b 
 |-  ( ph -> B = ( Base ` F ) )
6 islmodd.p 
 |-  ( ph -> .+^ = ( +g ` F ) )
7 islmodd.t 
 |-  ( ph -> .X. = ( .r ` F ) )
8 islmodd.u 
 |-  ( ph -> .1. = ( 1r ` F ) )
9 islmodd.r 
 |-  ( ph -> F e. Ring )
10 islmodd.l 
 |-  ( ph -> W e. Grp )
11 islmodd.w 
 |-  ( ( ph /\ x e. B /\ y e. V ) -> ( x .x. y ) e. V )
12 islmodd.c 
 |-  ( ( ph /\ ( x e. B /\ y e. V /\ z e. V ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
13 islmodd.d 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. V ) ) -> ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
14 islmodd.e 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. V ) ) -> ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
15 islmodd.g 
 |-  ( ( ph /\ x e. V ) -> ( .1. .x. x ) = x )
16 3 9 eqeltrrd 
 |-  ( ph -> ( Scalar ` W ) e. Ring )
17 11 3expb 
 |-  ( ( ph /\ ( x e. B /\ y e. V ) ) -> ( x .x. y ) e. V )
18 17 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. V ( x .x. y ) e. V )
19 oveq1 
 |-  ( x = r -> ( x .x. y ) = ( r .x. y ) )
20 19 eleq1d 
 |-  ( x = r -> ( ( x .x. y ) e. V <-> ( r .x. y ) e. V ) )
21 oveq2 
 |-  ( y = w -> ( r .x. y ) = ( r .x. w ) )
22 21 eleq1d 
 |-  ( y = w -> ( ( r .x. y ) e. V <-> ( r .x. w ) e. V ) )
23 20 22 rspc2v 
 |-  ( ( r e. B /\ w e. V ) -> ( A. x e. B A. y e. V ( x .x. y ) e. V -> ( r .x. w ) e. V ) )
24 23 ad2ant2l 
 |-  ( ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) -> ( A. x e. B A. y e. V ( x .x. y ) e. V -> ( r .x. w ) e. V ) )
25 18 24 mpan9 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( r .x. w ) e. V )
26 12 ralrimivvva 
 |-  ( ph -> A. x e. B A. y e. V A. z e. V ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
27 oveq1 
 |-  ( x = r -> ( x .x. ( y .+ z ) ) = ( r .x. ( y .+ z ) ) )
28 oveq1 
 |-  ( x = r -> ( x .x. z ) = ( r .x. z ) )
29 19 28 oveq12d 
 |-  ( x = r -> ( ( x .x. y ) .+ ( x .x. z ) ) = ( ( r .x. y ) .+ ( r .x. z ) ) )
30 27 29 eqeq12d 
 |-  ( x = r -> ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) <-> ( r .x. ( y .+ z ) ) = ( ( r .x. y ) .+ ( r .x. z ) ) ) )
31 oveq1 
 |-  ( y = w -> ( y .+ z ) = ( w .+ z ) )
32 31 oveq2d 
 |-  ( y = w -> ( r .x. ( y .+ z ) ) = ( r .x. ( w .+ z ) ) )
33 21 oveq1d 
 |-  ( y = w -> ( ( r .x. y ) .+ ( r .x. z ) ) = ( ( r .x. w ) .+ ( r .x. z ) ) )
34 32 33 eqeq12d 
 |-  ( y = w -> ( ( r .x. ( y .+ z ) ) = ( ( r .x. y ) .+ ( r .x. z ) ) <-> ( r .x. ( w .+ z ) ) = ( ( r .x. w ) .+ ( r .x. z ) ) ) )
35 oveq2 
 |-  ( z = u -> ( w .+ z ) = ( w .+ u ) )
36 35 oveq2d 
 |-  ( z = u -> ( r .x. ( w .+ z ) ) = ( r .x. ( w .+ u ) ) )
37 oveq2 
 |-  ( z = u -> ( r .x. z ) = ( r .x. u ) )
38 37 oveq2d 
 |-  ( z = u -> ( ( r .x. w ) .+ ( r .x. z ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) )
39 36 38 eqeq12d 
 |-  ( z = u -> ( ( r .x. ( w .+ z ) ) = ( ( r .x. w ) .+ ( r .x. z ) ) <-> ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) ) )
40 30 34 39 rspc3v 
 |-  ( ( r e. B /\ w e. V /\ u e. V ) -> ( A. x e. B A. y e. V A. z e. V ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) -> ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) ) )
41 40 3com23 
 |-  ( ( r e. B /\ u e. V /\ w e. V ) -> ( A. x e. B A. y e. V A. z e. V ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) -> ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) ) )
42 41 3expb 
 |-  ( ( r e. B /\ ( u e. V /\ w e. V ) ) -> ( A. x e. B A. y e. V A. z e. V ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) -> ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) ) )
43 42 adantll 
 |-  ( ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) -> ( A. x e. B A. y e. V A. z e. V ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) -> ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) ) )
44 26 43 mpan9 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) )
45 simpll 
 |-  ( ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) -> x e. B )
46 13 3exp2 
 |-  ( ph -> ( x e. B -> ( y e. B -> ( z e. V -> ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) )
47 46 imp43 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. V ) ) -> ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
48 47 ralrimivva 
 |-  ( ( ph /\ x e. B ) -> A. y e. B A. z e. V ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
49 45 48 sylan2 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> A. y e. B A. z e. V ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
50 simprlr 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> r e. B )
51 simprrr 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> w e. V )
52 oveq2 
 |-  ( y = r -> ( x .+^ y ) = ( x .+^ r ) )
53 52 oveq1d 
 |-  ( y = r -> ( ( x .+^ y ) .x. z ) = ( ( x .+^ r ) .x. z ) )
54 oveq1 
 |-  ( y = r -> ( y .x. z ) = ( r .x. z ) )
55 54 oveq2d 
 |-  ( y = r -> ( ( x .x. z ) .+ ( y .x. z ) ) = ( ( x .x. z ) .+ ( r .x. z ) ) )
56 53 55 eqeq12d 
 |-  ( y = r -> ( ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) <-> ( ( x .+^ r ) .x. z ) = ( ( x .x. z ) .+ ( r .x. z ) ) ) )
57 oveq2 
 |-  ( z = w -> ( ( x .+^ r ) .x. z ) = ( ( x .+^ r ) .x. w ) )
58 oveq2 
 |-  ( z = w -> ( x .x. z ) = ( x .x. w ) )
59 oveq2 
 |-  ( z = w -> ( r .x. z ) = ( r .x. w ) )
60 58 59 oveq12d 
 |-  ( z = w -> ( ( x .x. z ) .+ ( r .x. z ) ) = ( ( x .x. w ) .+ ( r .x. w ) ) )
61 57 60 eqeq12d 
 |-  ( z = w -> ( ( ( x .+^ r ) .x. z ) = ( ( x .x. z ) .+ ( r .x. z ) ) <-> ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) )
62 56 61 rspc2v 
 |-  ( ( r e. B /\ w e. V ) -> ( A. y e. B A. z e. V ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) -> ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) )
63 50 51 62 syl2anc 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( A. y e. B A. z e. V ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) -> ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) )
64 49 63 mpd 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) )
65 25 44 64 3jca 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) )
66 14 3exp2 
 |-  ( ph -> ( x e. B -> ( y e. B -> ( z e. V -> ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) ) ) )
67 66 imp43 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. V ) ) -> ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
68 67 ralrimivva 
 |-  ( ( ph /\ x e. B ) -> A. y e. B A. z e. V ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
69 45 68 sylan2 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> A. y e. B A. z e. V ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
70 oveq2 
 |-  ( y = r -> ( x .X. y ) = ( x .X. r ) )
71 70 oveq1d 
 |-  ( y = r -> ( ( x .X. y ) .x. z ) = ( ( x .X. r ) .x. z ) )
72 54 oveq2d 
 |-  ( y = r -> ( x .x. ( y .x. z ) ) = ( x .x. ( r .x. z ) ) )
73 71 72 eqeq12d 
 |-  ( y = r -> ( ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) <-> ( ( x .X. r ) .x. z ) = ( x .x. ( r .x. z ) ) ) )
74 oveq2 
 |-  ( z = w -> ( ( x .X. r ) .x. z ) = ( ( x .X. r ) .x. w ) )
75 59 oveq2d 
 |-  ( z = w -> ( x .x. ( r .x. z ) ) = ( x .x. ( r .x. w ) ) )
76 74 75 eqeq12d 
 |-  ( z = w -> ( ( ( x .X. r ) .x. z ) = ( x .x. ( r .x. z ) ) <-> ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) ) )
77 73 76 rspc2v 
 |-  ( ( r e. B /\ w e. V ) -> ( A. y e. B A. z e. V ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) -> ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) ) )
78 50 51 77 syl2anc 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( A. y e. B A. z e. V ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) -> ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) ) )
79 69 78 mpd 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) )
80 15 ralrimiva 
 |-  ( ph -> A. x e. V ( .1. .x. x ) = x )
81 oveq2 
 |-  ( x = w -> ( .1. .x. x ) = ( .1. .x. w ) )
82 id 
 |-  ( x = w -> x = w )
83 81 82 eqeq12d 
 |-  ( x = w -> ( ( .1. .x. x ) = x <-> ( .1. .x. w ) = w ) )
84 83 rspcv 
 |-  ( w e. V -> ( A. x e. V ( .1. .x. x ) = x -> ( .1. .x. w ) = w ) )
85 84 ad2antll 
 |-  ( ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) -> ( A. x e. V ( .1. .x. x ) = x -> ( .1. .x. w ) = w ) )
86 80 85 mpan9 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( .1. .x. w ) = w )
87 65 79 86 jca32 
 |-  ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) )
88 87 anassrs 
 |-  ( ( ( ph /\ ( x e. B /\ r e. B ) ) /\ ( u e. V /\ w e. V ) ) -> ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) )
89 88 ralrimivva 
 |-  ( ( ph /\ ( x e. B /\ r e. B ) ) -> A. u e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) )
90 89 ralrimivva 
 |-  ( ph -> A. x e. B A. r e. B A. u e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) )
91 3 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` W ) ) )
92 5 91 eqtrd 
 |-  ( ph -> B = ( Base ` ( Scalar ` W ) ) )
93 4 oveqd 
 |-  ( ph -> ( r .x. w ) = ( r ( .s ` W ) w ) )
94 93 1 eleq12d 
 |-  ( ph -> ( ( r .x. w ) e. V <-> ( r ( .s ` W ) w ) e. ( Base ` W ) ) )
95 eqidd 
 |-  ( ph -> r = r )
96 2 oveqd 
 |-  ( ph -> ( w .+ u ) = ( w ( +g ` W ) u ) )
97 4 95 96 oveq123d 
 |-  ( ph -> ( r .x. ( w .+ u ) ) = ( r ( .s ` W ) ( w ( +g ` W ) u ) ) )
98 4 oveqd 
 |-  ( ph -> ( r .x. u ) = ( r ( .s ` W ) u ) )
99 2 93 98 oveq123d 
 |-  ( ph -> ( ( r .x. w ) .+ ( r .x. u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) )
100 97 99 eqeq12d 
 |-  ( ph -> ( ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) <-> ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) ) )
101 3 fveq2d 
 |-  ( ph -> ( +g ` F ) = ( +g ` ( Scalar ` W ) ) )
102 6 101 eqtrd 
 |-  ( ph -> .+^ = ( +g ` ( Scalar ` W ) ) )
103 102 oveqd 
 |-  ( ph -> ( x .+^ r ) = ( x ( +g ` ( Scalar ` W ) ) r ) )
104 eqidd 
 |-  ( ph -> w = w )
105 4 103 104 oveq123d 
 |-  ( ph -> ( ( x .+^ r ) .x. w ) = ( ( x ( +g ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) )
106 4 oveqd 
 |-  ( ph -> ( x .x. w ) = ( x ( .s ` W ) w ) )
107 2 106 93 oveq123d 
 |-  ( ph -> ( ( x .x. w ) .+ ( r .x. w ) ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) )
108 105 107 eqeq12d 
 |-  ( ph -> ( ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) <-> ( ( x ( +g ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) )
109 94 100 108 3anbi123d 
 |-  ( ph -> ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) <-> ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) ) )
110 3 fveq2d 
 |-  ( ph -> ( .r ` F ) = ( .r ` ( Scalar ` W ) ) )
111 7 110 eqtrd 
 |-  ( ph -> .X. = ( .r ` ( Scalar ` W ) ) )
112 111 oveqd 
 |-  ( ph -> ( x .X. r ) = ( x ( .r ` ( Scalar ` W ) ) r ) )
113 4 112 104 oveq123d 
 |-  ( ph -> ( ( x .X. r ) .x. w ) = ( ( x ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) )
114 eqidd 
 |-  ( ph -> x = x )
115 4 114 93 oveq123d 
 |-  ( ph -> ( x .x. ( r .x. w ) ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) )
116 113 115 eqeq12d 
 |-  ( ph -> ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) <-> ( ( x ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) ) )
117 3 fveq2d 
 |-  ( ph -> ( 1r ` F ) = ( 1r ` ( Scalar ` W ) ) )
118 8 117 eqtrd 
 |-  ( ph -> .1. = ( 1r ` ( Scalar ` W ) ) )
119 4 118 104 oveq123d 
 |-  ( ph -> ( .1. .x. w ) = ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) )
120 119 eqeq1d 
 |-  ( ph -> ( ( .1. .x. w ) = w <-> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) )
121 116 120 anbi12d 
 |-  ( ph -> ( ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) <-> ( ( ( x ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) )
122 109 121 anbi12d 
 |-  ( ph -> ( ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) <-> ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
123 1 122 raleqbidv 
 |-  ( ph -> ( A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) <-> A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
124 1 123 raleqbidv 
 |-  ( ph -> ( A. u e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) <-> A. u e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
125 92 124 raleqbidv 
 |-  ( ph -> ( A. r e. B A. u e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) <-> A. r e. ( Base ` ( Scalar ` W ) ) A. u e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
126 92 125 raleqbidv 
 |-  ( ph -> ( A. x e. B A. r e. B A. u e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) <-> A. x e. ( Base ` ( Scalar ` W ) ) A. r e. ( Base ` ( Scalar ` W ) ) A. u e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
127 90 126 mpbid 
 |-  ( ph -> A. x e. ( Base ` ( Scalar ` W ) ) A. r e. ( Base ` ( Scalar ` W ) ) A. u e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) )
128 eqid 
 |-  ( Base ` W ) = ( Base ` W )
129 eqid 
 |-  ( +g ` W ) = ( +g ` W )
130 eqid 
 |-  ( .s ` W ) = ( .s ` W )
131 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
132 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
133 eqid 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
134 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
135 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
136 128 129 130 131 132 133 134 135 islmod 
 |-  ( W e. LMod <-> ( W e. Grp /\ ( Scalar ` W ) e. Ring /\ A. x e. ( Base ` ( Scalar ` W ) ) A. r e. ( Base ` ( Scalar ` W ) ) A. u e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
137 10 16 127 136 syl3anbrc 
 |-  ( ph -> W e. LMod )