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