This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )