Theorem nmoeq0

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

	Ref	Expression
Hypotheses	nmo0.1	⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
	nmo0.2	⊢ 𝑉 = ( Base ‘ 𝑆 )
	nmo0.3	⊢ 0 = ( 0g ‘ 𝑇 )
Assertion	nmoeq0	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( ( 𝑁 ‘ 𝐹 ) = 0 ↔ 𝐹 = ( 𝑉 × { 0 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmo0.1	⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2		nmo0.2	⊢ 𝑉 = ( Base ‘ 𝑆 )
3		nmo0.3	⊢ 0 = ( 0g ‘ 𝑇 )
4		id	⊢ ( ( 𝑁 ‘ 𝐹 ) = 0 → ( 𝑁 ‘ 𝐹 ) = 0 )
5		0re	⊢ 0 ∈ ℝ
6	4 5	eqeltrdi	⊢ ( ( 𝑁 ‘ 𝐹 ) = 0 → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )
7	1	isnghm2	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) )
8	7	biimpar	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) → 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) )
9	6 8	sylan2	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) → 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) )
10		eqid	⊢ ( norm ‘ 𝑆 ) = ( norm ‘ 𝑆 )
11		eqid	⊢ ( norm ‘ 𝑇 ) = ( norm ‘ 𝑇 )
12	1 2 10 11	nmoi	⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
13	9 12	sylan	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
14		simplr	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐹 ) = 0 )
15	14	oveq1d	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) = ( 0 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
16		simpl1	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) → 𝑆 ∈ NrmGrp )
17	2 10	nmcl	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ )
18	16 17	sylan	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ )
19	18	recnd	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℂ )
20	19	mul02d	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( 0 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) = 0 )
21	15 20	eqtrd	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) = 0 )
22	13 21	breqtrd	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 0 )
23		simpll2	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → 𝑇 ∈ NrmGrp )
24		simpl3	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
25		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
26	2 25	ghmf	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
27	24 26	syl	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
28	27	ffvelcdmda	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) )
29	25 11	nmge0	⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ) → 0 ≤ ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
30	23 28 29	syl2anc	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → 0 ≤ ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
31	25 11	nmcl	⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
32	23 28 31	syl2anc	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
33		letri3	⊢ ( ( ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = 0 ↔ ( ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 0 ∧ 0 ≤ ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
34	32 5 33	sylancl	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = 0 ↔ ( ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 0 ∧ 0 ≤ ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
35	22 30 34	mpbir2and	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = 0 )
36	25 11 3	nmeq0	⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = 0 ↔ ( 𝐹 ‘ 𝑥 ) = 0 ) )
37	23 28 36	syl2anc	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = 0 ↔ ( 𝐹 ‘ 𝑥 ) = 0 ) )
38	35 37	mpbid	⊢ ( ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑥 ) = 0 )
39	38	mpteq2dva	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑉 ↦ 0 ) )
40	27	feqmptd	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) → 𝐹 = ( 𝑥 ∈ 𝑉 ↦ ( 𝐹 ‘ 𝑥 ) ) )
41		fconstmpt	⊢ ( 𝑉 × { 0 } ) = ( 𝑥 ∈ 𝑉 ↦ 0 )
42	41	a1i	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) → ( 𝑉 × { 0 } ) = ( 𝑥 ∈ 𝑉 ↦ 0 ) )
43	39 40 42	3eqtr4d	⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) = 0 ) → 𝐹 = ( 𝑉 × { 0 } ) )
44	43	ex	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( ( 𝑁 ‘ 𝐹 ) = 0 → 𝐹 = ( 𝑉 × { 0 } ) ) )
45	1 2 3	nmo0	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) = 0 )
46	45	3adant3	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) = 0 )
47		fveqeq2	⊢ ( 𝐹 = ( 𝑉 × { 0 } ) → ( ( 𝑁 ‘ 𝐹 ) = 0 ↔ ( 𝑁 ‘ ( 𝑉 × { 0 } ) ) = 0 ) )
48	46 47	syl5ibrcom	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 = ( 𝑉 × { 0 } ) → ( 𝑁 ‘ 𝐹 ) = 0 ) )
49	44 48	impbid	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( ( 𝑁 ‘ 𝐹 ) = 0 ↔ 𝐹 = ( 𝑉 × { 0 } ) ) )