This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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