4ipval2

Description: Four times the inner product value ipval3 , useful for simplifying certain proofs. (Contributed by NM, 10-Apr-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	4ipval2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to 4 (A P B) = {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})$

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	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}$
7	6	oveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to 4 (A P B) = 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})$
8		simp1	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to U \in NrmCVec$
9	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G B \in X$
10	1 4	nvcl	$⊢ (U \in NrmCVec \land A G B \in X) \to N (A G B) \in ℝ$
11	8 9 10	syl2anc	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G B) \in ℝ$
12	11	recnd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G B) \in ℂ$
13	12	sqcld	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G B)}^{2} \in ℂ$
14		neg1cn	$⊢ - 1 \in ℂ$
15	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land B \in X) \to -1 S B \in X$
16	14 15	mp3an2	$⊢ (U \in NrmCVec \land B \in X) \to -1 S B \in X$
17	16	3adant2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to -1 S B \in X$
18	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land -1 S B \in X) \to A G (-1 S B) \in X$
19	17 18	syld3an3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G (-1 S B) \in X$
20	1 4	nvcl	$⊢ (U \in NrmCVec \land A G (-1 S B) \in X) \to N (A G (-1 S B)) \in ℝ$
21	8 19 20	syl2anc	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G (-1 S B)) \in ℝ$
22	21	recnd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G (-1 S B)) \in ℂ$
23	22	sqcld	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G (-1 S B))}^{2} \in ℂ$
24	13 23	subcld	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G B)}^{2} - {N (A G (-1 S B))}^{2} \in ℂ$
25		ax-icn	$⊢ i \in ℂ$
26	1 3	nvscl	$⊢ (U \in NrmCVec \land i \in ℂ \land B \in X) \to i S B \in X$
27	25 26	mp3an2	$⊢ (U \in NrmCVec \land B \in X) \to i S B \in X$
28	27	3adant2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i S B \in X$
29	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land i S B \in X) \to A G (i S B) \in X$
30	28 29	syld3an3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G (i S B) \in X$
31	1 4	nvcl	$⊢ (U \in NrmCVec \land A G (i S B) \in X) \to N (A G (i S B)) \in ℝ$
32	8 30 31	syl2anc	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G (i S B)) \in ℝ$
33	32	recnd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G (i S B)) \in ℂ$
34	33	sqcld	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G (i S B))}^{2} \in ℂ$
35		negicn	$⊢ - i \in ℂ$
36	1 3	nvscl	$⊢ (U \in NrmCVec \land - i \in ℂ \land B \in X) \to (- i) S B \in X$
37	35 36	mp3an2	$⊢ (U \in NrmCVec \land B \in X) \to (- i) S B \in X$
38	37	3adant2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (- i) S B \in X$
39	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land (- i) S B \in X) \to A G ((- i) S B) \in X$
40	38 39	syld3an3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G ((- i) S B) \in X$
41	1 4	nvcl	$⊢ (U \in NrmCVec \land A G ((- i) S B) \in X) \to N (A G ((- i) S B)) \in ℝ$
42	8 40 41	syl2anc	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G ((- i) S B)) \in ℝ$
43	42	recnd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G ((- i) S B)) \in ℂ$
44	43	sqcld	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G ((- i) S B))}^{2} \in ℂ$
45	34 44	subcld	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2} \in ℂ$
46		mulcl	$⊢ (i \in ℂ \land {N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2} \in ℂ) \to i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2}) \in ℂ$
47	25 45 46	sylancr	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2}) \in ℂ$
48	24 47	addcld	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {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}) \in ℂ$
49		4cn	$⊢ 4 \in ℂ$
50		4ne0	$⊢ 4 \neq 0$
51		divcan2	$⊢ ({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}) \in ℂ \land 4 \in ℂ \land 4 \neq 0) \to 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}) = {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})$
52	49 50 51	mp3an23	$⊢ {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}) \in ℂ \to 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}) = {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})$
53	48 52	syl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to 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}) = {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})$
54	7 53	eqtrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to 4 (A P B) = {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})$

Metamath Proof Explorer

Theorem 4ipval2

Proof