Proof of Theorem lmhmclm
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lmhmlmod1 21032 | . . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) | 
| 2 |  | lmhmlmod2 21031 | . . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) | 
| 3 | 1, 2 | 2thd 265 | . . 3
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑆 ∈ LMod ↔ 𝑇 ∈ LMod)) | 
| 4 |  | eqid 2737 | . . . . . 6
⊢
(Scalar‘𝑆) =
(Scalar‘𝑆) | 
| 5 |  | eqid 2737 | . . . . . 6
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) | 
| 6 | 4, 5 | lmhmsca 21029 | . . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑇) = (Scalar‘𝑆)) | 
| 7 | 6 | eqcomd 2743 | . . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑆) = (Scalar‘𝑇)) | 
| 8 | 7 | fveq2d 6910 | . . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Base‘(Scalar‘𝑆)) =
(Base‘(Scalar‘𝑇))) | 
| 9 | 8 | oveq2d 7447 | . . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (ℂfld
↾s (Base‘(Scalar‘𝑆))) = (ℂfld
↾s (Base‘(Scalar‘𝑇)))) | 
| 10 | 7, 9 | eqeq12d 2753 | . . 3
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((Scalar‘𝑆) = (ℂfld
↾s (Base‘(Scalar‘𝑆))) ↔ (Scalar‘𝑇) = (ℂfld
↾s (Base‘(Scalar‘𝑇))))) | 
| 11 | 8 | eleq1d 2826 | . . 3
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((Base‘(Scalar‘𝑆)) ∈
(SubRing‘ℂfld) ↔ (Base‘(Scalar‘𝑇)) ∈
(SubRing‘ℂfld))) | 
| 12 | 3, 10, 11 | 3anbi123d 1438 | . 2
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑆 ∈ LMod ∧ (Scalar‘𝑆) = (ℂfld
↾s (Base‘(Scalar‘𝑆))) ∧ (Base‘(Scalar‘𝑆)) ∈
(SubRing‘ℂfld)) ↔ (𝑇 ∈ LMod ∧ (Scalar‘𝑇) = (ℂfld
↾s (Base‘(Scalar‘𝑇))) ∧ (Base‘(Scalar‘𝑇)) ∈
(SubRing‘ℂfld)))) | 
| 13 |  | eqid 2737 | . . 3
⊢
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆)) | 
| 14 | 4, 13 | isclm 25097 | . 2
⊢ (𝑆 ∈ ℂMod ↔ (𝑆 ∈ LMod ∧
(Scalar‘𝑆) =
(ℂfld ↾s (Base‘(Scalar‘𝑆))) ∧
(Base‘(Scalar‘𝑆)) ∈
(SubRing‘ℂfld))) | 
| 15 |  | eqid 2737 | . . 3
⊢
(Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇)) | 
| 16 | 5, 15 | isclm 25097 | . 2
⊢ (𝑇 ∈ ℂMod ↔ (𝑇 ∈ LMod ∧
(Scalar‘𝑇) =
(ℂfld ↾s (Base‘(Scalar‘𝑇))) ∧
(Base‘(Scalar‘𝑇)) ∈
(SubRing‘ℂfld))) | 
| 17 | 12, 14, 16 | 3bitr4g 314 | 1
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑆 ∈ ℂMod ↔ 𝑇 ∈ ℂMod)) |