Metamath Proof Explorer

Theorem ncvsdif

Description: The norm of the difference between two vectors. (Contributed by NM, 1-Dec-2006) (Revised by AV, 8-Oct-2021)

Ref Expression
Hypotheses ncvsprp.v 
|- V = ( Base ` W )
ncvsprp.n 
|- N = ( norm ` W )
ncvsprp.s 
|- .x. = ( .s ` W )
ncvsdif.p 
|- .+ = ( +g ` W )
Assertion ncvsdif 
|- ( ( W e. ( NrmVec i^i CVec ) /\ A e. V /\ B e. V ) -> ( N ` ( A .+ ( -u 1 .x. B ) ) ) = ( N ` ( B .+ ( -u 1 .x. A ) ) ) )

Proof

Step Hyp Ref Expression
1 ncvsprp.v 
 |-  V = ( Base ` W )
2 ncvsprp.n 
 |-  N = ( norm ` W )
3 ncvsprp.s 
 |-  .x. = ( .s ` W )
4 ncvsdif.p 
 |-  .+ = ( +g ` W )
5 elin 
 |-  ( W e. ( NrmVec i^i CVec ) <-> ( W e. NrmVec /\ W e. CVec ) )
6 id 
 |-  ( W e. CVec -> W e. CVec )
7 6 cvsclm 
 |-  ( W e. CVec -> W e. CMod )
8 5 7 simplbiim 
 |-  ( W e. ( NrmVec i^i CVec ) -> W e. CMod )
9 eqid 
 |-  ( -g ` W ) = ( -g ` W )
10 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
11 1 4 9 10 3 clmvsubval 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( A ( -g ` W ) B ) = ( A .+ ( -u 1 .x. B ) ) )
12 11 eqcomd 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( A .+ ( -u 1 .x. B ) ) = ( A ( -g ` W ) B ) )
13 8 12 syl3an1 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V /\ B e. V ) -> ( A .+ ( -u 1 .x. B ) ) = ( A ( -g ` W ) B ) )
14 13 fveq2d 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V /\ B e. V ) -> ( N ` ( A .+ ( -u 1 .x. B ) ) ) = ( N ` ( A ( -g ` W ) B ) ) )
15 nvcnlm 
 |-  ( W e. NrmVec -> W e. NrmMod )
16 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
17 15 16 syl 
 |-  ( W e. NrmVec -> W e. NrmGrp )
18 17 adantr 
 |-  ( ( W e. NrmVec /\ W e. CVec ) -> W e. NrmGrp )
19 5 18 sylbi 
 |-  ( W e. ( NrmVec i^i CVec ) -> W e. NrmGrp )
20 1 2 9 nmsub 
 |-  ( ( W e. NrmGrp /\ A e. V /\ B e. V ) -> ( N ` ( A ( -g ` W ) B ) ) = ( N ` ( B ( -g ` W ) A ) ) )
21 19 20 syl3an1 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V /\ B e. V ) -> ( N ` ( A ( -g ` W ) B ) ) = ( N ` ( B ( -g ` W ) A ) ) )
22 8 3ad2ant1 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V /\ B e. V ) -> W e. CMod )
23 simp3 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V /\ B e. V ) -> B e. V )
24 simp2 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V /\ B e. V ) -> A e. V )
25 1 4 9 10 3 clmvsubval 
 |-  ( ( W e. CMod /\ B e. V /\ A e. V ) -> ( B ( -g ` W ) A ) = ( B .+ ( -u 1 .x. A ) ) )
26 22 23 24 25 syl3anc 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V /\ B e. V ) -> ( B ( -g ` W ) A ) = ( B .+ ( -u 1 .x. A ) ) )
27 26 fveq2d 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V /\ B e. V ) -> ( N ` ( B ( -g ` W ) A ) ) = ( N ` ( B .+ ( -u 1 .x. A ) ) ) )
28 14 21 27 3eqtrd 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ A e. V /\ B e. V ) -> ( N ` ( A .+ ( -u 1 .x. B ) ) ) = ( N ` ( B .+ ( -u 1 .x. A ) ) ) )