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