Metamath Proof Explorer


Theorem islmod

Description: The predicate "is a left module". (Contributed by NM, 4-Nov-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses islmod.v V = Base W
islmod.a + ˙ = + W
islmod.s · ˙ = W
islmod.f F = Scalar W
islmod.k K = Base F
islmod.p ˙ = + F
islmod.t × ˙ = F
islmod.u 1 ˙ = 1 F
Assertion islmod W LMod W Grp F Ring 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

Proof

Step Hyp Ref Expression
1 islmod.v V = Base W
2 islmod.a + ˙ = + W
3 islmod.s · ˙ = W
4 islmod.f F = Scalar W
5 islmod.k K = Base F
6 islmod.p ˙ = + F
7 islmod.t × ˙ = F
8 islmod.u 1 ˙ = 1 F
9 fveq2 g = W Base g = Base W
10 9 1 eqtr4di g = W Base g = V
11 fveq2 g = W + g = + W
12 11 2 eqtr4di g = W + g = + ˙
13 fveq2 g = W Scalar g = Scalar W
14 13 4 eqtr4di g = W Scalar g = F
15 fveq2 g = W g = W
16 15 3 eqtr4di g = W g = · ˙
17 16 sbceq1d g = W [˙ g / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w [˙· ˙ / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w
18 14 17 sbceqbid g = W [˙ Scalar g / f]˙ [˙ g / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w [˙F / f]˙ [˙· ˙ / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w
19 12 18 sbceqbid g = W [˙+ g / a]˙ [˙ Scalar g / f]˙ [˙ g / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w [˙+ ˙ / a]˙ [˙F / f]˙ [˙· ˙ / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w
20 10 19 sbceqbid g = W [˙Base g / v]˙ [˙+ g / a]˙ [˙ Scalar g / f]˙ [˙ g / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w [˙V / v]˙ [˙+ ˙ / a]˙ [˙F / f]˙ [˙· ˙ / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w
21 1 fvexi V V
22 2 fvexi + ˙ V
23 4 fvexi F V
24 simp3 v = V a = + ˙ f = F f = F
25 24 fveq2d v = V a = + ˙ f = F Base f = Base F
26 25 5 eqtr4di v = V a = + ˙ f = F Base f = K
27 24 fveq2d v = V a = + ˙ f = F + f = + F
28 27 6 eqtr4di v = V a = + ˙ f = F + f = ˙
29 24 fveq2d v = V a = + ˙ f = F f = F
30 29 7 eqtr4di v = V a = + ˙ f = F f = × ˙
31 30 sbceq1d v = V a = + ˙ f = F [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w [˙× ˙ / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w
32 7 fvexi × ˙ V
33 oveq t = × ˙ q t r = q × ˙ r
34 33 oveq1d t = × ˙ q t r s w = q × ˙ r s w
35 34 eqeq1d t = × ˙ q t r s w = q s r s w q × ˙ r s w = q s r s w
36 35 anbi1d t = × ˙ q t r s w = q s r s w 1 f s w = w q × ˙ r s w = q s r s w 1 f s w = w
37 36 anbi2d t = × ˙ r s w 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 1 f s w = w r s w 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 × ˙ r s w = q s r s w 1 f s w = w
38 37 2ralbidv t = × ˙ x v w v r s w 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 1 f s w = w x v w v r s w 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 × ˙ r s w = q s r s w 1 f s w = w
39 38 2ralbidv t = × ˙ q k r k x v w v r s w 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 1 f s w = w q k r k x v w v r s w 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 × ˙ r s w = q s r s w 1 f s w = w
40 39 anbi2d t = × ˙ f Ring q k r k x v w v r s w 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 1 f s w = w f Ring q k r k x v w v r s w 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 × ˙ r s w = q s r s w 1 f s w = w
41 32 40 sbcie [˙× ˙ / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w f Ring q k r k x v w v r s w 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 × ˙ r s w = q s r s w 1 f s w = w
42 24 eleq1d v = V a = + ˙ f = F f Ring F Ring
43 simp1 v = V a = + ˙ f = F v = V
44 43 eleq2d v = V a = + ˙ f = F r s w v r s w V
45 simp2 v = V a = + ˙ f = F a = + ˙
46 45 oveqd v = V a = + ˙ f = F w a x = w + ˙ x
47 46 oveq2d v = V a = + ˙ f = F r s w a x = r s w + ˙ x
48 45 oveqd v = V a = + ˙ f = F r s w a r s x = r s w + ˙ r s x
49 47 48 eqeq12d v = V a = + ˙ f = F r s w a x = r s w a r s x r s w + ˙ x = r s w + ˙ r s x
50 45 oveqd v = V a = + ˙ f = F q s w a r s w = q s w + ˙ r s w
51 50 eqeq2d v = V a = + ˙ f = F q p r s w = q s w a r s w q p r s w = q s w + ˙ r s w
52 44 49 51 3anbi123d v = V a = + ˙ f = F r s w 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 V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w
53 24 fveq2d v = V a = + ˙ f = F 1 f = 1 F
54 53 8 eqtr4di v = V a = + ˙ f = F 1 f = 1 ˙
55 54 oveq1d v = V a = + ˙ f = F 1 f s w = 1 ˙ s w
56 55 eqeq1d v = V a = + ˙ f = F 1 f s w = w 1 ˙ s w = w
57 56 anbi2d v = V a = + ˙ f = F q × ˙ r s w = q s r s w 1 f s w = w q × ˙ r s w = q s r s w 1 ˙ s w = w
58 52 57 anbi12d v = V a = + ˙ f = F r s w 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 × ˙ r s w = q s r s w 1 f s w = w r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w
59 43 58 raleqbidv v = V a = + ˙ f = F w v r s w 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 × ˙ r s w = q s r s w 1 f s w = w w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w
60 43 59 raleqbidv v = V a = + ˙ f = F x v w v r s w 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 × ˙ r s w = q s r s w 1 f s w = w x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w
61 60 2ralbidv v = V a = + ˙ f = F q k r k x v w v r s w 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 × ˙ r s w = q s r s w 1 f s w = w q k r k x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w
62 42 61 anbi12d v = V a = + ˙ f = F f Ring q k r k x v w v r s w 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 × ˙ r s w = q s r s w 1 f s w = w F Ring q k r k x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w
63 41 62 syl5bb v = V a = + ˙ f = F [˙× ˙ / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w F Ring q k r k x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w
64 31 63 bitrd v = V a = + ˙ f = F [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w F Ring q k r k x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w
65 28 64 sbceqbid v = V a = + ˙ f = F [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w [˙ ˙ / p]˙ F Ring q k r k x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w
66 26 65 sbceqbid v = V a = + ˙ f = F [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w [˙K / k]˙ [˙ ˙ / p]˙ F Ring q k r k x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w
67 66 sbcbidv v = V a = + ˙ f = F [˙· ˙ / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w [˙· ˙ / s]˙ [˙K / k]˙ [˙ ˙ / p]˙ F Ring q k r k x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w
68 21 22 23 67 sbc3ie [˙V / v]˙ [˙+ ˙ / a]˙ [˙F / f]˙ [˙· ˙ / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w [˙· ˙ / s]˙ [˙K / k]˙ [˙ ˙ / p]˙ F Ring q k r k x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w
69 3 fvexi · ˙ V
70 5 fvexi K V
71 6 fvexi ˙ V
72 simp2 s = · ˙ k = K p = ˙ k = K
73 simp1 s = · ˙ k = K p = ˙ s = · ˙
74 73 oveqd s = · ˙ k = K p = ˙ r s w = r · ˙ w
75 74 eleq1d s = · ˙ k = K p = ˙ r s w V r · ˙ w V
76 73 oveqd s = · ˙ k = K p = ˙ r s w + ˙ x = r · ˙ w + ˙ x
77 73 oveqd s = · ˙ k = K p = ˙ r s x = r · ˙ x
78 74 77 oveq12d s = · ˙ k = K p = ˙ r s w + ˙ r s x = r · ˙ w + ˙ r · ˙ x
79 76 78 eqeq12d s = · ˙ k = K p = ˙ r s w + ˙ x = r s w + ˙ r s x r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x
80 simp3 s = · ˙ k = K p = ˙ p = ˙
81 80 oveqd s = · ˙ k = K p = ˙ q p r = q ˙ r
82 81 oveq1d s = · ˙ k = K p = ˙ q p r s w = q ˙ r s w
83 73 oveqd s = · ˙ k = K p = ˙ q ˙ r s w = q ˙ r · ˙ w
84 82 83 eqtrd s = · ˙ k = K p = ˙ q p r s w = q ˙ r · ˙ w
85 73 oveqd s = · ˙ k = K p = ˙ q s w = q · ˙ w
86 85 74 oveq12d s = · ˙ k = K p = ˙ q s w + ˙ r s w = q · ˙ w + ˙ r · ˙ w
87 84 86 eqeq12d s = · ˙ k = K p = ˙ q p r s w = q s w + ˙ r s w q ˙ r · ˙ w = q · ˙ w + ˙ r · ˙ w
88 75 79 87 3anbi123d s = · ˙ k = K p = ˙ r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w r · ˙ w V r · ˙ w + ˙ x = r · ˙ w + ˙ r · ˙ x q ˙ r · ˙ w = q · ˙ w + ˙ r · ˙ w
89 73 oveqd s = · ˙ k = K p = ˙ q × ˙ r s w = q × ˙ r · ˙ w
90 74 oveq2d s = · ˙ k = K p = ˙ q s r s w = q s r · ˙ w
91 73 oveqd s = · ˙ k = K p = ˙ q s r · ˙ w = q · ˙ r · ˙ w
92 90 91 eqtrd s = · ˙ k = K p = ˙ q s r s w = q · ˙ r · ˙ w
93 89 92 eqeq12d s = · ˙ k = K p = ˙ q × ˙ r s w = q s r s w q × ˙ r · ˙ w = q · ˙ r · ˙ w
94 73 oveqd s = · ˙ k = K p = ˙ 1 ˙ s w = 1 ˙ · ˙ w
95 94 eqeq1d s = · ˙ k = K p = ˙ 1 ˙ s w = w 1 ˙ · ˙ w = w
96 93 95 anbi12d s = · ˙ k = K p = ˙ q × ˙ r s w = q s r s w 1 ˙ s w = w q × ˙ r · ˙ w = q · ˙ r · ˙ w 1 ˙ · ˙ w = w
97 88 96 anbi12d s = · ˙ k = K p = ˙ r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w 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
98 97 2ralbidv s = · ˙ k = K p = ˙ x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w 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
99 72 98 raleqbidv s = · ˙ k = K p = ˙ r k x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w 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
100 72 99 raleqbidv s = · ˙ k = K p = ˙ q k r k x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w 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
101 100 anbi2d s = · ˙ k = K p = ˙ F Ring q k r k x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w F Ring 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
102 69 70 71 101 sbc3ie [˙· ˙ / s]˙ [˙K / k]˙ [˙ ˙ / p]˙ F Ring q k r k x V w V r s w V r s w + ˙ x = r s w + ˙ r s x q p r s w = q s w + ˙ r s w q × ˙ r s w = q s r s w 1 ˙ s w = w F Ring 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
103 68 102 bitri [˙V / v]˙ [˙+ ˙ / a]˙ [˙F / f]˙ [˙· ˙ / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w F Ring 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
104 20 103 bitrdi g = W [˙Base g / v]˙ [˙+ g / a]˙ [˙ Scalar g / f]˙ [˙ g / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w F Ring 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
105 df-lmod LMod = g Grp | [˙Base g / v]˙ [˙+ g / a]˙ [˙ Scalar g / f]˙ [˙ g / s]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f Ring q k r k x v w v r s w 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 1 f s w = w
106 104 105 elrab2 W LMod W Grp F Ring 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
107 3anass W Grp F Ring 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 W Grp F Ring 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
108 106 107 bitr4i W LMod W Grp F Ring 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