ipasslem10

Description: Lemma for ipassi . Show the inner product associative law for the imaginary number _i . (Contributed by NM, 24-Aug-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ip1i.1	$⊢ X = BaseSet (U)$
	ip1i.2	$⊢ G = +_{v} (U)$
	ip1i.4	$⊢ S = \cdot_{𝑠OLD} (U)$
	ip1i.7	$⊢ P = \cdot_{𝑖OLD} (U)$
	ip1i.9	$⊢ U \in {CPreHil}_{OLD}$
	ipasslem10.a	$⊢ A \in X$
	ipasslem10.b	$⊢ B \in X$
	ipasslem10.6	$⊢ N = {norm}_{CV} (U)$
Assertion	ipasslem10	$⊢ (i S A) P B = i (A P B)$

Proof

Step	Hyp	Ref	Expression
1		ip1i.1	$⊢ X = BaseSet (U)$
2		ip1i.2	$⊢ G = +_{v} (U)$
3		ip1i.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		ip1i.7	$⊢ P = \cdot_{𝑖OLD} (U)$
5		ip1i.9	$⊢ U \in {CPreHil}_{OLD}$
6		ipasslem10.a	$⊢ A \in X$
7		ipasslem10.b	$⊢ B \in X$
8		ipasslem10.6	$⊢ N = {norm}_{CV} (U)$
9	5	phnvi	$⊢ U \in NrmCVec$
10		ax-icn	$⊢ i \in ℂ$
11	1 3	nvscl	$⊢ (U \in NrmCVec \land i \in ℂ \land A \in X) \to i S A \in X$
12	9 10 6 11	mp3an	$⊢ i S A \in X$
13	1 2 3 8 4	4ipval2	$⊢ (U \in NrmCVec \land B \in X \land i S A \in X) \to 4 (B P (i S A)) = {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2} + i ({N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2})$
14	9 7 12 13	mp3an	$⊢ 4 (B P (i S A)) = {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2} + i ({N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2})$
15		4cn	$⊢ 4 \in ℂ$
16		negicn	$⊢ - i \in ℂ$
17	1 4	dipcl	$⊢ (U \in NrmCVec \land B \in X \land A \in X) \to B P A \in ℂ$
18	9 7 6 17	mp3an	$⊢ B P A \in ℂ$
19	15 16 18	mul12i	$⊢ 4 (- i) (B P A) = (- i) 4 (B P A)$
20	1 2	nvgcl	$⊢ (U \in NrmCVec \land B \in X \land i S A \in X) \to B G (i S A) \in X$
21	9 7 12 20	mp3an	$⊢ B G (i S A) \in X$
22	1 8 9 21	nvcli	$⊢ N (B G (i S A)) \in ℝ$
23	22	recni	$⊢ N (B G (i S A)) \in ℂ$
24	23	sqcli	$⊢ {N (B G (i S A))}^{2} \in ℂ$
25		neg1cn	$⊢ - 1 \in ℂ$
26	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land i S A \in X) \to -1 S (i S A) \in X$
27	9 25 12 26	mp3an	$⊢ -1 S (i S A) \in X$
28	1 2	nvgcl	$⊢ (U \in NrmCVec \land B \in X \land -1 S (i S A) \in X) \to B G (-1 S (i S A)) \in X$
29	9 7 27 28	mp3an	$⊢ B G (-1 S (i S A)) \in X$
30	1 8 9 29	nvcli	$⊢ N (B G (-1 S (i S A))) \in ℝ$
31	30	recni	$⊢ N (B G (-1 S (i S A))) \in ℂ$
32	31	sqcli	$⊢ {N (B G (-1 S (i S A)))}^{2} \in ℂ$
33	24 32	subcli	$⊢ {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2} \in ℂ$
34	1 3	nvscl	$⊢ (U \in NrmCVec \land i \in ℂ \land i S A \in X) \to i S (i S A) \in X$
35	9 10 12 34	mp3an	$⊢ i S (i S A) \in X$
36	1 2	nvgcl	$⊢ (U \in NrmCVec \land B \in X \land i S (i S A) \in X) \to B G (i S (i S A)) \in X$
37	9 7 35 36	mp3an	$⊢ B G (i S (i S A)) \in X$
38	1 8 9 37	nvcli	$⊢ N (B G (i S (i S A))) \in ℝ$
39	38	recni	$⊢ N (B G (i S (i S A))) \in ℂ$
40	39	sqcli	$⊢ {N (B G (i S (i S A)))}^{2} \in ℂ$
41	1 3	nvscl	$⊢ (U \in NrmCVec \land - i \in ℂ \land i S A \in X) \to (- i) S (i S A) \in X$
42	9 16 12 41	mp3an	$⊢ (- i) S (i S A) \in X$
43	1 2	nvgcl	$⊢ (U \in NrmCVec \land B \in X \land (- i) S (i S A) \in X) \to B G ((- i) S (i S A)) \in X$
44	9 7 42 43	mp3an	$⊢ B G ((- i) S (i S A)) \in X$
45	1 8 9 44	nvcli	$⊢ N (B G ((- i) S (i S A))) \in ℝ$
46	45	recni	$⊢ N (B G ((- i) S (i S A))) \in ℂ$
47	46	sqcli	$⊢ {N (B G ((- i) S (i S A)))}^{2} \in ℂ$
48	40 47	subcli	$⊢ {N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2} \in ℂ$
49	10 48	mulcli	$⊢ i ({N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2}) \in ℂ$
50	33 49	addcomi	$⊢ {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2} + i ({N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2}) = i ({N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2}) + {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2}$
51	1 2	nvgcl	$⊢ (U \in NrmCVec \land B \in X \land A \in X) \to B G A \in X$
52	9 7 6 51	mp3an	$⊢ B G A \in X$
53	1 8 9 52	nvcli	$⊢ N (B G A) \in ℝ$
54	53	recni	$⊢ N (B G A) \in ℂ$
55	54	sqcli	$⊢ {N (B G A)}^{2} \in ℂ$
56	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land A \in X) \to -1 S A \in X$
57	9 25 6 56	mp3an	$⊢ -1 S A \in X$
58	1 2	nvgcl	$⊢ (U \in NrmCVec \land B \in X \land -1 S A \in X) \to B G (-1 S A) \in X$
59	9 7 57 58	mp3an	$⊢ B G (-1 S A) \in X$
60	1 8 9 59	nvcli	$⊢ N (B G (-1 S A)) \in ℝ$
61	60	recni	$⊢ N (B G (-1 S A)) \in ℂ$
62	61	sqcli	$⊢ {N (B G (-1 S A))}^{2} \in ℂ$
63	55 62	subcli	$⊢ {N (B G A)}^{2} - {N (B G (-1 S A))}^{2} \in ℂ$
64	1 3	nvscl	$⊢ (U \in NrmCVec \land - i \in ℂ \land A \in X) \to (- i) S A \in X$
65	9 16 6 64	mp3an	$⊢ (- i) S A \in X$
66	1 2	nvgcl	$⊢ (U \in NrmCVec \land B \in X \land (- i) S A \in X) \to B G ((- i) S A) \in X$
67	9 7 65 66	mp3an	$⊢ B G ((- i) S A) \in X$
68	1 8 9 67	nvcli	$⊢ N (B G ((- i) S A)) \in ℝ$
69	68	recni	$⊢ N (B G ((- i) S A)) \in ℂ$
70	69	sqcli	$⊢ {N (B G ((- i) S A))}^{2} \in ℂ$
71	24 70	subcli	$⊢ {N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2} \in ℂ$
72	10 71	mulcli	$⊢ i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2}) \in ℂ$
73	16 63 72	adddii	$⊢ (- i) ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2} + i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2})) = (- i) ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2}) + (- i) i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2})$
74	10 10 6	3pm3.2i	$⊢ (i \in ℂ \land i \in ℂ \land A \in X)$
75	1 3	nvsass	$⊢ (U \in NrmCVec \land (i \in ℂ \land i \in ℂ \land A \in X)) \to i i S A = i S (i S A)$
76	9 74 75	mp2an	$⊢ i i S A = i S (i S A)$
77		ixi	$⊢ i i = - 1$
78	77	oveq1i	$⊢ i i S A = -1 S A$
79	76 78	eqtr3i	$⊢ i S (i S A) = -1 S A$
80	79	oveq2i	$⊢ B G (i S (i S A)) = B G (-1 S A)$
81	80	fveq2i	$⊢ N (B G (i S (i S A))) = N (B G (-1 S A))$
82	81	oveq1i	$⊢ {N (B G (i S (i S A)))}^{2} = {N (B G (-1 S A))}^{2}$
83	10 10	mulneg1i	$⊢ (- i) i = - i i$
84	77	negeqi	$⊢ - i i = - -1$
85		negneg1e1	$⊢ - -1 = 1$
86	83 84 85	3eqtri	$⊢ (- i) i = 1$
87	86	oveq1i	$⊢ (- i) i S A = 1 S A$
88	16 10 6	3pm3.2i	$⊢ (- i \in ℂ \land i \in ℂ \land A \in X)$
89	1 3	nvsass	$⊢ (U \in NrmCVec \land (- i \in ℂ \land i \in ℂ \land A \in X)) \to (- i) i S A = (- i) S (i S A)$
90	9 88 89	mp2an	$⊢ (- i) i S A = (- i) S (i S A)$
91	1 3	nvsid	$⊢ (U \in NrmCVec \land A \in X) \to 1 S A = A$
92	9 6 91	mp2an	$⊢ 1 S A = A$
93	87 90 92	3eqtr3i	$⊢ (- i) S (i S A) = A$
94	93	oveq2i	$⊢ B G ((- i) S (i S A)) = B G A$
95	94	fveq2i	$⊢ N (B G ((- i) S (i S A))) = N (B G A)$
96	95	oveq1i	$⊢ {N (B G ((- i) S (i S A)))}^{2} = {N (B G A)}^{2}$
97	82 96	oveq12i	$⊢ {N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2} = {N (B G (-1 S A))}^{2} - {N (B G A)}^{2}$
98	97	oveq2i	$⊢ i ({N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2}) = i ({N (B G (-1 S A))}^{2} - {N (B G A)}^{2})$
99	63	mulm1i	$⊢ -1 ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2}) = - ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2})$
100	55 62	negsubdi2i	$⊢ - ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2}) = {N (B G (-1 S A))}^{2} - {N (B G A)}^{2}$
101	99 100	eqtr2i	$⊢ {N (B G (-1 S A))}^{2} - {N (B G A)}^{2} = -1 ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2})$
102	101	oveq2i	$⊢ i ({N (B G (-1 S A))}^{2} - {N (B G A)}^{2}) = i -1 ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2})$
103	10 25 63	mulassi	$⊢ i -1 ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2}) = i -1 ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2})$
104	102 103	eqtr4i	$⊢ i ({N (B G (-1 S A))}^{2} - {N (B G A)}^{2}) = i -1 ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2})$
105	10	mulm1i	$⊢ -1 i = - i$
106	25 10 105	mulcomli	$⊢ i -1 = - i$
107	106	oveq1i	$⊢ i -1 ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2}) = (- i) ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2})$
108	98 104 107	3eqtri	$⊢ i ({N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2}) = (- i) ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2})$
109	25 10 6	3pm3.2i	$⊢ (- 1 \in ℂ \land i \in ℂ \land A \in X)$
110	1 3	nvsass	$⊢ (U \in NrmCVec \land (- 1 \in ℂ \land i \in ℂ \land A \in X)) \to -1 i S A = -1 S (i S A)$
111	9 109 110	mp2an	$⊢ -1 i S A = -1 S (i S A)$
112	105	oveq1i	$⊢ -1 i S A = (- i) S A$
113	111 112	eqtr3i	$⊢ -1 S (i S A) = (- i) S A$
114	113	oveq2i	$⊢ B G (-1 S (i S A)) = B G ((- i) S A)$
115	114	fveq2i	$⊢ N (B G (-1 S (i S A))) = N (B G ((- i) S A))$
116	115	oveq1i	$⊢ {N (B G (-1 S (i S A)))}^{2} = {N (B G ((- i) S A))}^{2}$
117	116	oveq2i	$⊢ {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2} = {N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2}$
118	71	mulid2i	$⊢ 1 ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2}) = {N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2}$
119	117 118	eqtr4i	$⊢ {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2} = 1 ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2})$
120	86	oveq1i	$⊢ (- i) i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2}) = 1 ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2})$
121	119 120	eqtr4i	$⊢ {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2} = (- i) i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2})$
122	16 10 71	mulassi	$⊢ (- i) i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2}) = (- i) i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2})$
123	121 122	eqtri	$⊢ {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2} = (- i) i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2})$
124	108 123	oveq12i	$⊢ i ({N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2}) + {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2} = (- i) ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2}) + (- i) i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2})$
125	73 124	eqtr4i	$⊢ (- i) ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2} + i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2})) = i ({N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2}) + {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2}$
126	50 125	eqtr4i	$⊢ {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2} + i ({N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2}) = (- i) ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2} + i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2}))$
127	1 2 3 8 4	4ipval2	$⊢ (U \in NrmCVec \land B \in X \land A \in X) \to 4 (B P A) = {N (B G A)}^{2} - {N (B G (-1 S A))}^{2} + i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2})$
128	9 7 6 127	mp3an	$⊢ 4 (B P A) = {N (B G A)}^{2} - {N (B G (-1 S A))}^{2} + i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2})$
129	128	oveq2i	$⊢ (- i) 4 (B P A) = (- i) ({N (B G A)}^{2} - {N (B G (-1 S A))}^{2} + i ({N (B G (i S A))}^{2} - {N (B G ((- i) S A))}^{2}))$
130	126 129	eqtr4i	$⊢ {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2} + i ({N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2}) = (- i) 4 (B P A)$
131	19 130	eqtr4i	$⊢ 4 (- i) (B P A) = {N (B G (i S A))}^{2} - {N (B G (-1 S (i S A)))}^{2} + i ({N (B G (i S (i S A)))}^{2} - {N (B G ((- i) S (i S A)))}^{2})$
132	14 131	eqtr4i	$⊢ 4 (B P (i S A)) = 4 (- i) (B P A)$
133	1 4	dipcl	$⊢ (U \in NrmCVec \land B \in X \land i S A \in X) \to B P (i S A) \in ℂ$
134	9 7 12 133	mp3an	$⊢ B P (i S A) \in ℂ$
135	16 18	mulcli	$⊢ (- i) (B P A) \in ℂ$
136		4ne0	$⊢ 4 \neq 0$
137	134 135 15 136	mulcani	$⊢ 4 (B P (i S A)) = 4 (- i) (B P A) \leftrightarrow B P (i S A) = (- i) (B P A)$
138	132 137	mpbi	$⊢ B P (i S A) = (- i) (B P A)$
139	138	fveq2i	$⊢ \overline{B P (i S A)} = \overline{(- i) (B P A)}$
140	1 4	dipcj	$⊢ (U \in NrmCVec \land B \in X \land i S A \in X) \to \overline{B P (i S A)} = (i S A) P B$
141	9 7 12 140	mp3an	$⊢ \overline{B P (i S A)} = (i S A) P B$
142	16 18	cjmuli	$⊢ \overline{(- i) (B P A)} = \overline{- i} \overline{B P A}$
143	25 10	cjmuli	$⊢ \overline{-1 i} = \overline{- 1} \overline{i}$
144	105	fveq2i	$⊢ \overline{-1 i} = \overline{- i}$
145		neg1rr	$⊢ - 1 \in ℝ$
146	25	cjrebi	$⊢ - 1 \in ℝ \leftrightarrow \overline{- 1} = - 1$
147	145 146	mpbi	$⊢ \overline{- 1} = - 1$
148		cji	$⊢ \overline{i} = - i$
149	147 148	oveq12i	$⊢ \overline{- 1} \overline{i} = -1 (- i)$
150		ax-1cn	$⊢ 1 \in ℂ$
151	150 10	mul2negi	$⊢ -1 (- i) = 1 i$
152	10	mulid2i	$⊢ 1 i = i$
153	149 151 152	3eqtri	$⊢ \overline{- 1} \overline{i} = i$
154	143 144 153	3eqtr3i	$⊢ \overline{- i} = i$
155	1 4	dipcj	$⊢ (U \in NrmCVec \land B \in X \land A \in X) \to \overline{B P A} = A P B$
156	9 7 6 155	mp3an	$⊢ \overline{B P A} = A P B$
157	154 156	oveq12i	$⊢ \overline{- i} \overline{B P A} = i (A P B)$
158	142 157	eqtri	$⊢ \overline{(- i) (B P A)} = i (A P B)$
159	139 141 158	3eqtr3i	$⊢ (i S A) P B = i (A P B)$

Metamath Proof Explorer

Theorem ipasslem10

Proof