Metamath Proof Explorer


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 ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( norm ‘ ( 𝐴 𝐵 ) ) = ( norm ‘ ( 𝐵 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 fvoveq1 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( norm ‘ ( 𝐴 𝐵 ) ) = ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) ) )
2 oveq2 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( 𝐵 𝐴 ) = ( 𝐵 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
3 2 fveq2d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( norm ‘ ( 𝐵 𝐴 ) ) = ( norm ‘ ( 𝐵 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) )
4 1 3 eqeq12d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( norm ‘ ( 𝐴 𝐵 ) ) = ( norm ‘ ( 𝐵 𝐴 ) ) ↔ ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) ) = ( norm ‘ ( 𝐵 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ) )
5 oveq2 ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) )
6 5 fveq2d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) ) = ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) )
7 fvoveq1 ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( norm ‘ ( 𝐵 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) = ( norm ‘ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) − if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) )
8 6 7 eqeq12d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) ) = ( norm ‘ ( 𝐵 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ↔ ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) = ( norm ‘ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) − if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ) )
9 ifhvhv0 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ∈ ℋ
10 ifhvhv0 if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ∈ ℋ
11 9 10 normsubi ( norm ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) = ( norm ‘ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) − if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
12 4 8 11 dedth2h ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( norm ‘ ( 𝐴 𝐵 ) ) = ( norm ‘ ( 𝐵 𝐴 ) ) )