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

Metamath Proof Explorer

Theorem honegsubi

Description: Relationship between Hilbert operator addition and subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hodseq.2 
|- S : ~H --> ~H
hodseq.3 
|- T : ~H --> ~H
Assertion honegsubi 
|- ( S +op ( -u 1 .op T ) ) = ( S -op T )

Proof

Step Hyp Ref Expression
1 hodseq.2 
 |-  S : ~H --> ~H
2 hodseq.3 
 |-  T : ~H --> ~H
3 neg1cn 
 |-  -u 1 e. CC
4 homulcl 
 |-  ( ( -u 1 e. CC /\ T : ~H --> ~H ) -> ( -u 1 .op T ) : ~H --> ~H )
5 3 2 4 mp2an 
 |-  ( -u 1 .op T ) : ~H --> ~H
6 hosval 
 |-  ( ( S : ~H --> ~H /\ ( -u 1 .op T ) : ~H --> ~H /\ x e. ~H ) -> ( ( S +op ( -u 1 .op T ) ) ` x ) = ( ( S ` x ) +h ( ( -u 1 .op T ) ` x ) ) )
7 1 5 6 mp3an12 
 |-  ( x e. ~H -> ( ( S +op ( -u 1 .op T ) ) ` x ) = ( ( S ` x ) +h ( ( -u 1 .op T ) ` x ) ) )
8 1 ffvelcdmi 
 |-  ( x e. ~H -> ( S ` x ) e. ~H )
9 2 ffvelcdmi 
 |-  ( x e. ~H -> ( T ` x ) e. ~H )
10 hvsubval 
 |-  ( ( ( S ` x ) e. ~H /\ ( T ` x ) e. ~H ) -> ( ( S ` x ) -h ( T ` x ) ) = ( ( S ` x ) +h ( -u 1 .h ( T ` x ) ) ) )
11 8 9 10 syl2anc 
 |-  ( x e. ~H -> ( ( S ` x ) -h ( T ` x ) ) = ( ( S ` x ) +h ( -u 1 .h ( T ` x ) ) ) )
12 homval 
 |-  ( ( -u 1 e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( -u 1 .op T ) ` x ) = ( -u 1 .h ( T ` x ) ) )
13 3 2 12 mp3an12 
 |-  ( x e. ~H -> ( ( -u 1 .op T ) ` x ) = ( -u 1 .h ( T ` x ) ) )
14 13 oveq2d 
 |-  ( x e. ~H -> ( ( S ` x ) +h ( ( -u 1 .op T ) ` x ) ) = ( ( S ` x ) +h ( -u 1 .h ( T ` x ) ) ) )
15 11 14 eqtr4d 
 |-  ( x e. ~H -> ( ( S ` x ) -h ( T ` x ) ) = ( ( S ` x ) +h ( ( -u 1 .op T ) ` x ) ) )
16 7 15 eqtr4d 
 |-  ( x e. ~H -> ( ( S +op ( -u 1 .op T ) ) ` x ) = ( ( S ` x ) -h ( T ` x ) ) )
17 hodval 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( S -op T ) ` x ) = ( ( S ` x ) -h ( T ` x ) ) )
18 1 2 17 mp3an12 
 |-  ( x e. ~H -> ( ( S -op T ) ` x ) = ( ( S ` x ) -h ( T ` x ) ) )
19 16 18 eqtr4d 
 |-  ( x e. ~H -> ( ( S +op ( -u 1 .op T ) ) ` x ) = ( ( S -op T ) ` x ) )
20 19 rgen 
 |-  A. x e. ~H ( ( S +op ( -u 1 .op T ) ) ` x ) = ( ( S -op T ) ` x )
21 1 5 hoaddcli 
 |-  ( S +op ( -u 1 .op T ) ) : ~H --> ~H
22 1 2 hosubcli 
 |-  ( S -op T ) : ~H --> ~H
23 21 22 hoeqi 
 |-  ( A. x e. ~H ( ( S +op ( -u 1 .op T ) ) ` x ) = ( ( S -op T ) ` x ) <-> ( S +op ( -u 1 .op T ) ) = ( S -op T ) )
24 20 23 mpbi 
 |-  ( S +op ( -u 1 .op T ) ) = ( S -op T )