Metamath Proof Explorer

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 } ) ) )