Metamath Proof Explorer

Theorem hvaddsubval

Description: Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hvaddsubval 
|- ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) = ( A -h ( -u 1 .h B ) ) )

Proof

Step Hyp Ref Expression
1 neg1cn 
 |-  -u 1 e. CC
2 hvmulcl 
 |-  ( ( -u 1 e. CC /\ B e. ~H ) -> ( -u 1 .h B ) e. ~H )
3 1 2 mpan 
 |-  ( B e. ~H -> ( -u 1 .h B ) e. ~H )
4 hvsubval 
 |-  ( ( A e. ~H /\ ( -u 1 .h B ) e. ~H ) -> ( A -h ( -u 1 .h B ) ) = ( A +h ( -u 1 .h ( -u 1 .h B ) ) ) )
5 3 4 sylan2 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A -h ( -u 1 .h B ) ) = ( A +h ( -u 1 .h ( -u 1 .h B ) ) ) )
6 hvm1neg 
 |-  ( ( -u 1 e. CC /\ B e. ~H ) -> ( -u 1 .h ( -u 1 .h B ) ) = ( -u -u 1 .h B ) )
7 1 6 mpan 
 |-  ( B e. ~H -> ( -u 1 .h ( -u 1 .h B ) ) = ( -u -u 1 .h B ) )
8 negneg1e1 
 |-  -u -u 1 = 1
9 8 oveq1i 
 |-  ( -u -u 1 .h B ) = ( 1 .h B )
10 7 9 eqtrdi 
 |-  ( B e. ~H -> ( -u 1 .h ( -u 1 .h B ) ) = ( 1 .h B ) )
11 ax-hvmulid 
 |-  ( B e. ~H -> ( 1 .h B ) = B )
12 10 11 eqtrd 
 |-  ( B e. ~H -> ( -u 1 .h ( -u 1 .h B ) ) = B )
13 12 adantl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( -u 1 .h ( -u 1 .h B ) ) = B )
14 13 oveq2d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A +h ( -u 1 .h ( -u 1 .h B ) ) ) = ( A +h B ) )
15 5 14 eqtr2d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) = ( A -h ( -u 1 .h B ) ) )