This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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