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 ⊢ F ∈ S LMHom T → S ∈ CMod ↔ T ∈ CMod

Proof

Step Hyp Ref Expression
1 lmhmlmod1 ⊢ F ∈ S LMHom T → S ∈ LMod
2 lmhmlmod2 ⊢ F ∈ S LMHom T → T ∈ LMod
3 1 2 2thd ⊢ F ∈ S LMHom T → S ∈ LMod ↔ T ∈ LMod
4 eqid ⊢ Scalar ⁡ S = Scalar ⁡ S
5 eqid ⊢ Scalar ⁡ T = Scalar ⁡ T
6 4 5 lmhmsca ⊢ F ∈ S LMHom T → Scalar ⁡ T = Scalar ⁡ S
7 6 eqcomd ⊢ F ∈ S LMHom T → Scalar ⁡ S = Scalar ⁡ T
8 7 fveq2d ⊢ F ∈ S LMHom T → Base Scalar ⁡ S = Base Scalar ⁡ T
9 8 oveq2d ⊢ F ∈ S LMHom T → ℂ fld ↾ 𝑠 Base Scalar ⁡ S = ℂ fld ↾ 𝑠 Base Scalar ⁡ T
10 7 9 eqeq12d ⊢ F ∈ S LMHom T → Scalar ⁡ S = ℂ fld ↾ 𝑠 Base Scalar ⁡ S ↔ Scalar ⁡ T = ℂ fld ↾ 𝑠 Base Scalar ⁡ T
11 8 eleq1d ⊢ F ∈ S LMHom T → Base Scalar ⁡ S ∈ SubRing ⁡ ℂ fld ↔ Base Scalar ⁡ T ∈ SubRing ⁡ ℂ fld
12 3 10 11 3anbi123d ⊢ F ∈ S LMHom T → S ∈ LMod ∧ Scalar ⁡ S = ℂ fld ↾ 𝑠 Base Scalar ⁡ S ∧ Base Scalar ⁡ S ∈ SubRing ⁡ ℂ fld ↔ T ∈ LMod ∧ Scalar ⁡ T = ℂ fld ↾ 𝑠 Base Scalar ⁡ T ∧ Base Scalar ⁡ T ∈ SubRing ⁡ ℂ fld
13 eqid ⊢ Base Scalar ⁡ S = Base Scalar ⁡ S
14 4 13 isclm ⊢ S ∈ CMod ↔ S ∈ LMod ∧ Scalar ⁡ S = ℂ fld ↾ 𝑠 Base Scalar ⁡ S ∧ Base Scalar ⁡ S ∈ SubRing ⁡ ℂ fld
15 eqid ⊢ Base Scalar ⁡ T = Base Scalar ⁡ T
16 5 15 isclm ⊢ T ∈ CMod ↔ T ∈ LMod ∧ Scalar ⁡ T = ℂ fld ↾ 𝑠 Base Scalar ⁡ T ∧ Base Scalar ⁡ T ∈ SubRing ⁡ ℂ fld
17 12 14 16 3bitr4g ⊢ F ∈ S LMHom T → S ∈ CMod ↔ T ∈ CMod