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