Metamath Proof Explorer


Theorem hisubcomi

Description: Two vector subtractions simultaneously commute in an inner product. (Contributed by NM, 1-Jul-2005) (New usage is discouraged.)

Ref Expression
Hypotheses hisubcom.1
|- A e. ~H
hisubcom.2
|- B e. ~H
hisubcom.3
|- C e. ~H
hisubcom.4
|- D e. ~H
Assertion hisubcomi
|- ( ( A -h B ) .ih ( C -h D ) ) = ( ( B -h A ) .ih ( D -h C ) )

Proof

Step Hyp Ref Expression
1 hisubcom.1
 |-  A e. ~H
2 hisubcom.2
 |-  B e. ~H
3 hisubcom.3
 |-  C e. ~H
4 hisubcom.4
 |-  D e. ~H
5 2 1 hvnegdii
 |-  ( -u 1 .h ( B -h A ) ) = ( A -h B )
6 4 3 hvnegdii
 |-  ( -u 1 .h ( D -h C ) ) = ( C -h D )
7 5 6 oveq12i
 |-  ( ( -u 1 .h ( B -h A ) ) .ih ( -u 1 .h ( D -h C ) ) ) = ( ( A -h B ) .ih ( C -h D ) )
8 neg1cn
 |-  -u 1 e. CC
9 2 1 hvsubcli
 |-  ( B -h A ) e. ~H
10 4 3 hvsubcli
 |-  ( D -h C ) e. ~H
11 8 8 9 10 his35i
 |-  ( ( -u 1 .h ( B -h A ) ) .ih ( -u 1 .h ( D -h C ) ) ) = ( ( -u 1 x. ( * ` -u 1 ) ) x. ( ( B -h A ) .ih ( D -h C ) ) )
12 neg1rr
 |-  -u 1 e. RR
13 cjre
 |-  ( -u 1 e. RR -> ( * ` -u 1 ) = -u 1 )
14 12 13 ax-mp
 |-  ( * ` -u 1 ) = -u 1
15 14 oveq2i
 |-  ( -u 1 x. ( * ` -u 1 ) ) = ( -u 1 x. -u 1 )
16 ax-1cn
 |-  1 e. CC
17 16 16 mul2negi
 |-  ( -u 1 x. -u 1 ) = ( 1 x. 1 )
18 1t1e1
 |-  ( 1 x. 1 ) = 1
19 15 17 18 3eqtri
 |-  ( -u 1 x. ( * ` -u 1 ) ) = 1
20 19 oveq1i
 |-  ( ( -u 1 x. ( * ` -u 1 ) ) x. ( ( B -h A ) .ih ( D -h C ) ) ) = ( 1 x. ( ( B -h A ) .ih ( D -h C ) ) )
21 9 10 hicli
 |-  ( ( B -h A ) .ih ( D -h C ) ) e. CC
22 21 mulid2i
 |-  ( 1 x. ( ( B -h A ) .ih ( D -h C ) ) ) = ( ( B -h A ) .ih ( D -h C ) )
23 11 20 22 3eqtri
 |-  ( ( -u 1 .h ( B -h A ) ) .ih ( -u 1 .h ( D -h C ) ) ) = ( ( B -h A ) .ih ( D -h C ) )
24 7 23 eqtr3i
 |-  ( ( A -h B ) .ih ( C -h D ) ) = ( ( B -h A ) .ih ( D -h C ) )