Metamath Proof Explorer

Theorem cphnmvs

Description: Norm of a scalar product. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses cphnmvs.v ⊢ V = Base W
cphnmvs.n ⊢ N = norm ⁡ W
cphnmvs.s ⊢ · ˙ = ⋅ W
cphnmvs.f ⊢ F = Scalar ⁡ W
cphnmvs.k ⊢ K = Base F
Assertion cphnmvs ⊢ W ∈ CPreHil ∧ X ∈ K ∧ Y ∈ V → N ⁡ X · ˙ Y = X ⁢ N ⁡ Y

Proof

Step Hyp Ref Expression
1 cphnmvs.v ⊢ V = Base W
2 cphnmvs.n ⊢ N = norm ⁡ W
3 cphnmvs.s ⊢ · ˙ = ⋅ W
4 cphnmvs.f ⊢ F = Scalar ⁡ W
5 cphnmvs.k ⊢ K = Base F
6 cphnlm ⊢ W ∈ CPreHil → W ∈ NrmMod
7 eqid ⊢ norm ⁡ F = norm ⁡ F
8 1 2 3 4 5 7 nmvs ⊢ W ∈ NrmMod ∧ X ∈ K ∧ Y ∈ V → N ⁡ X · ˙ Y = norm ⁡ F ⁡ X ⁢ N ⁡ Y
9 6 8 syl3an1 ⊢ W ∈ CPreHil ∧ X ∈ K ∧ Y ∈ V → N ⁡ X · ˙ Y = norm ⁡ F ⁡ X ⁢ N ⁡ Y
10 cphclm ⊢ W ∈ CPreHil → W ∈ CMod
11 4 5 clmabs ⊢ W ∈ CMod ∧ X ∈ K → X = norm ⁡ F ⁡ X
12 10 11 sylan ⊢ W ∈ CPreHil ∧ X ∈ K → X = norm ⁡ F ⁡ X
13 12 3adant3 ⊢ W ∈ CPreHil ∧ X ∈ K ∧ Y ∈ V → X = norm ⁡ F ⁡ X
14 13 oveq1d ⊢ W ∈ CPreHil ∧ X ∈ K ∧ Y ∈ V → X ⁢ N ⁡ Y = norm ⁡ F ⁡ X ⁢ N ⁡ Y
15 9 14 eqtr4d ⊢ W ∈ CPreHil ∧ X ∈ K ∧ Y ∈ V → N ⁡ X · ˙ Y = X ⁢ N ⁡ Y