ipval2

Description: Expansion of the inner product value ipval . (Contributed by NM, 31-Jan-2007) (Revised by Mario Carneiro, 5-May-2014) (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	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}$

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	ipval	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B = \frac{\sum_{k = 1}^{4} i^{k} {N (A G (i^{k} S B))}^{2}}{4}$
7		ax-icn	$⊢ i \in ℂ$
8	1 2 3 4 5	ipval2lem4	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land i \in ℂ) \to {N (A G (i S B))}^{2} \in ℂ$
9	7 8	mpan2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G (i S B))}^{2} \in ℂ$
10		mulcl	$⊢ (i \in ℂ \land {N (A G (i S B))}^{2} \in ℂ) \to i {N (A G (i S B))}^{2} \in ℂ$
11	7 9 10	sylancr	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i {N (A G (i S B))}^{2} \in ℂ$
12		neg1cn	$⊢ - 1 \in ℂ$
13	1 2 3 4 5	ipval2lem4	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land - 1 \in ℂ) \to {N (A G (-1 S B))}^{2} \in ℂ$
14	12 13	mpan2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G (-1 S B))}^{2} \in ℂ$
15	11 14	subcld	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i {N (A G (i S B))}^{2} - {N (A G (-1 S B))}^{2} \in ℂ$
16		negicn	$⊢ - i \in ℂ$
17	1 2 3 4 5	ipval2lem4	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land - i \in ℂ) \to {N (A G ((- i) S B))}^{2} \in ℂ$
18	16 17	mpan2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G ((- i) S B))}^{2} \in ℂ$
19		mulcl	$⊢ (i \in ℂ \land {N (A G ((- i) S B))}^{2} \in ℂ) \to i {N (A G ((- i) S B))}^{2} \in ℂ$
20	7 18 19	sylancr	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i {N (A G ((- i) S B))}^{2} \in ℂ$
21	15 20	negsubd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i {N (A G (i S B))}^{2} - {N (A G (-1 S B))}^{2} + (- i {N (A G ((- i) S B))}^{2}) = i {N (A G (i S B))}^{2} - {N (A G (-1 S B))}^{2} - i {N (A G ((- i) S B))}^{2}$
22	14	mulm1d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to -1 {N (A G (-1 S B))}^{2} = - {N (A G (-1 S B))}^{2}$
23	22	oveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2} = i {N (A G (i S B))}^{2} + (- {N (A G (-1 S B))}^{2})$
24	11 14	negsubd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i {N (A G (i S B))}^{2} + (- {N (A G (-1 S B))}^{2}) = i {N (A G (i S B))}^{2} - {N (A G (-1 S B))}^{2}$
25	23 24	eqtrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2} = i {N (A G (i S B))}^{2} - {N (A G (-1 S B))}^{2}$
26		mulneg1	$⊢ (i \in ℂ \land {N (A G ((- i) S B))}^{2} \in ℂ) \to (- i) {N (A G ((- i) S B))}^{2} = - i {N (A G ((- i) S B))}^{2}$
27	7 18 26	sylancr	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (- i) {N (A G ((- i) S B))}^{2} = - i {N (A G ((- i) S B))}^{2}$
28	25 27	oveq12d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2} + (- i) {N (A G ((- i) S B))}^{2} = i {N (A G (i S B))}^{2} - {N (A G (-1 S B))}^{2} + (- i {N (A G ((- i) S B))}^{2})$
29		subdi	$⊢ (i \in ℂ \land {N (A G (i S B))}^{2} \in ℂ \land {N (A G ((- i) S B))}^{2} \in ℂ) \to i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2}) = i {N (A G (i S B))}^{2} - i {N (A G ((- i) S B))}^{2}$
30	7 29	mp3an1	$⊢ ({N (A G (i S B))}^{2} \in ℂ \land {N (A G ((- i) S B))}^{2} \in ℂ) \to i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2}) = i {N (A G (i S B))}^{2} - i {N (A G ((- i) S B))}^{2}$
31	9 18 30	syl2anc	$⊢ (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}) = i {N (A G (i S B))}^{2} - i {N (A G ((- i) S B))}^{2}$
32	31	oveq1d	$⊢ (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}) - {N (A G (-1 S B))}^{2} = i {N (A G (i S B))}^{2} - i {N (A G ((- i) S B))}^{2} - {N (A G (-1 S B))}^{2}$
33	11 20 14	sub32d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i {N (A G (i S B))}^{2} - i {N (A G ((- i) S B))}^{2} - {N (A G (-1 S B))}^{2} = i {N (A G (i S B))}^{2} - {N (A G (-1 S B))}^{2} - i {N (A G ((- i) S B))}^{2}$
34	32 33	eqtrd	$⊢ (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}) - {N (A G (-1 S B))}^{2} = i {N (A G (i S B))}^{2} - {N (A G (-1 S B))}^{2} - i {N (A G ((- i) S B))}^{2}$
35	21 28 34	3eqtr4d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2} + (- i) {N (A G ((- i) S B))}^{2} = i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2}) - {N (A G (-1 S B))}^{2}$
36	1 3	nvsid	$⊢ (U \in NrmCVec \land B \in X) \to 1 S B = B$
37	36	oveq2d	$⊢ (U \in NrmCVec \land B \in X) \to A G (1 S B) = A G B$
38	37	fveq2d	$⊢ (U \in NrmCVec \land B \in X) \to N (A G (1 S B)) = N (A G B)$
39	38	oveq1d	$⊢ (U \in NrmCVec \land B \in X) \to {N (A G (1 S B))}^{2} = {N (A G B)}^{2}$
40	39	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}$
41	40	oveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to 1 {N (A G (1 S B))}^{2} = 1 {N (A G B)}^{2}$
42	1 2 3 4 5	ipval2lem3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G B)}^{2} \in ℝ$
43	42	recnd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {N (A G B)}^{2} \in ℂ$
44	43	mullidd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to 1 {N (A G B)}^{2} = {N (A G B)}^{2}$
45	41 44	eqtrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to 1 {N (A G (1 S B))}^{2} = {N (A G B)}^{2}$
46	35 45	oveq12d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2}) + (- i) {N (A G ((- i) S B))}^{2} + 1 {N (A G (1 S B))}^{2} = i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2}) - {N (A G (-1 S B))}^{2} + {N (A G B)}^{2}$
47		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
48		df-4	$⊢ 4 = 3 + 1$
49		oveq2	$⊢ k = 4 \to i^{k} = i^{4}$
50		i4	$⊢ i^{4} = 1$
51	49 50	eqtrdi	$⊢ k = 4 \to i^{k} = 1$
52	51	oveq1d	$⊢ k = 4 \to i^{k} S B = 1 S B$
53	52	oveq2d	$⊢ k = 4 \to A G (i^{k} S B) = A G (1 S B)$
54	53	fveq2d	$⊢ k = 4 \to N (A G (i^{k} S B)) = N (A G (1 S B))$
55	54	oveq1d	$⊢ k = 4 \to {N (A G (i^{k} S B))}^{2} = {N (A G (1 S B))}^{2}$
56	51 55	oveq12d	$⊢ k = 4 \to i^{k} {N (A G (i^{k} S B))}^{2} = 1 {N (A G (1 S B))}^{2}$
57		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
58		expcl	$⊢ (i \in ℂ \land k \in ℕ_{0}) \to i^{k} \in ℂ$
59	7 57 58	sylancr	$⊢ k \in ℕ \to i^{k} \in ℂ$
60	59	adantl	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land k \in ℕ) \to i^{k} \in ℂ$
61	1 2 3 4 5	ipval2lem4	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land i^{k} \in ℂ) \to {N (A G (i^{k} S B))}^{2} \in ℂ$
62	59 61	sylan2	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land k \in ℕ) \to {N (A G (i^{k} S B))}^{2} \in ℂ$
63	60 62	mulcld	$⊢ ((U \in NrmCVec \land A \in X \land B \in X) \land k \in ℕ) \to i^{k} {N (A G (i^{k} S B))}^{2} \in ℂ$
64		df-3	$⊢ 3 = 2 + 1$
65		oveq2	$⊢ k = 3 \to i^{k} = i^{3}$
66		i3	$⊢ i^{3} = - i$
67	65 66	eqtrdi	$⊢ k = 3 \to i^{k} = - i$
68	67	oveq1d	$⊢ k = 3 \to i^{k} S B = (- i) S B$
69	68	oveq2d	$⊢ k = 3 \to A G (i^{k} S B) = A G ((- i) S B)$
70	69	fveq2d	$⊢ k = 3 \to N (A G (i^{k} S B)) = N (A G ((- i) S B))$
71	70	oveq1d	$⊢ k = 3 \to {N (A G (i^{k} S B))}^{2} = {N (A G ((- i) S B))}^{2}$
72	67 71	oveq12d	$⊢ k = 3 \to i^{k} {N (A G (i^{k} S B))}^{2} = (- i) {N (A G ((- i) S B))}^{2}$
73		df-2	$⊢ 2 = 1 + 1$
74		oveq2	$⊢ k = 2 \to i^{k} = i^{2}$
75		i2	$⊢ i^{2} = - 1$
76	74 75	eqtrdi	$⊢ k = 2 \to i^{k} = - 1$
77	76	oveq1d	$⊢ k = 2 \to i^{k} S B = -1 S B$
78	77	oveq2d	$⊢ k = 2 \to A G (i^{k} S B) = A G (-1 S B)$
79	78	fveq2d	$⊢ k = 2 \to N (A G (i^{k} S B)) = N (A G (-1 S B))$
80	79	oveq1d	$⊢ k = 2 \to {N (A G (i^{k} S B))}^{2} = {N (A G (-1 S B))}^{2}$
81	76 80	oveq12d	$⊢ k = 2 \to i^{k} {N (A G (i^{k} S B))}^{2} = -1 {N (A G (-1 S B))}^{2}$
82		1z	$⊢ 1 \in ℤ$
83		oveq2	$⊢ k = 1 \to i^{k} = i^{1}$
84		exp1	$⊢ i \in ℂ \to i^{1} = i$
85	7 84	ax-mp	$⊢ i^{1} = i$
86	83 85	eqtrdi	$⊢ k = 1 \to i^{k} = i$
87	86	oveq1d	$⊢ k = 1 \to i^{k} S B = i S B$
88	87	oveq2d	$⊢ k = 1 \to A G (i^{k} S B) = A G (i S B)$
89	88	fveq2d	$⊢ k = 1 \to N (A G (i^{k} S B)) = N (A G (i S B))$
90	89	oveq1d	$⊢ k = 1 \to {N (A G (i^{k} S B))}^{2} = {N (A G (i S B))}^{2}$
91	86 90	oveq12d	$⊢ k = 1 \to i^{k} {N (A G (i^{k} S B))}^{2} = i {N (A G (i S B))}^{2}$
92	91	fsum1	$⊢ (1 \in ℤ \land i {N (A G (i S B))}^{2} \in ℂ) \to \sum_{k = 1}^{1} i^{k} {N (A G (i^{k} S B))}^{2} = i {N (A G (i S B))}^{2}$
93	82 11 92	sylancr	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to \sum_{k = 1}^{1} i^{k} {N (A G (i^{k} S B))}^{2} = i {N (A G (i S B))}^{2}$
94		1nn	$⊢ 1 \in ℕ$
95	93 94	jctil	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (1 \in ℕ \land \sum_{k = 1}^{1} i^{k} {N (A G (i^{k} S B))}^{2} = i {N (A G (i S B))}^{2})$
96		eqidd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2} = i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2}$
97	47 73 81 63 95 96	fsump1i	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (2 \in ℕ \land \sum_{k = 1}^{2} i^{k} {N (A G (i^{k} S B))}^{2} = i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2})$
98		eqidd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2} + (- i) {N (A G ((- i) S B))}^{2} = i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2} + (- i) {N (A G ((- i) S B))}^{2}$
99	47 64 72 63 97 98	fsump1i	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (3 \in ℕ \land \sum_{k = 1}^{3} i^{k} {N (A G (i^{k} S B))}^{2} = i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2} + (- i) {N (A G ((- i) S B))}^{2})$
100		eqidd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2}) + (- i) {N (A G ((- i) S B))}^{2} + 1 {N (A G (1 S B))}^{2} = (i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2}) + (- i) {N (A G ((- i) S B))}^{2} + 1 {N (A G (1 S B))}^{2}$
101	47 48 56 63 99 100	fsump1i	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (4 \in ℕ \land \sum_{k = 1}^{4} i^{k} {N (A G (i^{k} S B))}^{2} = (i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2}) + (- i) {N (A G ((- i) S B))}^{2} + 1 {N (A G (1 S B))}^{2})$
102	101	simprd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to \sum_{k = 1}^{4} i^{k} {N (A G (i^{k} S B))}^{2} = (i {N (A G (i S B))}^{2} + -1 {N (A G (-1 S B))}^{2}) + (- i) {N (A G ((- i) S B))}^{2} + 1 {N (A G (1 S B))}^{2}$
103	43 14	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 ℂ$
104	9 18	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 ℂ$
105		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 ℂ$
106	7 104 105	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 ℂ$
107	103 106	addcomd	$⊢ (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}) = i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2}) + {N (A G B)}^{2} - {N (A G (-1 S B))}^{2}$
108	106 14 43	subadd23d	$⊢ (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}) - {N (A G (-1 S B))}^{2} + {N (A G B)}^{2} = i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2}) + {N (A G B)}^{2} - {N (A G (-1 S B))}^{2}$
109	107 108	eqtr4d	$⊢ (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}) = i ({N (A G (i S B))}^{2} - {N (A G ((- i) S B))}^{2}) - {N (A G (-1 S B))}^{2} + {N (A G B)}^{2}$
110	46 102 109	3eqtr4d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to \sum_{k = 1}^{4} i^{k} {N (A G (i^{k} 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})$
111	110	oveq1d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to \frac{\sum_{k = 1}^{4} i^{k} {N (A G (i^{k} 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}$
112	6 111	eqtrd	$⊢ (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}$

Metamath Proof Explorer

Theorem ipval2

Proof