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