Metamath Proof Explorer

Theorem ipval2lem3

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 ipval2lem3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A G 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 3 nvsid ⊢ U ∈ NrmCVec ∧ B ∈ X → 1 S B = B
7 6 oveq2d ⊢ U ∈ NrmCVec ∧ B ∈ X → A G 1 S B = A G B
8 7 fveq2d ⊢ U ∈ NrmCVec ∧ B ∈ X → N ⁡ A G 1 S B = N ⁡ A G B
9 8 oveq1d ⊢ U ∈ NrmCVec ∧ B ∈ X → N ⁡ A G 1 S B 2 = N ⁡ A G B 2
10 9 3adant2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A G 1 S B 2 = N ⁡ A G B 2
11 ax-1cn ⊢ 1 ∈ ℂ
12 1 2 3 4 5 ipval2lem2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ 1 ∈ ℂ → N ⁡ A G 1 S B 2 ∈ ℝ
13 11 12 mpan2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A G 1 S B 2 ∈ ℝ
14 10 13 eqeltrrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A G B 2 ∈ ℝ