Metamath Proof Explorer

Theorem 0nmhm

Description: The zero operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015)

		Ref	Expression
	Hypotheses	0nmhm.1	$⊢ V = {Base}_{S}$
		0nmhm.2	$⊢ \underset{˙}{0} = 0_{T}$
		0nmhm.f	$⊢ F = Scalar (S)$
		0nmhm.g	$⊢ G = Scalar (T)$
	Assertion	0nmhm	$⊢ (S \in NrmMod \land T \in NrmMod \land F = G) \to V \times \{\underset{˙}{0}\} \in (S NMHom T)$

Proof

Step	Hyp	Ref	Expression
1		0nmhm.1	$⊢ V = {Base}_{S}$
2		0nmhm.2	$⊢ \underset{˙}{0} = 0_{T}$
3		0nmhm.f	$⊢ F = Scalar (S)$
4		0nmhm.g	$⊢ G = Scalar (T)$
5		nlmlmod	$⊢ S \in NrmMod \to S \in LMod$
6		nlmlmod	$⊢ T \in NrmMod \to T \in LMod$
7		id	$⊢ F = G \to F = G$
8	2 1 3 4	0lmhm	$⊢ (S \in LMod \land T \in LMod \land F = G) \to V \times \{\underset{˙}{0}\} \in (S LMHom T)$
9	5 6 7 8	syl3an	$⊢ (S \in NrmMod \land T \in NrmMod \land F = G) \to V \times \{\underset{˙}{0}\} \in (S LMHom T)$
10		nlmngp	$⊢ S \in NrmMod \to S \in NrmGrp$
11		nlmngp	$⊢ T \in NrmMod \to T \in NrmGrp$
12	1 2	0nghm	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to V \times \{\underset{˙}{0}\} \in (S NGHom T)$
13	10 11 12	syl2an	$⊢ (S \in NrmMod \land T \in NrmMod) \to V \times \{\underset{˙}{0}\} \in (S NGHom T)$
14	13	3adant3	$⊢ (S \in NrmMod \land T \in NrmMod \land F = G) \to V \times \{\underset{˙}{0}\} \in (S NGHom T)$
15		isnmhm	$⊢ V \times \{\underset{˙}{0}\} \in (S NMHom T) \leftrightarrow ((S \in NrmMod \land T \in NrmMod) \land (V \times \{\underset{˙}{0}\} \in (S LMHom T) \land V \times \{\underset{˙}{0}\} \in (S NGHom T)))$
16	15	baib	$⊢ (S \in NrmMod \land T \in NrmMod) \to (V \times \{\underset{˙}{0}\} \in (S NMHom T) \leftrightarrow (V \times \{\underset{˙}{0}\} \in (S LMHom T) \land V \times \{\underset{˙}{0}\} \in (S NGHom T)))$
17	16	3adant3	$⊢ (S \in NrmMod \land T \in NrmMod \land F = G) \to (V \times \{\underset{˙}{0}\} \in (S NMHom T) \leftrightarrow (V \times \{\underset{˙}{0}\} \in (S LMHom T) \land V \times \{\underset{˙}{0}\} \in (S NGHom T)))$
18	9 14 17	mpbir2and	$⊢ (S \in NrmMod \land T \in NrmMod \land F = G) \to V \times \{\underset{˙}{0}\} \in (S NMHom T)$