Metamath Proof Explorer

Theorem ncvsm1

Description: The norm of the opposite of a vector. (Contributed by NM, 28-Nov-2006) (Revised by AV, 8-Oct-2021)

Ref Expression
Hypotheses ncvsprp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ncvsprp.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
ncvsprp.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion ncvsm1 ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ ( - 1 · 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ncvsprp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ncvsprp.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
3 ncvsprp.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 simpl ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ) → 𝑊 ∈ ( NrmVec ∩ ℂVec ) )
5 elin ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec ) )
6 id ⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂVec )
7 6 cvsclm ⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂMod )
8 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
9 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
10 8 9 clmneg1 ⊢ ( 𝑊 ∈ ℂMod → - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
11 7 10 syl ⊢ ( 𝑊 ∈ ℂVec → - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
12 5 11 simplbiim ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
13 12 adantr ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ) → - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
14 simpr ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
15 1 2 3 8 9 ncvsprp ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ ( - 1 · 𝐴 ) ) = ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐴 ) ) )
16 4 13 14 15 syl3anc ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ ( - 1 · 𝐴 ) ) = ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐴 ) ) )
17 ax-1cn ⊢ 1 ∈ ℂ
18 17 absnegi ⊢ ( abs ‘ - 1 ) = ( abs ‘ 1 )
19 abs1 ⊢ ( abs ‘ 1 ) = 1
20 18 19 eqtri ⊢ ( abs ‘ - 1 ) = 1
21 20 oveq1i ⊢ ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐴 ) ) = ( 1 · ( 𝑁 ‘ 𝐴 ) )
22 nvcnlm ⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod )
23 nlmngp ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
24 22 23 syl ⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ NrmGrp )
25 24 adantr ⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec ) → 𝑊 ∈ NrmGrp )
26 5 25 sylbi ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → 𝑊 ∈ NrmGrp )
27 1 2 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
28 26 27 sylan ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
29 28 recnd ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℂ )
30 29 mulid2d ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ) → ( 1 · ( 𝑁 ‘ 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )
31 21 30 syl5eq ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ) → ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )
32 16 31 eqtrd ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ ( - 1 · 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )