Metamath Proof Explorer

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	bitrid	\|- ( ph -> ( W e. CMod <-> ( W e. LMod /\ F = ( CCfld \|`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )