Theorem lmhmclm

Description: The domain of a linear operator is a subcomplex module iff the range is. (Contributed by Mario Carneiro, 21-Oct-2015)

	Ref	Expression
Assertion	lmhmclm	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝑆 ∈ ℂMod ↔ 𝑇 ∈ ℂMod ) )

Proof

Step	Hyp	Ref	Expression
1		lmhmlmod1	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
2		lmhmlmod2	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
3	1 2	2thd	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝑆 ∈ LMod ↔ 𝑇 ∈ LMod ) )
4		eqid	⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
5		eqid	⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
6	4 5	lmhmsca	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) )
7	6	eqcomd	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑇 ) )
8	7	fveq2d	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
9	8	oveq2d	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) )
10	7 9	eqeq12d	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( ( Scalar ‘ 𝑆 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ↔ ( Scalar ‘ 𝑇 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) ) )
11	8	eleq1d	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∈ ( SubRing ‘ ℂfld ) ↔ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∈ ( SubRing ‘ ℂfld ) ) )
12	3 10 11	3anbi123d	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( ( 𝑆 ∈ LMod ∧ ( Scalar ‘ 𝑆 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∈ ( SubRing ‘ ℂfld ) ) ↔ ( 𝑇 ∈ LMod ∧ ( Scalar ‘ 𝑇 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) ∧ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∈ ( SubRing ‘ ℂfld ) ) ) )
13		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
14	4 13	isclm	⊢ ( 𝑆 ∈ ℂMod ↔ ( 𝑆 ∈ LMod ∧ ( Scalar ‘ 𝑆 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∈ ( SubRing ‘ ℂfld ) ) )
15		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) )
16	5 15	isclm	⊢ ( 𝑇 ∈ ℂMod ↔ ( 𝑇 ∈ LMod ∧ ( Scalar ‘ 𝑇 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) ∧ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∈ ( SubRing ‘ ℂfld ) ) )
17	12 14 16	3bitr4g	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝑆 ∈ ℂMod ↔ 𝑇 ∈ ℂMod ) )