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. = ( 0g ` T )
0nmhm.f 
|- F = ( Scalar ` S )
0nmhm.g 
|- G = ( Scalar ` T )
Assertion 0nmhm 
|- ( ( S e. NrmMod /\ T e. NrmMod /\ F = G ) -> ( V X. { .0. } ) e. ( S NMHom T ) )

Proof

Step Hyp Ref Expression
1 0nmhm.1 
 |-  V = ( Base ` S )
2 0nmhm.2 
 |-  .0. = ( 0g ` T )
3 0nmhm.f 
 |-  F = ( Scalar ` S )
4 0nmhm.g 
 |-  G = ( Scalar ` T )
5 nlmlmod 
 |-  ( S e. NrmMod -> S e. LMod )
6 nlmlmod 
 |-  ( T e. NrmMod -> T e. LMod )
7 id 
 |-  ( F = G -> F = G )
8 2 1 3 4 0lmhm 
 |-  ( ( S e. LMod /\ T e. LMod /\ F = G ) -> ( V X. { .0. } ) e. ( S LMHom T ) )
9 5 6 7 8 syl3an 
 |-  ( ( S e. NrmMod /\ T e. NrmMod /\ F = G ) -> ( V X. { .0. } ) e. ( S LMHom T ) )
10 nlmngp 
 |-  ( S e. NrmMod -> S e. NrmGrp )
11 nlmngp 
 |-  ( T e. NrmMod -> T e. NrmGrp )
12 1 2 0nghm 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( V X. { .0. } ) e. ( S NGHom T ) )
13 10 11 12 syl2an 
 |-  ( ( S e. NrmMod /\ T e. NrmMod ) -> ( V X. { .0. } ) e. ( S NGHom T ) )
14 13 3adant3 
 |-  ( ( S e. NrmMod /\ T e. NrmMod /\ F = G ) -> ( V X. { .0. } ) e. ( S NGHom T ) )
15 isnmhm 
 |-  ( ( V X. { .0. } ) e. ( S NMHom T ) <-> ( ( S e. NrmMod /\ T e. NrmMod ) /\ ( ( V X. { .0. } ) e. ( S LMHom T ) /\ ( V X. { .0. } ) e. ( S NGHom T ) ) ) )
16 15 baib 
 |-  ( ( S e. NrmMod /\ T e. NrmMod ) -> ( ( V X. { .0. } ) e. ( S NMHom T ) <-> ( ( V X. { .0. } ) e. ( S LMHom T ) /\ ( V X. { .0. } ) e. ( S NGHom T ) ) ) )
17 16 3adant3 
 |-  ( ( S e. NrmMod /\ T e. NrmMod /\ F = G ) -> ( ( V X. { .0. } ) e. ( S NMHom T ) <-> ( ( V X. { .0. } ) e. ( S LMHom T ) /\ ( V X. { .0. } ) e. ( S NGHom T ) ) ) )
18 9 14 17 mpbir2and 
 |-  ( ( S e. NrmMod /\ T e. NrmMod /\ F = G ) -> ( V X. { .0. } ) e. ( S NMHom T ) )