nmoeq0

Description: The operator norm is zero only for 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	nmoeq0	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (N (F) = 0 \leftrightarrow F = V \times \{\underset{˙}{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		id	$⊢ N (F) = 0 \to N (F) = 0$
5		0re	$⊢ 0 \in ℝ$
6	4 5	eqeltrdi	$⊢ N (F) = 0 \to N (F) \in ℝ$
7	1	isnghm2	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (F \in (S NGHom T) \leftrightarrow N (F) \in ℝ)$
8	7	biimpar	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) \in ℝ) \to F \in (S NGHom T)$
9	6 8	sylan2	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \to F \in (S NGHom T)$
10		eqid	$⊢ norm (S) = norm (S)$
11		eqid	$⊢ norm (T) = norm (T)$
12	1 2 10 11	nmoi	$⊢ (F \in (S NGHom T) \land x \in V) \to norm (T) (F (x)) \leq N (F) norm (S) (x)$
13	9 12	sylan	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to norm (T) (F (x)) \leq N (F) norm (S) (x)$
14		simplr	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to N (F) = 0$
15	14	oveq1d	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to N (F) norm (S) (x) = 0 \cdot norm (S) (x)$
16		simpl1	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \to S \in NrmGrp$
17	2 10	nmcl	$⊢ (S \in NrmGrp \land x \in V) \to norm (S) (x) \in ℝ$
18	16 17	sylan	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to norm (S) (x) \in ℝ$
19	18	recnd	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to norm (S) (x) \in ℂ$
20	19	mul02d	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to 0 \cdot norm (S) (x) = 0$
21	15 20	eqtrd	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to N (F) norm (S) (x) = 0$
22	13 21	breqtrd	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to norm (T) (F (x)) \leq 0$
23		simpll2	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to T \in NrmGrp$
24		simpl3	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \to F \in (S GrpHom T)$
25		eqid	$⊢ {Base}_{T} = {Base}_{T}$
26	2 25	ghmf	$⊢ F \in (S GrpHom T) \to F : V ⟶ {Base}_{T}$
27	24 26	syl	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \to F : V ⟶ {Base}_{T}$
28	27	ffvelcdmda	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to F (x) \in {Base}_{T}$
29	25 11	nmge0	$⊢ (T \in NrmGrp \land F (x) \in {Base}_{T}) \to 0 \leq norm (T) (F (x))$
30	23 28 29	syl2anc	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to 0 \leq norm (T) (F (x))$
31	25 11	nmcl	$⊢ (T \in NrmGrp \land F (x) \in {Base}_{T}) \to norm (T) (F (x)) \in ℝ$
32	23 28 31	syl2anc	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to norm (T) (F (x)) \in ℝ$
33		letri3	$⊢ (norm (T) (F (x)) \in ℝ \land 0 \in ℝ) \to (norm (T) (F (x)) = 0 \leftrightarrow (norm (T) (F (x)) \leq 0 \land 0 \leq norm (T) (F (x))))$
34	32 5 33	sylancl	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to (norm (T) (F (x)) = 0 \leftrightarrow (norm (T) (F (x)) \leq 0 \land 0 \leq norm (T) (F (x))))$
35	22 30 34	mpbir2and	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to norm (T) (F (x)) = 0$
36	25 11 3	nmeq0	$⊢ (T \in NrmGrp \land F (x) \in {Base}_{T}) \to (norm (T) (F (x)) = 0 \leftrightarrow F (x) = \underset{˙}{0})$
37	23 28 36	syl2anc	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to (norm (T) (F (x)) = 0 \leftrightarrow F (x) = \underset{˙}{0})$
38	35 37	mpbid	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \land x \in V) \to F (x) = \underset{˙}{0}$
39	38	mpteq2dva	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \to (x \in V ⟼ F (x)) = (x \in V ⟼ \underset{˙}{0})$
40	27	feqmptd	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \to F = (x \in V ⟼ F (x))$
41		fconstmpt	$⊢ V \times \{\underset{˙}{0}\} = (x \in V ⟼ \underset{˙}{0})$
42	41	a1i	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \to V \times \{\underset{˙}{0}\} = (x \in V ⟼ \underset{˙}{0})$
43	39 40 42	3eqtr4d	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) = 0) \to F = V \times \{\underset{˙}{0}\}$
44	43	ex	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (N (F) = 0 \to F = V \times \{\underset{˙}{0}\})$
45	1 2 3	nmo0	$⊢ (S \in NrmGrp \land T \in NrmGrp) \to N (V \times \{\underset{˙}{0}\}) = 0$
46	45	3adant3	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (V \times \{\underset{˙}{0}\}) = 0$
47		fveqeq2	$⊢ F = V \times \{\underset{˙}{0}\} \to (N (F) = 0 \leftrightarrow N (V \times \{\underset{˙}{0}\}) = 0)$
48	46 47	syl5ibrcom	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (F = V \times \{\underset{˙}{0}\} \to N (F) = 0)$
49	44 48	impbid	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (N (F) = 0 \leftrightarrow F = V \times \{\underset{˙}{0}\})$

Metamath Proof Explorer

Theorem nmoeq0

Proof