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 ⊢ V = Base S
0nmhm.2 ⊢ 0 ˙ = 0 T
0nmhm.f ⊢ F = Scalar ⁡ S
0nmhm.g ⊢ G = Scalar ⁡ T
Assertion 0nmhm ⊢ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F = G → V × 0 ˙ ∈ S NMHom T

Proof

Step Hyp Ref Expression
1 0nmhm.1 ⊢ V = Base S
2 0nmhm.2 ⊢ 0 ˙ = 0 T
3 0nmhm.f ⊢ F = Scalar ⁡ S
4 0nmhm.g ⊢ G = Scalar ⁡ T
5 nlmlmod ⊢ S ∈ NrmMod → S ∈ LMod
6 nlmlmod ⊢ T ∈ NrmMod → T ∈ LMod
7 id ⊢ F = G → F = G
8 2 1 3 4 0lmhm ⊢ S ∈ LMod ∧ T ∈ LMod ∧ F = G → V × 0 ˙ ∈ S LMHom T
9 5 6 7 8 syl3an ⊢ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F = G → V × 0 ˙ ∈ S LMHom T
10 nlmngp ⊢ S ∈ NrmMod → S ∈ NrmGrp
11 nlmngp ⊢ T ∈ NrmMod → T ∈ NrmGrp
12 1 2 0nghm ⊢ S ∈ NrmGrp ∧ T ∈ NrmGrp → V × 0 ˙ ∈ S NGHom T
13 10 11 12 syl2an ⊢ S ∈ NrmMod ∧ T ∈ NrmMod → V × 0 ˙ ∈ S NGHom T
14 13 3adant3 ⊢ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F = G → V × 0 ˙ ∈ S NGHom T
15 isnmhm ⊢ V × 0 ˙ ∈ S NMHom T ↔ S ∈ NrmMod ∧ T ∈ NrmMod ∧ V × 0 ˙ ∈ S LMHom T ∧ V × 0 ˙ ∈ S NGHom T
16 15 baib ⊢ S ∈ NrmMod ∧ T ∈ NrmMod → V × 0 ˙ ∈ S NMHom T ↔ V × 0 ˙ ∈ S LMHom T ∧ V × 0 ˙ ∈ S NGHom T
17 16 3adant3 ⊢ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F = G → V × 0 ˙ ∈ S NMHom T ↔ V × 0 ˙ ∈ S LMHom T ∧ V × 0 ˙ ∈ S NGHom T
18 9 14 17 mpbir2and ⊢ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F = G → V × 0 ˙ ∈ S NMHom T