Metamath Proof Explorer


Theorem 0nghm

Description: The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypotheses 0nghm.2 𝑉 = ( Base ‘ 𝑆 )
0nghm.3 0 = ( 0g𝑇 )
Assertion 0nghm ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 0nghm.2 𝑉 = ( Base ‘ 𝑆 )
2 0nghm.3 0 = ( 0g𝑇 )
3 eqid ( 𝑆 normOp 𝑇 ) = ( 𝑆 normOp 𝑇 )
4 3 1 2 nmo0 ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( ( 𝑆 normOp 𝑇 ) ‘ ( 𝑉 × { 0 } ) ) = 0 )
5 0re 0 ∈ ℝ
6 4 5 eqeltrdi ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( ( 𝑆 normOp 𝑇 ) ‘ ( 𝑉 × { 0 } ) ) ∈ ℝ )
7 ngpgrp ( 𝑆 ∈ NrmGrp → 𝑆 ∈ Grp )
8 ngpgrp ( 𝑇 ∈ NrmGrp → 𝑇 ∈ Grp )
9 2 1 0ghm ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 GrpHom 𝑇 ) )
10 7 8 9 syl2an ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 GrpHom 𝑇 ) )
11 3 isnghm2 ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ ( 𝑉 × { 0 } ) ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( ( 𝑆 normOp 𝑇 ) ‘ ( 𝑉 × { 0 } ) ) ∈ ℝ ) )
12 10 11 mpd3an3 ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( ( 𝑆 normOp 𝑇 ) ‘ ( 𝑉 × { 0 } ) ) ∈ ℝ ) )
13 6 12 mpbird ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) )