This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nvs

Description: Proportionality property of the norm of a scalar product in a normed complex vector space. (Contributed by NM, 11-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvs.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvs.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
nvs.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion nvs ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nvs.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvs.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
3 nvs.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
4 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
5 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
6 1 4 2 5 3 nvi ⊢ ( 𝑈 ∈ NrmCVec → ( ⟨ ( +𝑣 ‘ 𝑈 ) , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( 0vec ‘ 𝑈 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
7 6 simp3d ⊢ ( 𝑈 ∈ NrmCVec → ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( 0vec ‘ 𝑈 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
8 simp2 ⊢ ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( 0vec ‘ 𝑈 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) )
9 8 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( 0vec ‘ 𝑈 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) )
10 7 9 syl ⊢ ( 𝑈 ∈ NrmCVec → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) )
11 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑦 𝑆 𝑥 ) = ( 𝑦 𝑆 𝐵 ) )
12 11 fveq2d ⊢ ( 𝑥 = 𝐵 → ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( 𝑁 ‘ ( 𝑦 𝑆 𝐵 ) ) )
13 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝐵 ) )
14 13 oveq2d ⊢ ( 𝑥 = 𝐵 → ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝐵 ) ) )
15 12 14 eqeq12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ↔ ( 𝑁 ‘ ( 𝑦 𝑆 𝐵 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝐵 ) ) ) )
16 fvoveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑁 ‘ ( 𝑦 𝑆 𝐵 ) ) = ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) )
17 fveq2 ⊢ ( 𝑦 = 𝐴 → ( abs ‘ 𝑦 ) = ( abs ‘ 𝐴 ) )
18 17 oveq1d ⊢ ( 𝑦 = 𝐴 → ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
19 16 18 eqeq12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑁 ‘ ( 𝑦 𝑆 𝐵 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝐵 ) ) ↔ ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ) )
20 15 19 rspc2v ⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ ℂ ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ) )
21 10 20 syl5 ⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ ℂ ) → ( 𝑈 ∈ NrmCVec → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ) )
22 21 3impia ⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ ℂ ∧ 𝑈 ∈ NrmCVec ) → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
23 22 3com13 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )