isclmi0

Description: Properties that determine a subcomplex module. (Contributed by NM, 5-Nov-2006) (Revised by AV, 4-Oct-2021)

	Ref	Expression
Hypotheses	isclmp.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	isclmp.a	$⊢ \underset{˙}{+} = +_{W}$
	isclmp.v	$⊢ V = {Base}_{W}$
	isclmp.s	$⊢ S = Scalar (W)$
	isclmp.k	$⊢ K = {Base}_{S}$
	isclmi0.1	$⊢ S = ℂ_{fld} ↾_{𝑠} K$
	isclmi0.2	$⊢ W \in Grp$
	isclmi0.3	$⊢ K \in SubRing (ℂ_{fld})$
	isclmi0.4	$⊢ x \in V \to 1 \underset{˙}{\cdot} x = x$
	isclmi0.5	$⊢ (y \in K \land x \in V) \to y \underset{˙}{\cdot} x \in V$
	isclmi0.6	$⊢ (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)$
	isclmi0.7	$⊢ (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)$
	isclmi0.8	$⊢ (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	isclmi0	$⊢ W \in CMod$

Proof

Step	Hyp	Ref	Expression
1		isclmp.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
2		isclmp.a	$⊢ \underset{˙}{+} = +_{W}$
3		isclmp.v	$⊢ V = {Base}_{W}$
4		isclmp.s	$⊢ S = Scalar (W)$
5		isclmp.k	$⊢ K = {Base}_{S}$
6		isclmi0.1	$⊢ S = ℂ_{fld} ↾_{𝑠} K$
7		isclmi0.2	$⊢ W \in Grp$
8		isclmi0.3	$⊢ K \in SubRing (ℂ_{fld})$
9		isclmi0.4	$⊢ x \in V \to 1 \underset{˙}{\cdot} x = x$
10		isclmi0.5	$⊢ (y \in K \land x \in V) \to y \underset{˙}{\cdot} x \in V$
11		isclmi0.6	$⊢ (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)$
12		isclmi0.7	$⊢ (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)$
13		isclmi0.8	$⊢ (y \in K \land z \in K \land x \in V) \to z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)$
14	7 6 8	3pm3.2i	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))$
15	10	ancoms	$⊢ (x \in V \land y \in K) \to y \underset{˙}{\cdot} x \in V$
16	11	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)$
17	16	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)$
18	17	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)$
19	12 13	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))$
20	19	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))$
21	20	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))$
22	21	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))$
23	15 18 22	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)))$
24	23	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)))$
25	9 24	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))))$
26	25	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))))$
27	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)))))$
28	14 26 27	mpbir2an	$⊢ W \in CMod$

Metamath Proof Explorer

Theorem isclmi0

Proof