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 ⊢ V = Base S
0nghm.3 ⊢ 0 ˙ = 0 T
Assertion 0nghm ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → V × 0 ˙ ∈ S NGHom T

Proof

Step Hyp Ref Expression
1 0nghm.2 ⊢ V = Base S
2 0nghm.3 ⊢ 0 ˙ = 0 T
3 eqid ⊢ S normOp T = S normOp T
4 3 1 2 nmo0 ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → S normOp T ⁡ V × 0 ˙ = 0
5 0re ⊢ 0 ∈ ℝ
6 4 5 eqeltrdi ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → S normOp T ⁡ V × 0 ˙ ∈ ℝ
7 ngpgrp ⊢ S ∈ NrmGrp → S ∈ Grp
8 ngpgrp ⊢ T ∈ NrmGrp → T ∈ Grp
9 2 1 0ghm ⊢ S ∈ Grp ∧ T ∈ Grp → V × 0 ˙ ∈ S GrpHom T
10 7 8 9 syl2an ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → V × 0 ˙ ∈ S GrpHom T
11 3 isnghm2 ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp ∧ V × 0 ˙ ∈ S GrpHom T → V × 0 ˙ ∈ S NGHom T ↔ S normOp T ⁡ V × 0 ˙ ∈ ℝ
12 10 11 mpd3an3 ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → V × 0 ˙ ∈ S NGHom T ↔ S normOp T ⁡ V × 0 ˙ ∈ ℝ
13 6 12 mpbird ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → V × 0 ˙ ∈ S NGHom T