Theorem bj-isclm

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

	Ref	Expression
Hypotheses	bj-isclm.scal	|- ( ph -> F = ( Scalar ` W ) )
	bj-isclm.base	|- ( ph -> K = ( Base ` F ) )
Assertion	bj-isclm	|- ( ph -> ( W e. CMod <-> ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-isclm.scal	|- ( ph -> F = ( Scalar ` W ) )
2		bj-isclm.base	|- ( ph -> K = ( Base ` F ) )
3		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
4		eqid	|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
5	3 4	isclm	|- ( W e. CMod <-> ( W e. LMod /\ ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) /\ ( Base ` ( Scalar ` W ) ) e. ( SubRing ` CCfld ) ) )
6	1	eqcomd	|- ( ph -> ( Scalar ` W ) = F )
7		fveq2	|- ( F = ( Scalar ` W ) -> ( Base ` F ) = ( Base ` ( Scalar ` W ) ) )
8		eqtr	|- ( ( K = ( Base ` F ) /\ ( Base ` F ) = ( Base ` ( Scalar ` W ) ) ) -> K = ( Base ` ( Scalar ` W ) ) )
9	8	eqcomd	|- ( ( K = ( Base ` F ) /\ ( Base ` F ) = ( Base ` ( Scalar ` W ) ) ) -> ( Base ` ( Scalar ` W ) ) = K )
10	9	ex	|- ( K = ( Base ` F ) -> ( ( Base ` F ) = ( Base ` ( Scalar ` W ) ) -> ( Base ` ( Scalar ` W ) ) = K ) )
11	2 7 10	syl2im	|- ( ph -> ( F = ( Scalar ` W ) -> ( Base ` ( Scalar ` W ) ) = K ) )
12	1 11	mpd	|- ( ph -> ( Base ` ( Scalar ` W ) ) = K )
13	12	oveq2d	|- ( ph -> ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) = ( CCfld |`s K ) )
14	6 13	eqeq12d	|- ( ph -> ( ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) <-> F = ( CCfld |`s K ) ) )
15	12	eleq1d	|- ( ph -> ( ( Base ` ( Scalar ` W ) ) e. ( SubRing ` CCfld ) <-> K e. ( SubRing ` CCfld ) ) )
16	14 15	3anbi23d	|- ( ph -> ( ( W e. LMod /\ ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) /\ ( Base ` ( Scalar ` W ) ) e. ( SubRing ` CCfld ) ) <-> ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )
17	5 16	syl5bb	|- ( ph -> ( W e. CMod <-> ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )