Metamath Proof Explorer


Theorem slmdlema

Description: Lemma for properties of a semimodule. (Contributed by NM, 8-Dec-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 + ˙ = + W
isslmd.s · ˙ = W
isslmd.0 0 ˙ = 0 W
isslmd.f F = Scalar W
isslmd.k K = Base F
isslmd.p ˙ = + F
isslmd.t × ˙ = F
isslmd.u 1 ˙ = 1 F
isslmd.o O = 0 F
Assertion slmdlema W SLMod Q K R K X V Y V R · ˙ Y V R · ˙ Y + ˙ X = R · ˙ Y + ˙ R · ˙ X Q ˙ R · ˙ Y = Q · ˙ Y + ˙ R · ˙ Y Q × ˙ R · ˙ Y = Q · ˙ R · ˙ Y 1 ˙ · ˙ Y = Y O · ˙ Y = 0 ˙

Proof

Step Hyp Ref Expression
1 isslmd.v V = Base W
2 isslmd.a + ˙ = + W
3 isslmd.s · ˙ = W
4 isslmd.0 0 ˙ = 0 W
5 isslmd.f F = Scalar W
6 isslmd.k K = Base F
7 isslmd.p ˙ = + F
8 isslmd.t × ˙ = F
9 isslmd.u 1 ˙ = 1 F
10 isslmd.o O = 0 F
11 1 2 3 4 5 6 7 8 9 10 isslmd W SLMod W CMnd F SRing q K r K x V w V r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x q ˙ r · ˙ w = q · ˙ w + ˙ r · ˙ w q × ˙ r · ˙ w = q · ˙ r · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙
12 11 simp3bi W SLMod q K r K x V w V r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x q ˙ r · ˙ w = q · ˙ w + ˙ r · ˙ w q × ˙ r · ˙ w = q · ˙ r · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙
13 oveq1 q = Q q ˙ r = Q ˙ r
14 13 oveq1d q = Q q ˙ r · ˙ w = Q ˙ r · ˙ w
15 oveq1 q = Q q · ˙ w = Q · ˙ w
16 15 oveq1d q = Q q · ˙ w + ˙ r · ˙ w = Q · ˙ w + ˙ r · ˙ w
17 14 16 eqeq12d q = Q q ˙ r · ˙ w = q · ˙ w + ˙ r · ˙ w Q ˙ r · ˙ w = Q · ˙ w + ˙ r · ˙ w
18 17 3anbi3d q = Q r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x q ˙ r · ˙ w = q · ˙ w + ˙ r · ˙ w r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x Q ˙ r · ˙ w = Q · ˙ w + ˙ r · ˙ w
19 oveq1 q = Q q × ˙ r = Q × ˙ r
20 19 oveq1d q = Q q × ˙ r · ˙ w = Q × ˙ r · ˙ w
21 oveq1 q = Q q · ˙ r · ˙ w = Q · ˙ r · ˙ w
22 20 21 eqeq12d q = Q q × ˙ r · ˙ w = q · ˙ r · ˙ w Q × ˙ r · ˙ w = Q · ˙ r · ˙ w
23 22 3anbi1d q = Q q × ˙ r · ˙ w = q · ˙ r · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙ Q × ˙ r · ˙ w = Q · ˙ r · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙
24 18 23 anbi12d q = Q r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x q ˙ r · ˙ w = q · ˙ w + ˙ r · ˙ w q × ˙ r · ˙ w = q · ˙ r · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙ r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x Q ˙ r · ˙ w = Q · ˙ w + ˙ r · ˙ w Q × ˙ r · ˙ w = Q · ˙ r · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙
25 24 2ralbidv q = Q x V w V r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x q ˙ r · ˙ w = q · ˙ w + ˙ r · ˙ w q × ˙ r · ˙ w = q · ˙ r · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙ x V w V r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x Q ˙ r · ˙ w = Q · ˙ w + ˙ r · ˙ w Q × ˙ r · ˙ w = Q · ˙ r · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙
26 oveq1 r = R r · ˙ w = R · ˙ w
27 26 eleq1d r = R r · ˙ w V R · ˙ w V
28 oveq1 r = R r · ˙ w + ˙ x = R · ˙ w + ˙ x
29 oveq1 r = R r · ˙ x = R · ˙ x
30 26 29 oveq12d r = R r · ˙ w + ˙ r · ˙ x = R · ˙ w + ˙ R · ˙ x
31 28 30 eqeq12d r = R r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x R · ˙ w + ˙ x = R · ˙ w + ˙ R · ˙ x
32 oveq2 r = R Q ˙ r = Q ˙ R
33 32 oveq1d r = R Q ˙ r · ˙ w = Q ˙ R · ˙ w
34 26 oveq2d r = R Q · ˙ w + ˙ r · ˙ w = Q · ˙ w + ˙ R · ˙ w
35 33 34 eqeq12d r = R Q ˙ r · ˙ w = Q · ˙ w + ˙ r · ˙ w Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w
36 27 31 35 3anbi123d r = R r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x Q ˙ r · ˙ w = Q · ˙ w + ˙ r · ˙ w R · ˙ w V R · ˙ w + ˙ x = R · ˙ w + ˙ R · ˙ x Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w
37 oveq2 r = R Q × ˙ r = Q × ˙ R
38 37 oveq1d r = R Q × ˙ r · ˙ w = Q × ˙ R · ˙ w
39 26 oveq2d r = R Q · ˙ r · ˙ w = Q · ˙ R · ˙ w
40 38 39 eqeq12d r = R Q × ˙ r · ˙ w = Q · ˙ r · ˙ w Q × ˙ R · ˙ w = Q · ˙ R · ˙ w
41 40 3anbi1d r = R Q × ˙ r · ˙ w = Q · ˙ r · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙ Q × ˙ R · ˙ w = Q · ˙ R · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙
42 36 41 anbi12d r = R r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x Q ˙ r · ˙ w = Q · ˙ w + ˙ r · ˙ w Q × ˙ r · ˙ w = Q · ˙ r · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙ R · ˙ w V R · ˙ w + ˙ x = R · ˙ w + ˙ R · ˙ x Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w Q × ˙ R · ˙ w = Q · ˙ R · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙
43 42 2ralbidv r = R x V w V r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x Q ˙ r · ˙ w = Q · ˙ w + ˙ r · ˙ w Q × ˙ r · ˙ w = Q · ˙ r · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙ x V w V R · ˙ w V R · ˙ w + ˙ x = R · ˙ w + ˙ R · ˙ x Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w Q × ˙ R · ˙ w = Q · ˙ R · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙
44 25 43 rspc2v Q K R K q K r K x V w V r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x q ˙ r · ˙ w = q · ˙ w + ˙ r · ˙ w q × ˙ r · ˙ w = q · ˙ r · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙ x V w V R · ˙ w V R · ˙ w + ˙ x = R · ˙ w + ˙ R · ˙ x Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w Q × ˙ R · ˙ w = Q · ˙ R · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙
45 12 44 mpan9 W SLMod Q K R K x V w V R · ˙ w V R · ˙ w + ˙ x = R · ˙ w + ˙ R · ˙ x Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w Q × ˙ R · ˙ w = Q · ˙ R · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙
46 oveq2 x = X w + ˙ x = w + ˙ X
47 46 oveq2d x = X R · ˙ w + ˙ x = R · ˙ w + ˙ X
48 oveq2 x = X R · ˙ x = R · ˙ X
49 48 oveq2d x = X R · ˙ w + ˙ R · ˙ x = R · ˙ w + ˙ R · ˙ X
50 47 49 eqeq12d x = X R · ˙ w + ˙ x = R · ˙ w + ˙ R · ˙ x R · ˙ w + ˙ X = R · ˙ w + ˙ R · ˙ X
51 50 3anbi2d x = X R · ˙ w V R · ˙ w + ˙ x = R · ˙ w + ˙ R · ˙ x Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w R · ˙ w V R · ˙ w + ˙ X = R · ˙ w + ˙ R · ˙ X Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w
52 51 anbi1d x = X R · ˙ w V R · ˙ w + ˙ x = R · ˙ w + ˙ R · ˙ x Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w Q × ˙ R · ˙ w = Q · ˙ R · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙ R · ˙ w V R · ˙ w + ˙ X = R · ˙ w + ˙ R · ˙ X Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w Q × ˙ R · ˙ w = Q · ˙ R · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙
53 oveq2 w = Y R · ˙ w = R · ˙ Y
54 53 eleq1d w = Y R · ˙ w V R · ˙ Y V
55 oveq1 w = Y w + ˙ X = Y + ˙ X
56 55 oveq2d w = Y R · ˙ w + ˙ X = R · ˙ Y + ˙ X
57 53 oveq1d w = Y R · ˙ w + ˙ R · ˙ X = R · ˙ Y + ˙ R · ˙ X
58 56 57 eqeq12d w = Y R · ˙ w + ˙ X = R · ˙ w + ˙ R · ˙ X R · ˙ Y + ˙ X = R · ˙ Y + ˙ R · ˙ X
59 oveq2 w = Y Q ˙ R · ˙ w = Q ˙ R · ˙ Y
60 oveq2 w = Y Q · ˙ w = Q · ˙ Y
61 60 53 oveq12d w = Y Q · ˙ w + ˙ R · ˙ w = Q · ˙ Y + ˙ R · ˙ Y
62 59 61 eqeq12d w = Y Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w Q ˙ R · ˙ Y = Q · ˙ Y + ˙ R · ˙ Y
63 54 58 62 3anbi123d w = Y R · ˙ w V R · ˙ w + ˙ X = R · ˙ w + ˙ R · ˙ X Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w R · ˙ Y V R · ˙ Y + ˙ X = R · ˙ Y + ˙ R · ˙ X Q ˙ R · ˙ Y = Q · ˙ Y + ˙ R · ˙ Y
64 oveq2 w = Y Q × ˙ R · ˙ w = Q × ˙ R · ˙ Y
65 53 oveq2d w = Y Q · ˙ R · ˙ w = Q · ˙ R · ˙ Y
66 64 65 eqeq12d w = Y Q × ˙ R · ˙ w = Q · ˙ R · ˙ w Q × ˙ R · ˙ Y = Q · ˙ R · ˙ Y
67 oveq2 w = Y 1 ˙ · ˙ w = 1 ˙ · ˙ Y
68 id w = Y w = Y
69 67 68 eqeq12d w = Y 1 ˙ · ˙ w = w 1 ˙ · ˙ Y = Y
70 oveq2 w = Y O · ˙ w = O · ˙ Y
71 70 eqeq1d w = Y O · ˙ w = 0 ˙ O · ˙ Y = 0 ˙
72 66 69 71 3anbi123d w = Y Q × ˙ R · ˙ w = Q · ˙ R · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙ Q × ˙ R · ˙ Y = Q · ˙ R · ˙ Y 1 ˙ · ˙ Y = Y O · ˙ Y = 0 ˙
73 63 72 anbi12d w = Y R · ˙ w V R · ˙ w + ˙ X = R · ˙ w + ˙ R · ˙ X Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w Q × ˙ R · ˙ w = Q · ˙ R · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙ R · ˙ Y V R · ˙ Y + ˙ X = R · ˙ Y + ˙ R · ˙ X Q ˙ R · ˙ Y = Q · ˙ Y + ˙ R · ˙ Y Q × ˙ R · ˙ Y = Q · ˙ R · ˙ Y 1 ˙ · ˙ Y = Y O · ˙ Y = 0 ˙
74 52 73 rspc2v X V Y V x V w V R · ˙ w V R · ˙ w + ˙ x = R · ˙ w + ˙ R · ˙ x Q ˙ R · ˙ w = Q · ˙ w + ˙ R · ˙ w Q × ˙ R · ˙ w = Q · ˙ R · ˙ w 1 ˙ · ˙ w = w O · ˙ w = 0 ˙ R · ˙ Y V R · ˙ Y + ˙ X = R · ˙ Y + ˙ R · ˙ X Q ˙ R · ˙ Y = Q · ˙ Y + ˙ R · ˙ Y Q × ˙ R · ˙ Y = Q · ˙ R · ˙ Y 1 ˙ · ˙ Y = Y O · ˙ Y = 0 ˙
75 45 74 syl5com W SLMod Q K R K X V Y V R · ˙ Y V R · ˙ Y + ˙ X = R · ˙ Y + ˙ R · ˙ X Q ˙ R · ˙ Y = Q · ˙ Y + ˙ R · ˙ Y Q × ˙ R · ˙ Y = Q · ˙ R · ˙ Y 1 ˙ · ˙ Y = Y O · ˙ Y = 0 ˙
76 75 3impia W SLMod Q K R K X V Y V R · ˙ Y V R · ˙ Y + ˙ X = R · ˙ Y + ˙ R · ˙ X Q ˙ R · ˙ Y = Q · ˙ Y + ˙ R · ˙ Y Q × ˙ R · ˙ Y = Q · ˙ R · ˙ Y 1 ˙ · ˙ Y = Y O · ˙ Y = 0 ˙