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 = \cdot_{𝑠OLD} (U)$
	dipfval.6	$⊢ N = {norm}_{CV} (U)$
	dipfval.7	$⊢ P = \cdot_{𝑖OLD} (U)$
Assertion	ipval2lem2	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land C \in ℂ) \to {N (A G (C S B))}^{2} \in ℝ$

Step	Hyp	Ref	Expression
1		dipfval.1	$⊢ X = BaseSet (U)$
2		dipfval.2	$⊢ G = +_{v} (U)$
3		dipfval.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		dipfval.6	$⊢ N = {norm}_{CV} (U)$
5		dipfval.7	$⊢ P = \cdot_{𝑖OLD} (U)$
6		simpl1	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land C \in ℂ) \to U \in NrmCVec$
7		simpl2	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land C \in ℂ) \to A \in X$
8	1 3	nvscl	$⊢ (U \in NrmCVec \land C \in ℂ \land B \in X) \to C S B \in X$
9	8	3com23	$⊢ (U \in NrmCVec \land B \in X \land C \in ℂ) \to C S B \in X$
10	9	3expa	$⊢ ((U \in NrmCVec \land B \in X) \land C \in ℂ) \to C S B \in X$
11	10	3adantl2	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land C \in ℂ) \to C S B \in X$
12	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land C S B \in X) \to A G (C S B) \in X$
13	6 7 11 12	syl3anc	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land C \in ℂ) \to A G (C S B) \in X$
14	1 4	nvcl	$⊢ (U \in NrmCVec \land A G (C S B) \in X) \to N (A G (C S B)) \in ℝ$
15	6 13 14	syl2anc	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land C \in ℂ) \to N (A G (C S B)) \in ℝ$
16	15	resqcld	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land C \in ℂ) \to {N (A G (C S B))}^{2} \in ℝ$

Metamath Proof Explorer