This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-clm

Description: Define the class of subcomplex modules, which are left modules over a subring of the field of complex numbers CCfld , which allows to use the complex addition, multiplication, etc. in theorems about subcomplex modules. Since the field of complex numbers is commutative and so are its subrings (see subrgcrng ), left modules over such subrings are the same as right modules, see rmodislmod . Therefore, we drop the word "left" from "subcomplex left module". (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Assertion df-clm ⊢ CMod = w ∈ LMod | [˙ Scalar ⁡ w / f]˙ [˙Base f / k]˙ f = ℂ fld ↾ 𝑠 k ∧ k ∈ SubRing ⁡ ℂ fld

Detailed syntax breakdown

Step Hyp Ref Expression
0 cclm class CMod
1 vw setvar w
2 clmod class LMod
3 csca class Scalar
4 1 cv setvar w
5 4 3 cfv class Scalar ⁡ w
6 vf setvar f
7 cbs class Base
8 6 cv setvar f
9 8 7 cfv class Base f
10 vk setvar k
11 ccnfld class ℂ fld
12 cress class ↾ 𝑠
13 10 cv setvar k
14 11 13 12 co class ℂ fld ↾ 𝑠 k
15 8 14 wceq wff f = ℂ fld ↾ 𝑠 k
16 csubrg class SubRing
17 11 16 cfv class SubRing ⁡ ℂ fld
18 13 17 wcel wff k ∈ SubRing ⁡ ℂ fld
19 15 18 wa wff f = ℂ fld ↾ 𝑠 k ∧ k ∈ SubRing ⁡ ℂ fld
20 19 10 9 wsbc wff [˙Base f / k]˙ f = ℂ fld ↾ 𝑠 k ∧ k ∈ SubRing ⁡ ℂ fld
21 20 6 5 wsbc wff [˙ Scalar ⁡ w / f]˙ [˙Base f / k]˙ f = ℂ fld ↾ 𝑠 k ∧ k ∈ SubRing ⁡ ℂ fld
22 21 1 2 crab class w ∈ LMod | [˙ Scalar ⁡ w / f]˙ [˙Base f / k]˙ f = ℂ fld ↾ 𝑠 k ∧ k ∈ SubRing ⁡ ℂ fld
23 0 22 wceq wff CMod = w ∈ LMod | [˙ Scalar ⁡ w / f]˙ [˙Base f / k]˙ f = ℂ fld ↾ 𝑠 k ∧ k ∈ SubRing ⁡ ℂ fld