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\in \mathscr{H}$$
	normsub.2	$$⊢B\in \mathscr{H}$$
Assertion	normsubi	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}B\right)={norm}_{ℎ}\left(B{-}_{ℎ}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		normsub.1	$$⊢A\in \mathscr{H}$$
2		normsub.2	$$⊢B\in \mathscr{H}$$
3		neg1cn	$$⊢-1\in ℂ$$
4	2 1	hvsubcli	$$⊢B{-}_{ℎ}A\in \mathscr{H}$$
5	3 4	norm-iii-i	$$⊢{norm}_{ℎ}\left(-1{\cdot }_{ℎ}\left(B{-}_{ℎ}A\right)\right)=\left|-1\right|{norm}_{ℎ}\left(B{-}_{ℎ}A\right)$$
6	2 1	hvnegdii	$$⊢-1{\cdot }_{ℎ}\left(B{-}_{ℎ}A\right)=A{-}_{ℎ}B$$
7	6	fveq2i	$$⊢{norm}_{ℎ}\left(-1{\cdot }_{ℎ}\left(B{-}_{ℎ}A\right)\right)={norm}_{ℎ}\left(A{-}_{ℎ}B\right)$$
8		ax-1cn	$$⊢1\in ℂ$$
9	8	absnegi	$$⊢\left|-1\right|=\left|1\right|$$
10		abs1	$$⊢\left|1\right|=1$$
11	9 10	eqtri	$$⊢\left|-1\right|=1$$
12	11	oveq1i	$$⊢\left|-1\right|{norm}_{ℎ}\left(B{-}_{ℎ}A\right)=1{norm}_{ℎ}\left(B{-}_{ℎ}A\right)$$
13	4	normcli	$$⊢{norm}_{ℎ}\left(B{-}_{ℎ}A\right)\in ℝ$$
14	13	recni	$$⊢{norm}_{ℎ}\left(B{-}_{ℎ}A\right)\in ℂ$$
15	14	mullidi	$$⊢1{norm}_{ℎ}\left(B{-}_{ℎ}A\right)={norm}_{ℎ}\left(B{-}_{ℎ}A\right)$$
16	12 15	eqtri	$$⊢\left|-1\right|{norm}_{ℎ}\left(B{-}_{ℎ}A\right)={norm}_{ℎ}\left(B{-}_{ℎ}A\right)$$
17	5 7 16	3eqtr3i	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}B\right)={norm}_{ℎ}\left(B{-}_{ℎ}A\right)$$