# 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 ${⊢}{\phi }\to {V}={\mathrm{Base}}_{{W}}$
islmodd.a
islmodd.f ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({W}\right)$
islmodd.s
islmodd.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{F}}$
islmodd.p
islmodd.t
islmodd.u
islmodd.r ${⊢}{\phi }\to {F}\in \mathrm{Ring}$
islmodd.l ${⊢}{\phi }\to {W}\in \mathrm{Grp}$
islmodd.w
islmodd.c
islmodd.d
islmodd.e
islmodd.g
Assertion islmodd ${⊢}{\phi }\to {W}\in \mathrm{LMod}$

### Proof

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