Theorem bj-isclm

Description: The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024)

	Ref	Expression
Hypotheses	bj-isclm.scal	$$⊢\phi \to F=\mathrm{Scalar}\left(W\right)$$
	bj-isclm.base	$$⊢\phi \to K={\mathrm{Base}}_F$$
Assertion	bj-isclm	$$⊢\phi \to \left(W\in \mathrm{CMod}\leftrightarrow \left(W\in \mathrm{LMod}\wedge F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\wedge K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-isclm.scal	$$⊢\phi \to F=\mathrm{Scalar}\left(W\right)$$
2		bj-isclm.base	$$⊢\phi \to K={\mathrm{Base}}_F$$
3		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
4		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
5	3 4	isclm	$$⊢W\in \mathrm{CMod}\leftrightarrow \left(W\in \mathrm{LMod}\wedge \mathrm{Scalar}\left(W\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
6	1	eqcomd	$$⊢\phi \to \mathrm{Scalar}\left(W\right)=F$$
7		fveq2	$$⊢F=\mathrm{Scalar}\left(W\right)\to {\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
8		eqtr	$$⊢\left(K={\mathrm{Base}}_F\wedge {\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to K={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
9	8	eqcomd	$$⊢\left(K={\mathrm{Base}}_F\wedge {\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}=K$$
10	9	ex	$$⊢K={\mathrm{Base}}_F\to \left({\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\to {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}=K\right)$$
11	2 7 10	syl2im	$$⊢\phi \to \left(F=\mathrm{Scalar}\left(W\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}=K\right)$$
12	1 11	mpd	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}=K$$
13	12	oveq2d	$$⊢\phi \to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
14	6 13	eqeq12d	$$⊢\phi \to \left(\mathrm{Scalar}\left(W\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\leftrightarrow F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)$$
15	12	eleq1d	$$⊢\phi \to \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\leftrightarrow K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
16	14 15	3anbi23d	$$⊢\phi \to \left(\left(W\in \mathrm{LMod}\wedge \mathrm{Scalar}\left(W\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\leftrightarrow \left(W\in \mathrm{LMod}\wedge F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\wedge K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\right)$$
17	5 16	bitrid	$$⊢\phi \to \left(W\in \mathrm{CMod}\leftrightarrow \left(W\in \mathrm{LMod}\wedge F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\wedge K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\right)$$