Metamath Proof Explorer

Theorem ncvsprp

Description: Proportionality property of the norm of a scalar product in a normed subcomplex vector space. (Contributed by NM, 11-Nov-2006) (Revised by AV, 8-Oct-2021)

Ref Expression
Hypotheses ncvsprp.v ⊢ V = Base W
ncvsprp.n ⊢ N = norm ⁡ W
ncvsprp.s ⊢ · ˙ = ⋅ W
ncvsprp.f ⊢ F = Scalar ⁡ W
ncvsprp.k ⊢ K = Base F
Assertion ncvsprp ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ K ∧ B ∈ V → N ⁡ A · ˙ B = A ⁢ N ⁡ B

Proof

Step Hyp Ref Expression
1 ncvsprp.v ⊢ V = Base W
2 ncvsprp.n ⊢ N = norm ⁡ W
3 ncvsprp.s ⊢ · ˙ = ⋅ W
4 ncvsprp.f ⊢ F = Scalar ⁡ W
5 ncvsprp.k ⊢ K = Base F
6 elin ⊢ W ∈ NrmVec ∩ ℂVec ↔ W ∈ NrmVec ∧ W ∈ ℂVec
7 nvcnlm ⊢ W ∈ NrmVec → W ∈ NrmMod
8 7 adantr ⊢ W ∈ NrmVec ∧ W ∈ ℂVec → W ∈ NrmMod
9 6 8 sylbi ⊢ W ∈ NrmVec ∩ ℂVec → W ∈ NrmMod
10 eqid ⊢ norm ⁡ F = norm ⁡ F
11 1 2 3 4 5 10 nmvs ⊢ W ∈ NrmMod ∧ A ∈ K ∧ B ∈ V → N ⁡ A · ˙ B = norm ⁡ F ⁡ A ⁢ N ⁡ B
12 9 11 syl3an1 ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ K ∧ B ∈ V → N ⁡ A · ˙ B = norm ⁡ F ⁡ A ⁢ N ⁡ B
13 id ⊢ W ∈ ℂVec → W ∈ ℂVec
14 13 cvsclm ⊢ W ∈ ℂVec → W ∈ CMod
15 6 14 simplbiim ⊢ W ∈ NrmVec ∩ ℂVec → W ∈ CMod
16 4 5 clmabs ⊢ W ∈ CMod ∧ A ∈ K → A = norm ⁡ F ⁡ A
17 15 16 sylan ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ K → A = norm ⁡ F ⁡ A
18 17 3adant3 ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ K ∧ B ∈ V → A = norm ⁡ F ⁡ A
19 18 eqcomd ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ K ∧ B ∈ V → norm ⁡ F ⁡ A = A
20 19 oveq1d ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ K ∧ B ∈ V → norm ⁡ F ⁡ A ⁢ N ⁡ B = A ⁢ N ⁡ B
21 12 20 eqtrd ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ K ∧ B ∈ V → N ⁡ A · ˙ B = A ⁢ N ⁡ B