Metamath Proof Explorer

Theorem ipval2lem4

Description: Lemma for ipval3 . (Contributed by NM, 1-Feb-2007) (New usage is discouraged.)

Ref Expression
Hypotheses dipfval.1 ⊢ X = BaseSet ⁡ U
dipfval.2 ⊢ G = + v ⁡ U
dipfval.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
dipfval.6 ⊢ N = norm CV ⁡ U
dipfval.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
Assertion ipval2lem4 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℂ → N ⁡ A G C S B 2 ∈ ℂ

Proof

Step Hyp Ref Expression
1 dipfval.1 ⊢ X = BaseSet ⁡ U
2 dipfval.2 ⊢ G = + v ⁡ U
3 dipfval.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 dipfval.6 ⊢ N = norm CV ⁡ U
5 dipfval.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
6 1 2 3 4 5 ipval2lem2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℂ → N ⁡ A G C S B 2 ∈ ℝ
7 6 recnd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℂ → N ⁡ A G C S B 2 ∈ ℂ