Theorem normsubi

Description: Negative doesn't change the norm of a Hilbert space vector. (Contributed by NM, 11-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	normsub.1	|- A e. ~H
	normsub.2	|- B e. ~H
Assertion	normsubi	|- ( normh ` ( A -h B ) ) = ( normh ` ( B -h A ) )

Proof

Step	Hyp	Ref	Expression
1		normsub.1	|- A e. ~H
2		normsub.2	|- B e. ~H
3		neg1cn	|- -u 1 e. CC
4	2 1	hvsubcli	|- ( B -h A ) e. ~H
5	3 4	norm-iii-i	|- ( normh ` ( -u 1 .h ( B -h A ) ) ) = ( ( abs ` -u 1 ) x. ( normh ` ( B -h A ) ) )
6	2 1	hvnegdii	|- ( -u 1 .h ( B -h A ) ) = ( A -h B )
7	6	fveq2i	|- ( normh ` ( -u 1 .h ( B -h A ) ) ) = ( normh ` ( A -h B ) )
8		ax-1cn	|- 1 e. CC
9	8	absnegi	|- ( abs ` -u 1 ) = ( abs ` 1 )
10		abs1	|- ( abs ` 1 ) = 1
11	9 10	eqtri	|- ( abs ` -u 1 ) = 1
12	11	oveq1i	|- ( ( abs ` -u 1 ) x. ( normh ` ( B -h A ) ) ) = ( 1 x. ( normh ` ( B -h A ) ) )
13	4	normcli	|- ( normh ` ( B -h A ) ) e. RR
14	13	recni	|- ( normh ` ( B -h A ) ) e. CC
15	14	mullidi	|- ( 1 x. ( normh ` ( B -h A ) ) ) = ( normh ` ( B -h A ) )
16	12 15	eqtri	|- ( ( abs ` -u 1 ) x. ( normh ` ( B -h A ) ) ) = ( normh ` ( B -h A ) )
17	5 7 16	3eqtr3i	|- ( normh ` ( A -h B ) ) = ( normh ` ( B -h A ) )