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 = \cdot_{𝑠OLD} (U)$
	dipfval.6	$⊢ N = {norm}_{CV} (U)$
	dipfval.7	$⊢ P = \cdot_{𝑖OLD} (U)$
Assertion	ipval2lem3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G 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 3	nvsid	$⊢ (U \in NrmCVec \land B \in X) \to 1 S B = B$
7	6	oveq2d	$⊢ (U \in NrmCVec \land B \in X) \to A G (1 S B) = A G B$
8	7	fveq2d	$⊢ (U \in NrmCVec \land B \in X) \to N (A G (1 S B)) = N (A G B)$
9	8	oveq1d	$⊢ (U \in NrmCVec \land B \in X) \to {N (A G (1 S B))}^{2} = {N (A G B)}^{2}$
10	9	3adant2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G (1 S B))}^{2} = {N (A G B)}^{2}$
11		ax-1cn	$⊢ 1 \in ℂ$
12	1 2 3 4 5	ipval2lem2	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land 1 \in ℂ) \to {N (A G (1 S B))}^{2} \in ℝ$
13	11 12	mpan2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G (1 S B))}^{2} \in ℝ$
14	10 13	eqeltrrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G B)}^{2} \in ℝ$

Metamath Proof Explorer