nmo0

Description: The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015)

	Ref	Expression
Hypotheses	nmo0.1	$⊢ N = S normOp T$
	nmo0.2	$⊢ V = {Base}_{S}$
	nmo0.3	$⊢ \underset{˙}{0} = 0_{T}$
Assertion	nmo0	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to N (V \times \{\underset{˙}{0}\}) = 0$

Proof

Step	Hyp	Ref	Expression
1		nmo0.1	$⊢ N = S normOp T$
2		nmo0.2	$⊢ V = {Base}_{S}$
3		nmo0.3	$⊢ \underset{˙}{0} = 0_{T}$
4		eqid	$⊢ norm (S) = norm (S)$
5		eqid	$⊢ norm (T) = norm (T)$
6		eqid	$⊢ 0_{S} = 0_{S}$
7		simpl	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to S \in NrmGrp$
8		simpr	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to T \in NrmGrp$
9		ngpgrp	$⊢ S \in NrmGrp \to S \in Grp$
10		ngpgrp	$⊢ T \in NrmGrp \to T \in Grp$
11	3 2	0ghm	$⊢ (S \in Grp \land T \in Grp) \to V \times \{\underset{˙}{0}\} \in (S GrpHom T)$
12	9 10 11	syl2an	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to V \times \{\underset{˙}{0}\} \in (S GrpHom T)$
13		0red	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to 0 \in ℝ$
14		0le0	$⊢ 0 \leq 0$
15	14	a1i	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to 0 \leq 0$
16	3	fvexi	$⊢ \underset{˙}{0} \in V$
17	16	fvconst2	$⊢ x \in V \to (V \times \{\underset{˙}{0}\}) (x) = \underset{˙}{0}$
18	17	ad2antrl	$⊢ ((S \in NrmGrp \land T \in NrmGrp) \land (x \in V \land x \neq 0_{S})) \to (V \times \{\underset{˙}{0}\}) (x) = \underset{˙}{0}$
19	18	fveq2d	$⊢ ((S \in NrmGrp \land T \in NrmGrp) \land (x \in V \land x \neq 0_{S})) \to norm (T) ((V \times \{\underset{˙}{0}\}) (x)) = norm (T) (\underset{˙}{0})$
20	5 3	nm0	$⊢ T \in NrmGrp \to norm (T) (\underset{˙}{0}) = 0$
21	20	ad2antlr	$⊢ ((S \in NrmGrp \land T \in NrmGrp) \land (x \in V \land x \neq 0_{S})) \to norm (T) (\underset{˙}{0}) = 0$
22	19 21	eqtrd	$⊢ ((S \in NrmGrp \land T \in NrmGrp) \land (x \in V \land x \neq 0_{S})) \to norm (T) ((V \times \{\underset{˙}{0}\}) (x)) = 0$
23	2 4	nmcl	$⊢ (S \in NrmGrp \land x \in V) \to norm (S) (x) \in ℝ$
24	23	ad2ant2r	$⊢ ((S \in NrmGrp \land T \in NrmGrp) \land (x \in V \land x \neq 0_{S})) \to norm (S) (x) \in ℝ$
25	24	recnd	$⊢ ((S \in NrmGrp \land T \in NrmGrp) \land (x \in V \land x \neq 0_{S})) \to norm (S) (x) \in ℂ$
26	25	mul02d	$⊢ ((S \in NrmGrp \land T \in NrmGrp) \land (x \in V \land x \neq 0_{S})) \to 0 \cdot norm (S) (x) = 0$
27	14 26	breqtrrid	$⊢ ((S \in NrmGrp \land T \in NrmGrp) \land (x \in V \land x \neq 0_{S})) \to 0 \leq 0 \cdot norm (S) (x)$
28	22 27	eqbrtrd	$⊢ ((S \in NrmGrp \land T \in NrmGrp) \land (x \in V \land x \neq 0_{S})) \to norm (T) ((V \times \{\underset{˙}{0}\}) (x)) \leq 0 \cdot norm (S) (x)$
29	1 2 4 5 6 7 8 12 13 15 28	nmolb2d	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to N (V \times \{\underset{˙}{0}\}) \leq 0$
30	1	nmoge0	$⊢ (S \in NrmGrp \land T \in NrmGrp \land V \times \{\underset{˙}{0}\} \in (S GrpHom T)) \to 0 \leq N (V \times \{\underset{˙}{0}\})$
31	12 30	mpd3an3	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to 0 \leq N (V \times \{\underset{˙}{0}\})$
32	1	nmocl	$⊢ (S \in NrmGrp \land T \in NrmGrp \land V \times \{\underset{˙}{0}\} \in (S GrpHom T)) \to N (V \times \{\underset{˙}{0}\}) \in ℝ^{*}$
33	12 32	mpd3an3	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to N (V \times \{\underset{˙}{0}\}) \in ℝ^{*}$
34		0xr	$⊢ 0 \in ℝ^{*}$
35		xrletri3	$⊢ (N (V \times \{\underset{˙}{0}\}) \in ℝ^{} \land 0 \in ℝ^{}) \to (N (V \times \{\underset{˙}{0}\}) = 0 \leftrightarrow (N (V \times \{\underset{˙}{0}\}) \leq 0 \land 0 \leq N (V \times \{\underset{˙}{0}\})))$
36	33 34 35	sylancl	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to (N (V \times \{\underset{˙}{0}\}) = 0 \leftrightarrow (N (V \times \{\underset{˙}{0}\}) \leq 0 \land 0 \leq N (V \times \{\underset{˙}{0}\})))$
37	29 31 36	mpbir2and	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to N (V \times \{\underset{˙}{0}\}) = 0$

Metamath Proof Explorer

Theorem nmo0

Proof