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

Proof

Step	Hyp	Ref	Expression
1		iscvsp.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
2		iscvsp.a	$$⊢\underset{\dot{}}{+}={+}_W$$
3		iscvsp.v	$$⊢V={\mathrm{Base}}_W$$
4		iscvsp.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
5		iscvsp.k	$$⊢K={\mathrm{Base}}_S$$
6		iscvsi.1	$$⊢W\in \mathrm{Grp}$$
7		iscvsi.2	$$⊢S={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
8		iscvsi.3	$$⊢S\in \mathrm{DivRing}$$
9		iscvsi.4	$$⊢K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
10		iscvsi.5	$$⊢x\in V\to 1\underset{\dot{}}{·}x=x$$
11		iscvsi.6	$$⊢\left(y\in K\wedge x\in V\right)\to y\underset{\dot{}}{·}x\in V$$
12		iscvsi.7	$$⊢\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)$$
13		iscvsi.8	$$⊢\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)$$
14		iscvsi.9	$$⊢\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)$$
15	8 7	pm3.2i	$$⊢\left(S\in \mathrm{DivRing}\wedge S={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)$$
16	6 15 9	3pm3.2i	$$⊢\left(W\in \mathrm{Grp}\wedge \left(S\in \mathrm{DivRing}\wedge S={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)\wedge K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
17	11	ancoms	$$⊢\left(x\in V\wedge y\in K\right)\to y\underset{\dot{}}{·}x\in V$$
18	12	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)$$
19	18	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)$$
20	19	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)$$
21	13 14	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)$$
22	21	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)$$
23	22	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)$$
24	23	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)$$
25	17 20 24	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)$$
26	25	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)$$
27	10 26	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)$$
28	27	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)$$
29	1 2 3 4 5	iscvsp	$$⊢W\in \mathrm{ℂVec}\leftrightarrow \left(\left(W\in \mathrm{Grp}\wedge \left(S\in \mathrm{DivRing}\wedge S={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)\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)$$
30	16 28 29	mpbir2an	$$⊢W\in \mathrm{ℂVec}$$