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 ℂMod = { 𝑤 ∈ LMod ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cclm ⊢ ℂMod
1 vw ⊢ 𝑤
2 clmod ⊢ LMod
3 csca ⊢ Scalar
4 1 cv ⊢ 𝑤
5 4 3 cfv ⊢ ( Scalar ‘ 𝑤 )
6 vf ⊢ 𝑓
7 cbs ⊢ Base
8 6 cv ⊢ 𝑓
9 8 7 cfv ⊢ ( Base ‘ 𝑓 )
10 vk ⊢ 𝑘
11 ccnfld ⊢ ℂfld
12 cress ⊢ ↾s
13 10 cv ⊢ 𝑘
14 11 13 12 co ⊢ ( ℂfld ↾s 𝑘 )
15 8 14 wceq ⊢ 𝑓 = ( ℂfld ↾s 𝑘 )
16 csubrg ⊢ SubRing
17 11 16 cfv ⊢ ( SubRing ‘ ℂfld )
18 13 17 wcel ⊢ 𝑘 ∈ ( SubRing ‘ ℂfld )
19 15 18 wa ⊢ ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) )
20 19 10 9 wsbc ⊢ [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) )
21 20 6 5 wsbc ⊢ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) )
22 21 1 2 crab ⊢ { 𝑤 ∈ LMod ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) ) }
23 0 22 wceq ⊢ ℂMod = { 𝑤 ∈ LMod ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) ) }