Theorem cvsi

Description: The properties of a subcomplex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. (Contributed by NM, 3-Nov-2006) (Revised by AV, 21-Sep-2021)

	Ref	Expression
Hypotheses	cvsi.x	⊢ 𝑋 = ( Base ‘ 𝑊 )
	cvsi.a	⊢ + = ( +g ‘ 𝑊 )
	cvsi.s	⊢ 𝑆 = ( Base ‘ ( Scalar ‘ 𝑊 ) )
	cvsi.m	⊢ ∙ = ( ·sf ‘ 𝑊 )
	cvsi.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion	cvsi	⊢ ( 𝑊 ∈ ℂVec → ( 𝑊 ∈ Abel ∧ ( 𝑆 ⊆ ℂ ∧ ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cvsi.x	⊢ 𝑋 = ( Base ‘ 𝑊 )
2		cvsi.a	⊢ + = ( +g ‘ 𝑊 )
3		cvsi.s	⊢ 𝑆 = ( Base ‘ ( Scalar ‘ 𝑊 ) )
4		cvsi.m	⊢ ∙ = ( ·sf ‘ 𝑊 )
5		cvsi.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		df-cvs	⊢ ℂVec = ( ℂMod ∩ LVec )
7	6	elin2	⊢ ( 𝑊 ∈ ℂVec ↔ ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) )
8		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9		lmodabl	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
10	8 9	syl	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ Abel )
11	10	adantl	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) → 𝑊 ∈ Abel )
12		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
13	12 3	clmsscn	⊢ ( 𝑊 ∈ ℂMod → 𝑆 ⊆ ℂ )
14		clmlmod	⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
15	1 12 3 4	lmodscaf	⊢ ( 𝑊 ∈ LMod → ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 )
16	14 15	syl	⊢ ( 𝑊 ∈ ℂMod → ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 )
17	13 16	jca	⊢ ( 𝑊 ∈ ℂMod → ( 𝑆 ⊆ ℂ ∧ ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 ) )
18	17	adantr	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) → ( 𝑆 ⊆ ℂ ∧ ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 ) )
19	1 5	clmvs1	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) → ( 1 · 𝑥 ) = 𝑥 )
20	14	adantr	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) → 𝑊 ∈ LMod )
21	20	ad2antrr	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑊 ∈ LMod )
22		simplr	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑦 ∈ 𝑆 )
23		simpllr	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
24		simpr	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
25	1 2 12 5 3	lmodvsdi	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
26	21 22 23 24 25	syl13anc	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
27	26	ralrimiva	⊢ ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
28	12	clmadd	⊢ ( 𝑊 ∈ ℂMod → + = ( +g ‘ ( Scalar ‘ 𝑊 ) ) )
29	28	ad2antrr	⊢ ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → + = ( +g ‘ ( Scalar ‘ 𝑊 ) ) )
30	29	oveqdr	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑦 + 𝑧 ) = ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) )
31	30	oveq1d	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) · 𝑥 ) )
32	20	ad2antrr	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑊 ∈ LMod )
33		simplr	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
34		simpr	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
35		simpllr	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑥 ∈ 𝑋 )
36		eqid	⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
37	1 2 12 5 3 36	lmodvsdir	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) )
38	32 33 34 35 37	syl13anc	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) )
39	31 38	eqtrd	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) )
40	12	clmmul	⊢ ( 𝑊 ∈ ℂMod → · = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
41	40	ad2antrr	⊢ ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → · = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
42	41	oveqdr	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑦 · 𝑧 ) = ( 𝑦 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) )
43	42	oveq1d	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( ( 𝑦 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) · 𝑥 ) )
44		eqid	⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
45	1 12 5 3 44	lmodvsass	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝑦 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) )
46	32 33 34 35 45	syl13anc	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) )
47	43 46	eqtrd	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) )
48	39 47	jca	⊢ ( ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) )
49	48	ralrimiva	⊢ ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) )
50	27 49	jca	⊢ ( ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) )
51	50	ralrimiva	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) )
52	19 51	jca	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋 ) → ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) ) )
53	52	ralrimiva	⊢ ( 𝑊 ∈ ℂMod → ∀ 𝑥 ∈ 𝑋 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) ) )
54	53	adantr	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) → ∀ 𝑥 ∈ 𝑋 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) ) )
55	11 18 54	3jca	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) → ( 𝑊 ∈ Abel ∧ ( 𝑆 ⊆ ℂ ∧ ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) ) ) )
56	7 55	sylbi	⊢ ( 𝑊 ∈ ℂVec → ( 𝑊 ∈ Abel ∧ ( 𝑆 ⊆ ℂ ∧ ∙ : ( 𝑆 × 𝑋 ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) ) ) ) ) )