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	$⊢ X = {Base}_{W}$
	cvsi.a	$⊢ \underset{˙}{+} = +_{W}$
	cvsi.s	$⊢ S = {Base}_{Scalar (W)}$
	cvsi.m	$⊢ \underset{˙}{∙} = \cdot_{𝑠𝑓} (W)$
	cvsi.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
Assertion	cvsi	$⊢ W \in ℂVec \to (W \in Abel \land (S \subseteq ℂ \land \underset{˙}{∙} : S \times X ⟶ X) \land \forall x \in X (1 \underset{˙}{\cdot} x = x \land \forall y \in S (\forall z \in X y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in S ((y + z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x) \land y z \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x)))))$

Proof

Step	Hyp	Ref	Expression
1		cvsi.x	$⊢ X = {Base}_{W}$
2		cvsi.a	$⊢ \underset{˙}{+} = +_{W}$
3		cvsi.s	$⊢ S = {Base}_{Scalar (W)}$
4		cvsi.m	$⊢ \underset{˙}{∙} = \cdot_{𝑠𝑓} (W)$
5		cvsi.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		df-cvs	$⊢ ℂVec = CMod \cap LVec$
7	6	elin2	$⊢ W \in ℂVec \leftrightarrow (W \in CMod \land W \in LVec)$
8		lveclmod	$⊢ W \in LVec \to W \in LMod$
9		lmodabl	$⊢ W \in LMod \to W \in Abel$
10	8 9	syl	$⊢ W \in LVec \to W \in Abel$
11	10	adantl	$⊢ (W \in CMod \land W \in LVec) \to W \in Abel$
12		eqid	$⊢ Scalar (W) = Scalar (W)$
13	12 3	clmsscn	$⊢ W \in CMod \to S \subseteq ℂ$
14		clmlmod	$⊢ W \in CMod \to W \in LMod$
15	1 12 3 4	lmodscaf	$⊢ W \in LMod \to \underset{˙}{∙} : S \times X ⟶ X$
16	14 15	syl	$⊢ W \in CMod \to \underset{˙}{∙} : S \times X ⟶ X$
17	13 16	jca	$⊢ W \in CMod \to (S \subseteq ℂ \land \underset{˙}{∙} : S \times X ⟶ X)$
18	17	adantr	$⊢ (W \in CMod \land W \in LVec) \to (S \subseteq ℂ \land \underset{˙}{∙} : S \times X ⟶ X)$
19	1 5	clmvs1	$⊢ (W \in CMod \land x \in X) \to 1 \underset{˙}{\cdot} x = x$
20	14	adantr	$⊢ (W \in CMod \land x \in X) \to W \in LMod$
21	20	ad2antrr	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in X) \to W \in LMod$
22		simplr	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in X) \to y \in S$
23		simpllr	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in X) \to x \in X$
24		simpr	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in X) \to z \in X$
25	1 2 12 5 3	lmodvsdi	$⊢ (W \in LMod \land (y \in S \land x \in X \land z \in X)) \to y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
26	21 22 23 24 25	syl13anc	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in X) \to y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
27	26	ralrimiva	$⊢ ((W \in CMod \land x \in X) \land y \in S) \to \forall z \in X y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
28	12	clmadd	$⊢ W \in CMod \to + = +_{Scalar (W)}$
29	28	ad2antrr	$⊢ ((W \in CMod \land x \in X) \land y \in S) \to + = +_{Scalar (W)}$
30	29	oveqdr	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to y + z = y +_{Scalar (W)} z$
31	30	oveq1d	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to (y + z) \underset{˙}{\cdot} x = (y +_{Scalar (W)} z) \underset{˙}{\cdot} x$
32	20	ad2antrr	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to W \in LMod$
33		simplr	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to y \in S$
34		simpr	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to z \in S$
35		simpllr	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to x \in X$
36		eqid	$⊢ +_{Scalar (W)} = +_{Scalar (W)}$
37	1 2 12 5 3 36	lmodvsdir	$⊢ (W \in LMod \land (y \in S \land z \in S \land x \in X)) \to (y +_{Scalar (W)} z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x)$
38	32 33 34 35 37	syl13anc	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to (y +_{Scalar (W)} z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x)$
39	31 38	eqtrd	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to (y + z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x)$
40	12	clmmul	$⊢ W \in CMod \to \times = \cdot_{Scalar (W)}$
41	40	ad2antrr	$⊢ ((W \in CMod \land x \in X) \land y \in S) \to \times = \cdot_{Scalar (W)}$
42	41	oveqdr	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to y z = y \cdot_{Scalar (W)} z$
43	42	oveq1d	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to y z \underset{˙}{\cdot} x = (y \cdot_{Scalar (W)} z) \underset{˙}{\cdot} x$
44		eqid	$⊢ \cdot_{Scalar (W)} = \cdot_{Scalar (W)}$
45	1 12 5 3 44	lmodvsass	$⊢ (W \in LMod \land (y \in S \land z \in S \land x \in X)) \to (y \cdot_{Scalar (W)} z) \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x)$
46	32 33 34 35 45	syl13anc	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to (y \cdot_{Scalar (W)} z) \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x)$
47	43 46	eqtrd	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to y z \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x)$
48	39 47	jca	$⊢ (((W \in CMod \land x \in X) \land y \in S) \land z \in S) \to ((y + z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x) \land y z \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x))$
49	48	ralrimiva	$⊢ ((W \in CMod \land x \in X) \land y \in S) \to \forall z \in S ((y + z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x) \land y z \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x))$
50	27 49	jca	$⊢ ((W \in CMod \land x \in X) \land y \in S) \to (\forall z \in X y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in S ((y + z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x) \land y z \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x)))$
51	50	ralrimiva	$⊢ (W \in CMod \land x \in X) \to \forall y \in S (\forall z \in X y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in S ((y + z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x) \land y z \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x)))$
52	19 51	jca	$⊢ (W \in CMod \land x \in X) \to (1 \underset{˙}{\cdot} x = x \land \forall y \in S (\forall z \in X y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in S ((y + z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x) \land y z \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x))))$
53	52	ralrimiva	$⊢ W \in CMod \to \forall x \in X (1 \underset{˙}{\cdot} x = x \land \forall y \in S (\forall z \in X y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in S ((y + z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x) \land y z \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x))))$
54	53	adantr	$⊢ (W \in CMod \land W \in LVec) \to \forall x \in X (1 \underset{˙}{\cdot} x = x \land \forall y \in S (\forall z \in X y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in S ((y + z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x) \land y z \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x))))$
55	11 18 54	3jca	$⊢ (W \in CMod \land W \in LVec) \to (W \in Abel \land (S \subseteq ℂ \land \underset{˙}{∙} : S \times X ⟶ X) \land \forall x \in X (1 \underset{˙}{\cdot} x = x \land \forall y \in S (\forall z \in X y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in S ((y + z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x) \land y z \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x)))))$
56	7 55	sylbi	$⊢ W \in ℂVec \to (W \in Abel \land (S \subseteq ℂ \land \underset{˙}{∙} : S \times X ⟶ X) \land \forall x \in X (1 \underset{˙}{\cdot} x = x \land \forall y \in S (\forall z \in X y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in S ((y + z) \underset{˙}{\cdot} x = (y \underset{˙}{\cdot} x) \underset{˙}{+} (z \underset{˙}{\cdot} x) \land y z \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (z \underset{˙}{\cdot} x)))))$

Metamath Proof Explorer

Theorem cvsi

Proof