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 ) ) )