Metamath Proof Explorer

Theorem ipval2lem2

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 ipval2lem2 ⊢ 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 simpl1 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℂ → U ∈ NrmCVec
7 simpl2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℂ → A ∈ X
8 1 3 nvscl ⊢ U ∈ NrmCVec ∧ C ∈ ℂ ∧ B ∈ X → C S B ∈ X
9 8 3com23 ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ C ∈ ℂ → C S B ∈ X
10 9 3expa ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ C ∈ ℂ → C S B ∈ X
11 10 3adantl2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℂ → C S B ∈ X
12 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ C S B ∈ X → A G C S B ∈ X
13 6 7 11 12 syl3anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℂ → A G C S B ∈ X
14 1 4 nvcl ⊢ U ∈ NrmCVec ∧ A G C S B ∈ X → N ⁡ A G C S B ∈ ℝ
15 6 13 14 syl2anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℂ → N ⁡ A G C S B ∈ ℝ
16 15 resqcld ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℂ → N ⁡ A G C S B 2 ∈ ℝ