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

Metamath Proof Explorer

Theorem nghmplusg

Description: The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Hypothesis nghmplusg.p 
|- .+ = ( +g ` T )
Assertion nghmplusg 
|- ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> ( F oF .+ G ) e. ( S NGHom T ) )

Proof

Step Hyp Ref Expression
1 nghmplusg.p 
 |-  .+ = ( +g ` T )
2 nghmrcl1 
 |-  ( F e. ( S NGHom T ) -> S e. NrmGrp )
3 2 3ad2ant2 
 |-  ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> S e. NrmGrp )
4 nghmrcl2 
 |-  ( F e. ( S NGHom T ) -> T e. NrmGrp )
5 4 3ad2ant2 
 |-  ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> T e. NrmGrp )
6 id 
 |-  ( T e. Abel -> T e. Abel )
7 nghmghm 
 |-  ( F e. ( S NGHom T ) -> F e. ( S GrpHom T ) )
8 nghmghm 
 |-  ( G e. ( S NGHom T ) -> G e. ( S GrpHom T ) )
9 1 ghmplusg 
 |-  ( ( T e. Abel /\ F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> ( F oF .+ G ) e. ( S GrpHom T ) )
10 6 7 8 9 syl3an 
 |-  ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> ( F oF .+ G ) e. ( S GrpHom T ) )
11 eqid 
 |-  ( S normOp T ) = ( S normOp T )
12 11 nghmcl 
 |-  ( F e. ( S NGHom T ) -> ( ( S normOp T ) ` F ) e. RR )
13 12 3ad2ant2 
 |-  ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> ( ( S normOp T ) ` F ) e. RR )
14 11 nghmcl 
 |-  ( G e. ( S NGHom T ) -> ( ( S normOp T ) ` G ) e. RR )
15 14 3ad2ant3 
 |-  ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> ( ( S normOp T ) ` G ) e. RR )
16 13 15 readdcld 
 |-  ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> ( ( ( S normOp T ) ` F ) + ( ( S normOp T ) ` G ) ) e. RR )
17 11 1 nmotri 
 |-  ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> ( ( S normOp T ) ` ( F oF .+ G ) ) <_ ( ( ( S normOp T ) ` F ) + ( ( S normOp T ) ` G ) ) )
18 11 bddnghm 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ ( F oF .+ G ) e. ( S GrpHom T ) ) /\ ( ( ( ( S normOp T ) ` F ) + ( ( S normOp T ) ` G ) ) e. RR /\ ( ( S normOp T ) ` ( F oF .+ G ) ) <_ ( ( ( S normOp T ) ` F ) + ( ( S normOp T ) ` G ) ) ) ) -> ( F oF .+ G ) e. ( S NGHom T ) )
19 3 5 10 16 17 18 syl32anc 
 |-  ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> ( F oF .+ G ) e. ( S NGHom T ) )