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	$⊢ \underset{˙}{0} = 0_{T}$
Assertion	0nghm	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to V \times \{\underset{˙}{0}\} \in (S NGHom T)$

Step	Hyp	Ref	Expression
1		0nghm.2	$⊢ V = {Base}_{S}$
2		0nghm.3	$⊢ \underset{˙}{0} = 0_{T}$
3		eqid	$⊢ S normOp T = S normOp T$
4	3 1 2	nmo0	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to (S normOp T) (V \times \{\underset{˙}{0}\}) = 0$
5		0re	$⊢ 0 \in ℝ$
6	4 5	eqeltrdi	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to (S normOp T) (V \times \{\underset{˙}{0}\}) \in ℝ$
7		ngpgrp	$⊢ S \in NrmGrp \to S \in Grp$
8		ngpgrp	$⊢ T \in NrmGrp \to T \in Grp$
9	2 1	0ghm	$⊢ (S \in Grp \land T \in Grp) \to V \times \{\underset{˙}{0}\} \in (S GrpHom T)$
10	7 8 9	syl2an	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to V \times \{\underset{˙}{0}\} \in (S GrpHom T)$
11	3	isnghm2	$⊢ (S \in NrmGrp \land T \in NrmGrp \land V \times \{\underset{˙}{0}\} \in (S GrpHom T)) \to (V \times \{\underset{˙}{0}\} \in (S NGHom T) \leftrightarrow (S normOp T) (V \times \{\underset{˙}{0}\}) \in ℝ)$
12	10 11	mpd3an3	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to (V \times \{\underset{˙}{0}\} \in (S NGHom T) \leftrightarrow (S normOp T) (V \times \{\underset{˙}{0}\}) \in ℝ)$
13	6 12	mpbird	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to V \times \{\underset{˙}{0}\} \in (S NGHom T)$

Metamath Proof Explorer