Metamath Proof Explorer

Theorem iscvsi

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

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

Proof

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