Theorem bj-isclm

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

	Ref	Expression
Hypotheses	bj-isclm.scal	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝑊 ) )
	bj-isclm.base	⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝐹 ) )
Assertion	bj-isclm	⊢ ( 𝜑 → ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-isclm.scal	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝑊 ) )
2		bj-isclm.base	⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝐹 ) )
3		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
4		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
5	3 4	isclm	⊢ ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( SubRing ‘ ℂfld ) ) )
6	1	eqcomd	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) = 𝐹 )
7		fveq2	⊢ ( 𝐹 = ( Scalar ‘ 𝑊 ) → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
8		eqtr	⊢ ( ( 𝐾 = ( Base ‘ 𝐹 ) ∧ ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
9	8	eqcomd	⊢ ( ( 𝐾 = ( Base ‘ 𝐹 ) ∧ ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = 𝐾 )
10	9	ex	⊢ ( 𝐾 = ( Base ‘ 𝐹 ) → ( ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = 𝐾 ) )
11	2 7 10	syl2im	⊢ ( 𝜑 → ( 𝐹 = ( Scalar ‘ 𝑊 ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = 𝐾 ) )
12	1 11	mpd	⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = 𝐾 )
13	12	oveq2d	⊢ ( 𝜑 → ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) = ( ℂfld ↾s 𝐾 ) )
14	6 13	eqeq12d	⊢ ( 𝜑 → ( ( Scalar ‘ 𝑊 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ 𝐹 = ( ℂfld ↾s 𝐾 ) ) )
15	12	eleq1d	⊢ ( 𝜑 → ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( SubRing ‘ ℂfld ) ↔ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )
16	14 15	3anbi23d	⊢ ( 𝜑 → ( ( 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( SubRing ‘ ℂfld ) ) ↔ ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
17	5 16	bitrid	⊢ ( 𝜑 → ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )