Metamath Proof Explorer

Theorem iscvsp

Description: The predicate "is a subcomplex vector space". (Contributed by NM, 31-May-2008) (Revised by AV, 4-Oct-2021)

Ref Expression
Hypotheses iscvsp.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
iscvsp.a ⊢ + = ( +g ‘ 𝑊 )
iscvsp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
iscvsp.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
iscvsp.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
Assertion iscvsp ( 𝑊 ∈ ℂVec ↔ ( ( 𝑊 ∈ Grp ∧ ( 𝑆 ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )

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 iscvs ⊢ ( 𝑊 ∈ ℂVec ↔ ( 𝑊 ∈ ℂMod ∧ ( Scalar ‘ 𝑊 ) ∈ DivRing ) )
7 1 2 3 4 5 isclmp ⊢ ( 𝑊 ∈ ℂMod ↔ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
8 7 anbi2ci ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( Scalar ‘ 𝑊 ) ∈ DivRing ) ↔ ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) ) )
9 anass ⊢ ( ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) ↔ ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) ) )
10 3anan12 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ↔ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ ( 𝑊 ∈ Grp ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
11 10 anbi2i ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ↔ ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ ( 𝑊 ∈ Grp ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ) )
12 anass ⊢ ( ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) ∧ ( 𝑊 ∈ Grp ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ↔ ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ ( 𝑊 ∈ Grp ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ) )
13 4 eqcomi ⊢ ( Scalar ‘ 𝑊 ) = 𝑆
14 13 eleq1i ⊢ ( ( Scalar ‘ 𝑊 ) ∈ DivRing ↔ 𝑆 ∈ DivRing )
15 14 anbi1i ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) ↔ ( 𝑆 ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) )
16 15 anbi1i ⊢ ( ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) ∧ ( 𝑊 ∈ Grp ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ↔ ( ( 𝑆 ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) ∧ ( 𝑊 ∈ Grp ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
17 11 12 16 3bitr2i ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ↔ ( ( 𝑆 ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) ∧ ( 𝑊 ∈ Grp ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
18 3anan12 ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑆 ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ↔ ( ( 𝑆 ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) ∧ ( 𝑊 ∈ Grp ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
19 17 18 bitr4i ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ↔ ( 𝑊 ∈ Grp ∧ ( 𝑆 ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )
20 19 anbi1i ⊢ ( ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) ↔ ( ( 𝑊 ∈ Grp ∧ ( 𝑆 ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
21 8 9 20 3bitr2i ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( Scalar ‘ 𝑊 ) ∈ DivRing ) ↔ ( ( 𝑊 ∈ Grp ∧ ( 𝑆 ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
22 6 21 bitri ⊢ ( 𝑊 ∈ ℂVec ↔ ( ( 𝑊 ∈ Grp ∧ ( 𝑆 ∈ DivRing ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )