# 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 ffvelrni
` |-  ( x e. ~H -> ( S ` x ) e. ~H )`
9 2 ffvelrni
` |-  ( 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 )`
` |-  ( S +op ( -u 1 .op T ) ) : ~H --> ~H`
` |-  ( S -op T ) : ~H --> ~H`
` |-  ( A. x e. ~H ( ( S +op ( -u 1 .op T ) ) ` x ) = ( ( S -op T ) ` x ) <-> ( S +op ( -u 1 .op T ) ) = ( S -op T ) )`
` |-  ( S +op ( -u 1 .op T ) ) = ( S -op T )`