# 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}={\mathrm{Base}}_{{W}}$
islmod.a
islmod.s
islmod.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
islmod.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
islmod.p
islmod.t
islmod.u
Assertion islmod

### Proof

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