ipval3

Description: Expansion of the inner product value ipval . (Contributed by NM, 17-Nov-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)$
	ipval3.3	$⊢ M = -_{v} (U)$
Assertion	ipval3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B = \frac{{N (A G B)}^{2} - {N (A M B)}^{2} + i ({N (A G (i S B))}^{2} - {N (A M (i S B))}^{2})}{4}$

Proof

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		ipval3.3	$⊢ M = -_{v} (U)$
7	1 2 3 4 5	ipval2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B = \frac{{N (A G B)}^{2} - {N (A G (-1 S B))}^{2} + i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2})}{4}$
8	1 2 3 6	nvmval	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A M B = A G (-1 S B)$
9	8	fveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A M B) = N (A G (-1 S B))$
10	9	oveq1d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A M B)}^{2} = {N (A G (-1 S B))}^{2}$
11	10	oveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G B)}^{2} - {N (A M B)}^{2} = {N (A G B)}^{2} - {N (A G (-1 S B))}^{2}$
12		ax-icn	$⊢ i \in ℂ$
13	1 3	nvscl	$⊢ (U \in NrmCVec \land i \in ℂ \land B \in X) \to i S B \in X$
14	12 13	mp3an2	$⊢ (U \in NrmCVec \land B \in X) \to i S B \in X$
15	14	3adant2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i S B \in X$
16	1 2 3 6	nvmval	$⊢ (U \in NrmCVec \land A \in X \land i S B \in X) \to A M (i S B) = A G (-1 S (i S B))$
17	15 16	syld3an3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A M (i S B) = A G (-1 S (i S B))$
18		neg1cn	$⊢ - 1 \in ℂ$
19	1 3	nvsass	$⊢ (U \in NrmCVec \land (- 1 \in ℂ \land i \in ℂ \land B \in X)) \to -1 i S B = -1 S (i S B)$
20	18 19	mp3anr1	$⊢ (U \in NrmCVec \land (i \in ℂ \land B \in X)) \to -1 i S B = -1 S (i S B)$
21	12 20	mpanr1	$⊢ (U \in NrmCVec \land B \in X) \to -1 i S B = -1 S (i S B)$
22	12	mulm1i	$⊢ -1 i = - i$
23	22	oveq1i	$⊢ -1 i S B = (- i) S B$
24	21 23	eqtr3di	$⊢ (U \in NrmCVec \land B \in X) \to -1 S (i S B) = (- i) S B$
25	24	3adant2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to -1 S (i S B) = (- i) S B$
26	25	oveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G (-1 S (i S B)) = A G ((- i) S B)$
27	17 26	eqtrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A M (i S B) = A G ((- i) S B)$
28	27	fveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A M (i S B)) = N (A G ((- i) S B))$
29	28	oveq1d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A M (i S B))}^{2} = {N (A G ((- i) S B))}^{2}$
30	29	oveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G (i S B))}^{2} - {N (A M (i S B))}^{2} = {N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2}$
31	30	oveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i ({N (A G (i S B))}^{2} - {N (A M (i S B))}^{2}) = i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2})$
32	11 31	oveq12d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G B)}^{2} - {N (A M B)}^{2} + i ({N (A G (i S B))}^{2} - {N (A M (i S B))}^{2}) = {N (A G B)}^{2} - {N (A G (-1 S B))}^{2} + i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2})$
33	32	oveq1d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to \frac{{N (A G B)}^{2} - {N (A M B)}^{2} + i ({N (A G (i S B))}^{2} - {N (A M (i S B))}^{2})}{4} = \frac{{N (A G B)}^{2} - {N (A G (-1 S B))}^{2} + i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2})}{4}$
34	7 33	eqtr4d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B = \frac{{N (A G B)}^{2} - {N (A M B)}^{2} + i ({N (A G (i S B))}^{2} - {N (A M (i S B))}^{2})}{4}$

Metamath Proof Explorer

Theorem ipval3

Proof