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 e. ( S NMHom T ) <-> ( ( S e. NrmMod /\ T e. NrmMod ) /\ ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )

Proof

Step Hyp Ref Expression
1 df-nmhm
 |-  NMHom = ( s e. NrmMod , t e. NrmMod |-> ( ( s LMHom t ) i^i ( s NGHom t ) ) )
2 1 elmpocl
 |-  ( F e. ( S NMHom T ) -> ( S e. NrmMod /\ T e. 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 ) i^i ( s NGHom t ) ) = ( ( S LMHom T ) i^i ( S NGHom T ) ) )
6 ovex
 |-  ( S LMHom T ) e. _V
7 6 inex1
 |-  ( ( S LMHom T ) i^i ( S NGHom T ) ) e. _V
8 5 1 7 ovmpoa
 |-  ( ( S e. NrmMod /\ T e. NrmMod ) -> ( S NMHom T ) = ( ( S LMHom T ) i^i ( S NGHom T ) ) )
9 8 eleq2d
 |-  ( ( S e. NrmMod /\ T e. NrmMod ) -> ( F e. ( S NMHom T ) <-> F e. ( ( S LMHom T ) i^i ( S NGHom T ) ) ) )
10 elin
 |-  ( F e. ( ( S LMHom T ) i^i ( S NGHom T ) ) <-> ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) )
11 9 10 bitrdi
 |-  ( ( S e. NrmMod /\ T e. NrmMod ) -> ( F e. ( S NMHom T ) <-> ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )
12 2 11 biadanii
 |-  ( F e. ( S NMHom T ) <-> ( ( S e. NrmMod /\ T e. NrmMod ) /\ ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )