Metamath Proof Explorer


Theorem nghmrcl1

Description: Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Assertion nghmrcl1 ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑆 ∈ NrmGrp )

Proof

Step Hyp Ref Expression
1 eqid ( 𝑆 normOp 𝑇 ) = ( 𝑆 normOp 𝑇 )
2 1 isnghm ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) ∈ ℝ ) ) )
3 2 simplbi ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) )
4 3 simpld ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑆 ∈ NrmGrp )