Metamath Proof Explorer

Theorem lmodlema

Description: Lemma for properties of a left module. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses islmod.v 
|- V = ( Base ` W )
islmod.a 
|- .+ = ( +g ` W )
islmod.s 
|- .x. = ( .s ` W )
islmod.f 
|- F = ( Scalar ` W )
islmod.k 
|- K = ( Base ` F )
islmod.p 
|- .+^ = ( +g ` F )
islmod.t 
|- .X. = ( .r ` F )
islmod.u 
|- .1. = ( 1r ` F )
Assertion lmodlema 
|- ( ( W e. LMod /\ ( Q e. K /\ R e. K ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) /\ ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y ) ) )

Proof

Step Hyp Ref Expression
1 islmod.v 
 |-  V = ( Base ` W )
2 islmod.a 
 |-  .+ = ( +g ` W )
3 islmod.s 
 |-  .x. = ( .s ` W )
4 islmod.f 
 |-  F = ( Scalar ` W )
5 islmod.k 
 |-  K = ( Base ` F )
6 islmod.p 
 |-  .+^ = ( +g ` F )
7 islmod.t 
 |-  .X. = ( .r ` F )
8 islmod.u 
 |-  .1. = ( 1r ` F )
9 1 2 3 4 5 6 7 8 islmod 
 |-  ( W e. LMod <-> ( W e. Grp /\ F e. Ring /\ 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 ) ) ) )
10 9 simp3bi 
 |-  ( W e. LMod -> 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 ) ) )
11 oveq1 
 |-  ( q = Q -> ( q .+^ r ) = ( Q .+^ r ) )
12 11 oveq1d 
 |-  ( q = Q -> ( ( q .+^ r ) .x. w ) = ( ( Q .+^ r ) .x. w ) )
13 oveq1 
 |-  ( q = Q -> ( q .x. w ) = ( Q .x. w ) )
14 13 oveq1d 
 |-  ( q = Q -> ( ( q .x. w ) .+ ( r .x. w ) ) = ( ( Q .x. w ) .+ ( r .x. w ) ) )
15 12 14 eqeq12d 
 |-  ( q = Q -> ( ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) <-> ( ( Q .+^ r ) .x. w ) = ( ( Q .x. w ) .+ ( r .x. w ) ) ) )
16 15 3anbi3d 
 |-  ( q = Q -> ( ( ( 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 ) ) ) <-> ( ( 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 ) ) ) ) )
17 oveq1 
 |-  ( q = Q -> ( q .X. r ) = ( Q .X. r ) )
18 17 oveq1d 
 |-  ( q = Q -> ( ( q .X. r ) .x. w ) = ( ( Q .X. r ) .x. w ) )
19 oveq1 
 |-  ( q = Q -> ( q .x. ( r .x. w ) ) = ( Q .x. ( r .x. w ) ) )
20 18 19 eqeq12d 
 |-  ( q = Q -> ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) <-> ( ( Q .X. r ) .x. w ) = ( Q .x. ( r .x. w ) ) ) )
21 20 anbi1d 
 |-  ( q = Q -> ( ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) <-> ( ( ( Q .X. r ) .x. w ) = ( Q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) )
22 16 21 anbi12d 
 |-  ( q = Q -> ( ( ( ( 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 ) ) <-> ( ( ( 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 ) ) ) )
23 22 2ralbidv 
 |-  ( q = Q -> ( 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 ) ) <-> 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 ) ) ) )
24 oveq1 
 |-  ( r = R -> ( r .x. w ) = ( R .x. w ) )
25 24 eleq1d 
 |-  ( r = R -> ( ( r .x. w ) e. V <-> ( R .x. w ) e. V ) )
26 oveq1 
 |-  ( r = R -> ( r .x. ( w .+ x ) ) = ( R .x. ( w .+ x ) ) )
27 oveq1 
 |-  ( r = R -> ( r .x. x ) = ( R .x. x ) )
28 24 27 oveq12d 
 |-  ( r = R -> ( ( r .x. w ) .+ ( r .x. x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) )
29 26 28 eqeq12d 
 |-  ( r = R -> ( ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) <-> ( R .x. ( w .+ x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) ) )
30 oveq2 
 |-  ( r = R -> ( Q .+^ r ) = ( Q .+^ R ) )
31 30 oveq1d 
 |-  ( r = R -> ( ( Q .+^ r ) .x. w ) = ( ( Q .+^ R ) .x. w ) )
32 24 oveq2d 
 |-  ( r = R -> ( ( Q .x. w ) .+ ( r .x. w ) ) = ( ( Q .x. w ) .+ ( R .x. w ) ) )
33 31 32 eqeq12d 
 |-  ( r = R -> ( ( ( Q .+^ r ) .x. w ) = ( ( Q .x. w ) .+ ( r .x. w ) ) <-> ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) )
34 25 29 33 3anbi123d 
 |-  ( r = R -> ( ( ( 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 ) ) ) <-> ( ( 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 ) ) ) ) )
35 oveq2 
 |-  ( r = R -> ( Q .X. r ) = ( Q .X. R ) )
36 35 oveq1d 
 |-  ( r = R -> ( ( Q .X. r ) .x. w ) = ( ( Q .X. R ) .x. w ) )
37 24 oveq2d 
 |-  ( r = R -> ( Q .x. ( r .x. w ) ) = ( Q .x. ( R .x. w ) ) )
38 36 37 eqeq12d 
 |-  ( r = R -> ( ( ( Q .X. r ) .x. w ) = ( Q .x. ( r .x. w ) ) <-> ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) ) )
39 38 anbi1d 
 |-  ( r = R -> ( ( ( ( Q .X. r ) .x. w ) = ( Q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) <-> ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) /\ ( .1. .x. w ) = w ) ) )
40 34 39 anbi12d 
 |-  ( r = R -> ( ( ( ( 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 ) ) <-> ( ( ( 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 ) ) ) )
41 40 2ralbidv 
 |-  ( r = R -> ( 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 ) ) <-> 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 ) ) ) )
42 23 41 rspc2v 
 |-  ( ( Q e. K /\ R e. K ) -> ( 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 ) ) -> 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 ) ) ) )
43 10 42 mpan9 
 |-  ( ( W e. LMod /\ ( Q e. K /\ 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 ) ) )
44 oveq2 
 |-  ( x = X -> ( w .+ x ) = ( w .+ X ) )
45 44 oveq2d 
 |-  ( x = X -> ( R .x. ( w .+ x ) ) = ( R .x. ( w .+ X ) ) )
46 oveq2 
 |-  ( x = X -> ( R .x. x ) = ( R .x. X ) )
47 46 oveq2d 
 |-  ( x = X -> ( ( R .x. w ) .+ ( R .x. x ) ) = ( ( R .x. w ) .+ ( R .x. X ) ) )
48 45 47 eqeq12d 
 |-  ( x = X -> ( ( R .x. ( w .+ x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) <-> ( R .x. ( w .+ X ) ) = ( ( R .x. w ) .+ ( R .x. X ) ) ) )
49 48 3anbi2d 
 |-  ( x = X -> ( ( ( 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 ) ) ) <-> ( ( 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 ) ) ) ) )
50 49 anbi1d 
 |-  ( x = X -> ( ( ( ( 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 ) ) <-> ( ( ( 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 ) ) ) )
51 oveq2 
 |-  ( w = Y -> ( R .x. w ) = ( R .x. Y ) )
52 51 eleq1d 
 |-  ( w = Y -> ( ( R .x. w ) e. V <-> ( R .x. Y ) e. V ) )
53 oveq1 
 |-  ( w = Y -> ( w .+ X ) = ( Y .+ X ) )
54 53 oveq2d 
 |-  ( w = Y -> ( R .x. ( w .+ X ) ) = ( R .x. ( Y .+ X ) ) )
55 51 oveq1d 
 |-  ( w = Y -> ( ( R .x. w ) .+ ( R .x. X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) )
56 54 55 eqeq12d 
 |-  ( w = Y -> ( ( R .x. ( w .+ X ) ) = ( ( R .x. w ) .+ ( R .x. X ) ) <-> ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) ) )
57 oveq2 
 |-  ( w = Y -> ( ( Q .+^ R ) .x. w ) = ( ( Q .+^ R ) .x. Y ) )
58 oveq2 
 |-  ( w = Y -> ( Q .x. w ) = ( Q .x. Y ) )
59 58 51 oveq12d 
 |-  ( w = Y -> ( ( Q .x. w ) .+ ( R .x. w ) ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) )
60 57 59 eqeq12d 
 |-  ( w = Y -> ( ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) <-> ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) )
61 52 56 60 3anbi123d 
 |-  ( w = Y -> ( ( ( 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 ) ) ) <-> ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) ) )
62 oveq2 
 |-  ( w = Y -> ( ( Q .X. R ) .x. w ) = ( ( Q .X. R ) .x. Y ) )
63 51 oveq2d 
 |-  ( w = Y -> ( Q .x. ( R .x. w ) ) = ( Q .x. ( R .x. Y ) ) )
64 62 63 eqeq12d 
 |-  ( w = Y -> ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) <-> ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) ) )
65 oveq2 
 |-  ( w = Y -> ( .1. .x. w ) = ( .1. .x. Y ) )
66 id 
 |-  ( w = Y -> w = Y )
67 65 66 eqeq12d 
 |-  ( w = Y -> ( ( .1. .x. w ) = w <-> ( .1. .x. Y ) = Y ) )
68 64 67 anbi12d 
 |-  ( w = Y -> ( ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) /\ ( .1. .x. w ) = w ) <-> ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y ) ) )
69 61 68 anbi12d 
 |-  ( w = Y -> ( ( ( ( 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 ) ) <-> ( ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) /\ ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y ) ) ) )
70 50 69 rspc2v 
 |-  ( ( X e. V /\ Y e. V ) -> ( 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 ) ) -> ( ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) /\ ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y ) ) ) )
71 43 70 syl5com 
 |-  ( ( W e. LMod /\ ( Q e. K /\ R e. K ) ) -> ( ( X e. V /\ Y e. V ) -> ( ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) /\ ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y ) ) ) )
72 71 3impia 
 |-  ( ( W e. LMod /\ ( Q e. K /\ R e. K ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) /\ ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y ) ) )