Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Affine, Euclidean, and Cartesian geometry
Real vector spaces
bj-isclm
Next ⟩
crrvec
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-isclm
Description:
The predicate "is a subcomplex module".
(Contributed by
BJ
, 6-Jan-2024)
Ref
Expression
Hypotheses
bj-isclm.scal
⊢
φ
→
F
=
Scalar
⁡
W
bj-isclm.base
⊢
φ
→
K
=
Base
F
Assertion
bj-isclm
⊢
φ
→
W
∈
CMod
↔
W
∈
LMod
∧
F
=
ℂ
fld
↾
𝑠
K
∧
K
∈
SubRing
⁡
ℂ
fld
Proof
Step
Hyp
Ref
Expression
1
bj-isclm.scal
⊢
φ
→
F
=
Scalar
⁡
W
2
bj-isclm.base
⊢
φ
→
K
=
Base
F
3
eqid
⊢
Scalar
⁡
W
=
Scalar
⁡
W
4
eqid
⊢
Base
Scalar
⁡
W
=
Base
Scalar
⁡
W
5
3
4
isclm
⊢
W
∈
CMod
↔
W
∈
LMod
∧
Scalar
⁡
W
=
ℂ
fld
↾
𝑠
Base
Scalar
⁡
W
∧
Base
Scalar
⁡
W
∈
SubRing
⁡
ℂ
fld
6
1
eqcomd
⊢
φ
→
Scalar
⁡
W
=
F
7
fveq2
⊢
F
=
Scalar
⁡
W
→
Base
F
=
Base
Scalar
⁡
W
8
eqtr
⊢
K
=
Base
F
∧
Base
F
=
Base
Scalar
⁡
W
→
K
=
Base
Scalar
⁡
W
9
8
eqcomd
⊢
K
=
Base
F
∧
Base
F
=
Base
Scalar
⁡
W
→
Base
Scalar
⁡
W
=
K
10
9
ex
⊢
K
=
Base
F
→
Base
F
=
Base
Scalar
⁡
W
→
Base
Scalar
⁡
W
=
K
11
2
7
10
syl2im
⊢
φ
→
F
=
Scalar
⁡
W
→
Base
Scalar
⁡
W
=
K
12
1
11
mpd
⊢
φ
→
Base
Scalar
⁡
W
=
K
13
12
oveq2d
⊢
φ
→
ℂ
fld
↾
𝑠
Base
Scalar
⁡
W
=
ℂ
fld
↾
𝑠
K
14
6
13
eqeq12d
⊢
φ
→
Scalar
⁡
W
=
ℂ
fld
↾
𝑠
Base
Scalar
⁡
W
↔
F
=
ℂ
fld
↾
𝑠
K
15
12
eleq1d
⊢
φ
→
Base
Scalar
⁡
W
∈
SubRing
⁡
ℂ
fld
↔
K
∈
SubRing
⁡
ℂ
fld
16
14
15
3anbi23d
⊢
φ
→
W
∈
LMod
∧
Scalar
⁡
W
=
ℂ
fld
↾
𝑠
Base
Scalar
⁡
W
∧
Base
Scalar
⁡
W
∈
SubRing
⁡
ℂ
fld
↔
W
∈
LMod
∧
F
=
ℂ
fld
↾
𝑠
K
∧
K
∈
SubRing
⁡
ℂ
fld
17
5
16
syl5bb
⊢
φ
→
W
∈
CMod
↔
W
∈
LMod
∧
F
=
ℂ
fld
↾
𝑠
K
∧
K
∈
SubRing
⁡
ℂ
fld