Metamath Proof Explorer

Theorem isnmhm

Description: A normed module homomorphism is a left module homomorphism which is also a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Assertion isnmhm ⊢ F ∈ S NMHom T ↔ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F ∈ S LMHom T ∧ F ∈ S NGHom T

Proof

Step Hyp Ref Expression
1 df-nmhm ⊢ NMHom = s ∈ NrmMod , t ∈ NrmMod ⟼ s LMHom t ∩ s NGHom t
2 1 elmpocl ⊢ F ∈ S NMHom T → S ∈ NrmMod ∧ T ∈ NrmMod
3 oveq12 ⊢ s = S ∧ t = T → s LMHom t = S LMHom T
4 oveq12 ⊢ s = S ∧ t = T → s NGHom t = S NGHom T
5 3 4 ineq12d ⊢ s = S ∧ t = T → s LMHom t ∩ s NGHom t = S LMHom T ∩ S NGHom T
6 ovex ⊢ S LMHom T ∈ V
7 6 inex1 ⊢ S LMHom T ∩ S NGHom T ∈ V
8 5 1 7 ovmpoa ⊢ S ∈ NrmMod ∧ T ∈ NrmMod → S NMHom T = S LMHom T ∩ S NGHom T
9 8 eleq2d ⊢ S ∈ NrmMod ∧ T ∈ NrmMod → F ∈ S NMHom T ↔ F ∈ S LMHom T ∩ S NGHom T
10 elin ⊢ F ∈ S LMHom T ∩ S NGHom T ↔ F ∈ S LMHom T ∧ F ∈ S NGHom T
11 9 10 bitrdi ⊢ S ∈ NrmMod ∧ T ∈ NrmMod → F ∈ S NMHom T ↔ F ∈ S LMHom T ∧ F ∈ S NGHom T
12 2 11 biadanii ⊢ F ∈ S NMHom T ↔ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F ∈ S LMHom T ∧ F ∈ S NGHom T