Metamath Proof Explorer

Theorem isnmhm2

Description: A normed module homomorphism is a left module homomorphism with bounded norm (a bounded linear operator). (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypothesis isnmhm2.1 
|- N = ( S normOp T )
Assertion isnmhm2 
|- ( ( S e. NrmMod /\ T e. NrmMod /\ F e. ( S LMHom T ) ) -> ( F e. ( S NMHom T ) <-> ( N ` F ) e. RR ) )

Proof

Step Hyp Ref Expression
1 isnmhm2.1 
 |-  N = ( S normOp T )
2 isnmhm 
 |-  ( F e. ( S NMHom T ) <-> ( ( S e. NrmMod /\ T e. NrmMod ) /\ ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )
3 2 baib 
 |-  ( ( S e. NrmMod /\ T e. NrmMod ) -> ( F e. ( S NMHom T ) <-> ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )
4 3 baibd 
 |-  ( ( ( S e. NrmMod /\ T e. NrmMod ) /\ F e. ( S LMHom T ) ) -> ( F e. ( S NMHom T ) <-> F e. ( S NGHom T ) ) )
5 lmghm 
 |-  ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )
6 nlmngp 
 |-  ( S e. NrmMod -> S e. NrmGrp )
7 nlmngp 
 |-  ( T e. NrmMod -> T e. NrmGrp )
8 1 isnghm 
 |-  ( F e. ( S NGHom T ) <-> ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) )
9 8 baib 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( F e. ( S NGHom T ) <-> ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) )
10 6 7 9 syl2an 
 |-  ( ( S e. NrmMod /\ T e. NrmMod ) -> ( F e. ( S NGHom T ) <-> ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) )
11 10 baibd 
 |-  ( ( ( S e. NrmMod /\ T e. NrmMod ) /\ F e. ( S GrpHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) e. RR ) )
12 5 11 sylan2 
 |-  ( ( ( S e. NrmMod /\ T e. NrmMod ) /\ F e. ( S LMHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) e. RR ) )
13 4 12 bitrd 
 |-  ( ( ( S e. NrmMod /\ T e. NrmMod ) /\ F e. ( S LMHom T ) ) -> ( F e. ( S NMHom T ) <-> ( N ` F ) e. RR ) )
14 13 3impa 
 |-  ( ( S e. NrmMod /\ T e. NrmMod /\ F e. ( S LMHom T ) ) -> ( F e. ( S NMHom T ) <-> ( N ` F ) e. RR ) )