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 𝑉 = ( Base ‘ 𝑆 )
0nmhm.2 0 = ( 0g𝑇 )
0nmhm.f 𝐹 = ( Scalar ‘ 𝑆 )
0nmhm.g 𝐺 = ( Scalar ‘ 𝑇 )
Assertion 0nmhm ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺 ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 NMHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 0nmhm.1 𝑉 = ( Base ‘ 𝑆 )
2 0nmhm.2 0 = ( 0g𝑇 )
3 0nmhm.f 𝐹 = ( Scalar ‘ 𝑆 )
4 0nmhm.g 𝐺 = ( Scalar ‘ 𝑇 )
5 nlmlmod ( 𝑆 ∈ NrmMod → 𝑆 ∈ LMod )
6 nlmlmod ( 𝑇 ∈ NrmMod → 𝑇 ∈ LMod )
7 id ( 𝐹 = 𝐺𝐹 = 𝐺 )
8 2 1 3 4 0lmhm ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ∧ 𝐹 = 𝐺 ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 LMHom 𝑇 ) )
9 5 6 7 8 syl3an ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺 ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 LMHom 𝑇 ) )
10 nlmngp ( 𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp )
11 nlmngp ( 𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp )
12 1 2 0nghm ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) )
13 10 11 12 syl2an ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) )
14 13 3adant3 ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺 ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) )
15 isnmhm ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 NMHom 𝑇 ) ↔ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) ∧ ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) ) ) )
16 15 baib ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) → ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 NMHom 𝑇 ) ↔ ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) ) ) )
17 16 3adant3 ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺 ) → ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 NMHom 𝑇 ) ↔ ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) ) ) )
18 9 14 17 mpbir2and ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺 ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 NMHom 𝑇 ) )