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	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	iscvsp.a	$⊢ \underset{˙}{+} = +_{W}$
	iscvsp.v	$⊢ V = {Base}_{W}$
	iscvsp.s	$⊢ S = Scalar (W)$
	iscvsp.k	$⊢ K = {Base}_{S}$
	iscvsi.1	$⊢ W \in Grp$
	iscvsi.2	$⊢ S = ℂ_{fld} ↾_{𝑠} K$
	iscvsi.3	$⊢ S \in DivRing$
	iscvsi.4	$⊢ K \in SubRing (ℂ_{fld})$
	iscvsi.5	$⊢ x \in V \to 1 \underset{˙}{\cdot} x = x$
	iscvsi.6	$⊢ (y \in K \land x \in V) \to y \underset{˙}{\cdot} x \in V$
	iscvsi.7	$⊢ (y \in K \land x \in V \land z \in V) \to y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
	iscvsi.8	$⊢ (y \in K \land z \in K \land x \in V) \to (z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)$
	iscvsi.9	$⊢ (y \in K \land z \in K \land x \in V) \to z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)$
Assertion	iscvsi	$⊢ W \in ℂVec$

Proof

Step	Hyp	Ref	Expression
1		iscvsp.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
2		iscvsp.a	$⊢ \underset{˙}{+} = +_{W}$
3		iscvsp.v	$⊢ V = {Base}_{W}$
4		iscvsp.s	$⊢ S = Scalar (W)$
5		iscvsp.k	$⊢ K = {Base}_{S}$
6		iscvsi.1	$⊢ W \in Grp$
7		iscvsi.2	$⊢ S = ℂ_{fld} ↾_{𝑠} K$
8		iscvsi.3	$⊢ S \in DivRing$
9		iscvsi.4	$⊢ K \in SubRing (ℂ_{fld})$
10		iscvsi.5	$⊢ x \in V \to 1 \underset{˙}{\cdot} x = x$
11		iscvsi.6	$⊢ (y \in K \land x \in V) \to y \underset{˙}{\cdot} x \in V$
12		iscvsi.7	$⊢ (y \in K \land x \in V \land z \in V) \to y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
13		iscvsi.8	$⊢ (y \in K \land z \in K \land x \in V) \to (z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)$
14		iscvsi.9	$⊢ (y \in K \land z \in K \land x \in V) \to z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)$
15	8 7	pm3.2i	$⊢ (S \in DivRing \land S = ℂ_{fld} ↾_{𝑠} K)$
16	6 15 9	3pm3.2i	$⊢ (W \in Grp \land (S \in DivRing \land S = ℂ_{fld} ↾_{𝑠} K) \land K \in SubRing (ℂ_{fld}))$
17	11	ancoms	$⊢ (x \in V \land y \in K) \to y \underset{˙}{\cdot} x \in V$
18	12	3com12	$⊢ (x \in V \land y \in K \land z \in V) \to y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
19	18	3expa	$⊢ ((x \in V \land y \in K) \land z \in V) \to y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
20	19	ralrimiva	$⊢ (x \in V \land y \in K) \to \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
21	13 14	jca	$⊢ (y \in K \land z \in K \land x \in V) \to ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))$
22	21	3comr	$⊢ (x \in V \land y \in K \land z \in K) \to ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))$
23	22	3expa	$⊢ ((x \in V \land y \in K) \land z \in K) \to ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))$
24	23	ralrimiva	$⊢ (x \in V \land y \in K) \to \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))$
25	17 20 24	3jca	$⊢ (x \in V \land y \in K) \to (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
26	25	ralrimiva	$⊢ x \in V \to \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
27	10 26	jca	$⊢ x \in V \to (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
28	27	rgen	$⊢ \forall x \in V (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
29	1 2 3 4 5	iscvsp	$⊢ W \in ℂVec \leftrightarrow ((W \in Grp \land (S \in DivRing \land S = ℂ_{fld} ↾_{𝑠} K) \land K \in SubRing (ℂ_{fld})) \land \forall x \in V (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$
30	16 28 29	mpbir2an	$⊢ W \in ℂVec$

Metamath Proof Explorer

Theorem iscvsi

Proof