This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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