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	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	iscvsp.a	$⊢ \underset{˙}{+} = +_{W}$
	iscvsp.v	$⊢ V = {Base}_{W}$
	iscvsp.s	$⊢ S = Scalar (W)$
	iscvsp.k	$⊢ K = {Base}_{S}$
Assertion	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)))))$

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		iscvs	$⊢ W \in ℂVec \leftrightarrow (W \in CMod \land Scalar (W) \in DivRing)$
7	1 2 3 4 5	isclmp	$⊢ W \in CMod \leftrightarrow ((W \in Grp \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)))))$
8	7	anbi2ci	$⊢ (W \in CMod \land Scalar (W) \in DivRing) \leftrightarrow (Scalar (W) \in DivRing \land ((W \in Grp \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))))))$
9		anass	$⊢ ((Scalar (W) \in DivRing \land (W \in Grp \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))))) \leftrightarrow (Scalar (W) \in DivRing \land ((W \in Grp \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))))))$
10		3anan12	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \leftrightarrow (S = ℂ_{fld} ↾_{𝑠} K \land (W \in Grp \land K \in SubRing (ℂ_{fld})))$
11	10	anbi2i	$⊢ (Scalar (W) \in DivRing \land (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \leftrightarrow (Scalar (W) \in DivRing \land (S = ℂ_{fld} ↾_{𝑠} K \land (W \in Grp \land K \in SubRing (ℂ_{fld}))))$
12		anass	$⊢ ((Scalar (W) \in DivRing \land S = ℂ_{fld} ↾_{𝑠} K) \land (W \in Grp \land K \in SubRing (ℂ_{fld}))) \leftrightarrow (Scalar (W) \in DivRing \land (S = ℂ_{fld} ↾_{𝑠} K \land (W \in Grp \land K \in SubRing (ℂ_{fld}))))$
13	4	eqcomi	$⊢ Scalar (W) = S$
14	13	eleq1i	$⊢ Scalar (W) \in DivRing \leftrightarrow S \in DivRing$
15	14	anbi1i	$⊢ (Scalar (W) \in DivRing \land S = ℂ_{fld} ↾_{𝑠} K) \leftrightarrow (S \in DivRing \land S = ℂ_{fld} ↾_{𝑠} K)$
16	15	anbi1i	$⊢ ((Scalar (W) \in DivRing \land S = ℂ_{fld} ↾_{𝑠} K) \land (W \in Grp \land K \in SubRing (ℂ_{fld}))) \leftrightarrow ((S \in DivRing \land S = ℂ_{fld} ↾_{𝑠} K) \land (W \in Grp \land K \in SubRing (ℂ_{fld})))$
17	11 12 16	3bitr2i	$⊢ (Scalar (W) \in DivRing \land (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \leftrightarrow ((S \in DivRing \land S = ℂ_{fld} ↾_{𝑠} K) \land (W \in Grp \land K \in SubRing (ℂ_{fld})))$
18		3anan12	$⊢ (W \in Grp \land (S \in DivRing \land S = ℂ_{fld} ↾_{𝑠} K) \land K \in SubRing (ℂ_{fld})) \leftrightarrow ((S \in DivRing \land S = ℂ_{fld} ↾_{𝑠} K) \land (W \in Grp \land K \in SubRing (ℂ_{fld})))$
19	17 18	bitr4i	$⊢ (Scalar (W) \in DivRing \land (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \leftrightarrow (W \in Grp \land (S \in DivRing \land S = ℂ_{fld} ↾_{𝑠} K) \land K \in SubRing (ℂ_{fld}))$
20	19	anbi1i	$⊢ ((Scalar (W) \in DivRing \land (W \in Grp \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))))) \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)))))$
21	8 9 20	3bitr2i	$⊢ (W \in CMod \land Scalar (W) \in DivRing) \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)))))$
22	6 21	bitri	$⊢ 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)))))$

Metamath Proof Explorer

Theorem iscvsp

Proof