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