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 )
4 hoadddi 
 |-  ( ( 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 ) ) )
8 7 3adant2 
 |-  ( ( 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 ) ) )
13 12 3adant1 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T +op ( -u 1 .op U ) ) ) = ( A .op ( T -op U ) ) )
14 homulcl 
 |-  ( ( A e. CC /\ T : ~H --> ~H ) -> ( A .op T ) : ~H --> ~H )
15 homulcl 
 |-  ( ( A e. CC /\ U : ~H --> ~H ) -> ( A .op U ) : ~H --> ~H )
16 honegsub 
 |-  ( ( ( 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 ) ) )
17 14 15 16 syl2an 
 |-  ( ( ( 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 ) ) )
18 17 3impdi 
 |-  ( ( 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 ) ) )
19 10 13 18 3eqtr3d 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T -op U ) ) = ( ( A .op T ) -op ( A .op U ) ) )