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

Metamath Proof Explorer

Theorem iscvsi

Proof