Theorem 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{\dot{}}{·}={\cdot }_W$$
	isclmp.a	$$⊢\underset{\dot{}}{+}={+}_W$$
	isclmp.v	$$⊢V={\mathrm{Base}}_W$$
	isclmp.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
	isclmp.k	$$⊢K={\mathrm{Base}}_S$$
	isclmi0.1	$$⊢S={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
	isclmi0.2	$$⊢W\in \mathrm{Grp}$$
	isclmi0.3	$$⊢K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
	isclmi0.4	$$⊢x\in V\to 1\underset{\dot{}}{·}x=x$$
	isclmi0.5	$$⊢\left(y\in K\wedge x\in V\right)\to y\underset{\dot{}}{·}x\in V$$
	isclmi0.6	$$⊢\left(y\in K\wedge x\in V\wedge z\in V\right)\to y\underset{\dot{}}{·}\left(x\underset{\dot{}}{+}z\right)=\left(y\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
	isclmi0.7	$$⊢\left(y\in K\wedge z\in K\wedge x\in V\right)\to \left(z+y\right)\underset{\dot{}}{·}x=\left(z\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}x\right)$$
	isclmi0.8	$$⊢\left(y\in K\wedge z\in K\wedge x\in V\right)\to zy\underset{\dot{}}{·}x=z\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}x\right)$$
Assertion	isclmi0	$$⊢W\in \mathrm{CMod}$$

Proof

Step	Hyp	Ref	Expression
1		isclmp.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
2		isclmp.a	$$⊢\underset{\dot{}}{+}={+}_W$$
3		isclmp.v	$$⊢V={\mathrm{Base}}_W$$
4		isclmp.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
5		isclmp.k	$$⊢K={\mathrm{Base}}_S$$
6		isclmi0.1	$$⊢S={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
7		isclmi0.2	$$⊢W\in \mathrm{Grp}$$
8		isclmi0.3	$$⊢K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
9		isclmi0.4	$$⊢x\in V\to 1\underset{\dot{}}{·}x=x$$
10		isclmi0.5	$$⊢\left(y\in K\wedge x\in V\right)\to y\underset{\dot{}}{·}x\in V$$
11		isclmi0.6	$$⊢\left(y\in K\wedge x\in V\wedge z\in V\right)\to y\underset{\dot{}}{·}\left(x\underset{\dot{}}{+}z\right)=\left(y\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
12		isclmi0.7	$$⊢\left(y\in K\wedge z\in K\wedge x\in V\right)\to \left(z+y\right)\underset{\dot{}}{·}x=\left(z\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}x\right)$$
13		isclmi0.8	$$⊢\left(y\in K\wedge z\in K\wedge x\in V\right)\to zy\underset{\dot{}}{·}x=z\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}x\right)$$
14	7 6 8	3pm3.2i	$$⊢\left(W\in \mathrm{Grp}\wedge S={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\wedge K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
15	10	ancoms	$$⊢\left(x\in V\wedge y\in K\right)\to y\underset{\dot{}}{·}x\in V$$
16	11	3com12	$$⊢\left(x\in V\wedge y\in K\wedge z\in V\right)\to y\underset{\dot{}}{·}\left(x\underset{\dot{}}{+}z\right)=\left(y\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
17	16	3expa	$$⊢\left(\left(x\in V\wedge y\in K\right)\wedge z\in V\right)\to y\underset{\dot{}}{·}\left(x\underset{\dot{}}{+}z\right)=\left(y\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
18	17	ralrimiva	$$⊢\left(x\in V\wedge y\in K\right)\to \forall z\in Vy\underset{\dot{}}{·}\left(x\underset{\dot{}}{+}z\right)=\left(y\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
19	12 13	jca	$$⊢\left(y\in K\wedge z\in K\wedge x\in V\right)\to \left(\left(z+y\right)\underset{\dot{}}{·}x=\left(z\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}x\right)\wedge zy\underset{\dot{}}{·}x=z\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}x\right)\right)$$
20	19	3comr	$$⊢\left(x\in V\wedge y\in K\wedge z\in K\right)\to \left(\left(z+y\right)\underset{\dot{}}{·}x=\left(z\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}x\right)\wedge zy\underset{\dot{}}{·}x=z\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}x\right)\right)$$
21	20	3expa	$$⊢\left(\left(x\in V\wedge y\in K\right)\wedge z\in K\right)\to \left(\left(z+y\right)\underset{\dot{}}{·}x=\left(z\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}x\right)\wedge zy\underset{\dot{}}{·}x=z\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}x\right)\right)$$
22	21	ralrimiva	$$⊢\left(x\in V\wedge y\in K\right)\to \forall z\in K\left(\left(z+y\right)\underset{\dot{}}{·}x=\left(z\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}x\right)\wedge zy\underset{\dot{}}{·}x=z\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}x\right)\right)$$
23	15 18 22	3jca	$$⊢\left(x\in V\wedge y\in K\right)\to \left(y\underset{\dot{}}{·}x\in V\wedge \forall z\in Vy\underset{\dot{}}{·}\left(x\underset{\dot{}}{+}z\right)=\left(y\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\wedge \forall z\in K\left(\left(z+y\right)\underset{\dot{}}{·}x=\left(z\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}x\right)\wedge zy\underset{\dot{}}{·}x=z\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}x\right)\right)\right)$$
24	23	ralrimiva	$$⊢x\in V\to \forall y\in K\left(y\underset{\dot{}}{·}x\in V\wedge \forall z\in Vy\underset{\dot{}}{·}\left(x\underset{\dot{}}{+}z\right)=\left(y\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\wedge \forall z\in K\left(\left(z+y\right)\underset{\dot{}}{·}x=\left(z\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}x\right)\wedge zy\underset{\dot{}}{·}x=z\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}x\right)\right)\right)$$
25	9 24	jca	$$⊢x\in V\to \left(1\underset{\dot{}}{·}x=x\wedge \forall y\in K\left(y\underset{\dot{}}{·}x\in V\wedge \forall z\in Vy\underset{\dot{}}{·}\left(x\underset{\dot{}}{+}z\right)=\left(y\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\wedge \forall z\in K\left(\left(z+y\right)\underset{\dot{}}{·}x=\left(z\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}x\right)\wedge zy\underset{\dot{}}{·}x=z\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}x\right)\right)\right)\right)$$
26	25	rgen	$$⊢\forall x\in V\left(1\underset{\dot{}}{·}x=x\wedge \forall y\in K\left(y\underset{\dot{}}{·}x\in V\wedge \forall z\in Vy\underset{\dot{}}{·}\left(x\underset{\dot{}}{+}z\right)=\left(y\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\wedge \forall z\in K\left(\left(z+y\right)\underset{\dot{}}{·}x=\left(z\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}x\right)\wedge zy\underset{\dot{}}{·}x=z\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}x\right)\right)\right)\right)$$
27	1 2 3 4 5	isclmp	$$⊢W\in \mathrm{CMod}\leftrightarrow \left(\left(W\in \mathrm{Grp}\wedge S={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\wedge K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\wedge \forall x\in V\left(1\underset{\dot{}}{·}x=x\wedge \forall y\in K\left(y\underset{\dot{}}{·}x\in V\wedge \forall z\in Vy\underset{\dot{}}{·}\left(x\underset{\dot{}}{+}z\right)=\left(y\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\wedge \forall z\in K\left(\left(z+y\right)\underset{\dot{}}{·}x=\left(z\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}x\right)\wedge zy\underset{\dot{}}{·}x=z\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}x\right)\right)\right)\right)\right)$$
28	14 26 27	mpbir2an	$$⊢W\in \mathrm{CMod}$$