# Metamath Proof Explorer

## Theorem hosubdi

Description: Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hosubdi
`|- ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T -op U ) ) = ( ( A .op T ) -op ( A .op U ) ) )`

### Proof

Step Hyp Ref Expression
1 neg1cn
` |-  -u 1 e. CC`
2 homulcl
` |-  ( ( -u 1 e. CC /\ U : ~H --> ~H ) -> ( -u 1 .op U ) : ~H --> ~H )`
3 1 2 mpan
` |-  ( U : ~H --> ~H -> ( -u 1 .op U ) : ~H --> ~H )`
` |-  ( ( A e. CC /\ T : ~H --> ~H /\ ( -u 1 .op U ) : ~H --> ~H ) -> ( A .op ( T +op ( -u 1 .op U ) ) ) = ( ( A .op T ) +op ( A .op ( -u 1 .op U ) ) ) )`
5 3 4 syl3an3
` |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T +op ( -u 1 .op U ) ) ) = ( ( A .op T ) +op ( A .op ( -u 1 .op U ) ) ) )`
6 homul12
` |-  ( ( A e. CC /\ -u 1 e. CC /\ U : ~H --> ~H ) -> ( A .op ( -u 1 .op U ) ) = ( -u 1 .op ( A .op U ) ) )`
7 1 6 mp3an2
` |-  ( ( A e. CC /\ U : ~H --> ~H ) -> ( A .op ( -u 1 .op U ) ) = ( -u 1 .op ( A .op U ) ) )`
` |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( -u 1 .op U ) ) = ( -u 1 .op ( A .op U ) ) )`
9 8 oveq2d
` |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( A .op T ) +op ( A .op ( -u 1 .op U ) ) ) = ( ( A .op T ) +op ( -u 1 .op ( A .op U ) ) ) )`
10 5 9 eqtrd
` |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T +op ( -u 1 .op U ) ) ) = ( ( A .op T ) +op ( -u 1 .op ( A .op U ) ) ) )`
11 honegsub
` |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( -u 1 .op U ) ) = ( T -op U ) )`
12 11 oveq2d
` |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T +op ( -u 1 .op U ) ) ) = ( A .op ( T -op U ) ) )`
` |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T +op ( -u 1 .op U ) ) ) = ( A .op ( T -op U ) ) )`
` |-  ( ( A e. CC /\ T : ~H --> ~H ) -> ( A .op T ) : ~H --> ~H )`
` |-  ( ( A e. CC /\ U : ~H --> ~H ) -> ( A .op U ) : ~H --> ~H )`
` |-  ( ( ( A .op T ) : ~H --> ~H /\ ( A .op U ) : ~H --> ~H ) -> ( ( A .op T ) +op ( -u 1 .op ( A .op U ) ) ) = ( ( A .op T ) -op ( A .op U ) ) )`
` |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( A e. CC /\ U : ~H --> ~H ) ) -> ( ( A .op T ) +op ( -u 1 .op ( A .op U ) ) ) = ( ( A .op T ) -op ( A .op U ) ) )`
` |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( A .op T ) +op ( -u 1 .op ( A .op U ) ) ) = ( ( A .op T ) -op ( A .op U ) ) )`
` |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T -op U ) ) = ( ( A .op T ) -op ( A .op U ) ) )`