Metamath Proof Explorer

Theorem isclmi0

Description: Properties that determine a subcomplex module. (Contributed by NM, 5-Nov-2006) (Revised by AV, 4-Oct-2021)

Ref Expression
Hypotheses isclmp.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
isclmp.a ⊢ + = ( +g ‘ 𝑊 )
isclmp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
isclmp.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
isclmp.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
isclmi0.1 ⊢ 𝑆 = ( ℂfld ↾s 𝐾 )
isclmi0.2 ⊢ 𝑊 ∈ Grp
isclmi0.3 ⊢ 𝐾 ∈ ( SubRing ‘ ℂfld )
isclmi0.4 ⊢ ( 𝑥 ∈ 𝑉 → ( 1 · 𝑥 ) = 𝑥 )
isclmi0.5 ⊢ ( ( 𝑦 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑦 · 𝑥 ) ∈ 𝑉 )
isclmi0.6 ⊢ ( ( 𝑦 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
isclmi0.7 ⊢ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) )
isclmi0.8 ⊢ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) )
Assertion isclmi0 𝑊 ∈ ℂMod

Proof

Step Hyp Ref Expression
1 isclmp.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
2 isclmp.a ⊢ + = ( +g ‘ 𝑊 )
3 isclmp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 isclmp.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
5 isclmp.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
6 isclmi0.1 ⊢ 𝑆 = ( ℂfld ↾s 𝐾 )
7 isclmi0.2 ⊢ 𝑊 ∈ Grp
8 isclmi0.3 ⊢ 𝐾 ∈ ( SubRing ‘ ℂfld )
9 isclmi0.4 ⊢ ( 𝑥 ∈ 𝑉 → ( 1 · 𝑥 ) = 𝑥 )
10 isclmi0.5 ⊢ ( ( 𝑦 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑦 · 𝑥 ) ∈ 𝑉 )
11 isclmi0.6 ⊢ ( ( 𝑦 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
12 isclmi0.7 ⊢ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) )
13 isclmi0.8 ⊢ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) )
14 7 6 8 3pm3.2i ⊢ ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) )
15 10 ancoms ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑦 · 𝑥 ) ∈ 𝑉 )
16 11 3com12 ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
17 16 3expa ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 ∈ 𝑉 ) → ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
18 17 ralrimiva ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ) → ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
19 12 13 jca ⊢ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) )
20 19 3comr ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) → ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) )
21 20 3expa ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 ∈ 𝐾 ) → ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) )
22 21 ralrimiva ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ) → ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) )
23 15 18 22 3jca ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ) → ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) )
24 23 ralrimiva ⊢ ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) )
25 9 24 jca ⊢ ( 𝑥 ∈ 𝑉 → ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) )
26 25 rgen ⊢ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) )
27 1 2 3 4 5 isclmp ⊢ ( 𝑊 ∈ ℂMod ↔ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
28 14 26 27 mpbir2an ⊢ 𝑊 ∈ ℂMod