Theorem normsub

Description: Swapping order of subtraction doesn't change the norm of a vector. (Contributed by NM, 14-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	normsub	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to {norm}_{ℎ}\left(A{-}_{ℎ}B\right)={norm}_{ℎ}\left(B{-}_{ℎ}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvoveq1	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {norm}_{ℎ}\left(A{-}_{ℎ}B\right)={norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}B\right)$$
2		oveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to B{-}_{ℎ}A=B{-}_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)$$
3	2	fveq2d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {norm}_{ℎ}\left(B{-}_{ℎ}A\right)={norm}_{ℎ}\left(B{-}_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
4	1 3	eqeq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left({norm}_{ℎ}\left(A{-}_{ℎ}B\right)={norm}_{ℎ}\left(B{-}_{ℎ}A\right)\leftrightarrow {norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}B\right)={norm}_{ℎ}\left(B{-}_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)$$
5		oveq2	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}B=if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}if\left(B\in \mathscr{H},B,0_{ℎ}\right)$$
6	5	fveq2d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to {norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}B\right)={norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)$$
7		fvoveq1	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to {norm}_{ℎ}\left(B{-}_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)={norm}_{ℎ}\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right){-}_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
8	6 7	eqeq12d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to \left({norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}B\right)={norm}_{ℎ}\left(B{-}_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\leftrightarrow {norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)={norm}_{ℎ}\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right){-}_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)$$
9		ifhvhv0	$$⊢if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \mathscr{H}$$
10		ifhvhv0	$$⊢if\left(B\in \mathscr{H},B,0_{ℎ}\right)\in \mathscr{H}$$
11	9 10	normsubi	$$⊢{norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)={norm}_{ℎ}\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right){-}_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
12	4 8 11	dedth2h	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to {norm}_{ℎ}\left(A{-}_{ℎ}B\right)={norm}_{ℎ}\left(B{-}_{ℎ}A\right)$$