Theorem ipasslem10 8443

Description: Lemma for ipassi 8445. Show the inner product associative law for the imaginary number i.

Hypotheses

Ref	Expression
ip1i.1	|- X = (Base` U)
ip1i.2	|- G = (+v` U)
ip1i.4	|- S = (.s` U)
ip1i.7	|- P = (.i` U)
ip1i.9	|- U e. CPreHil
ipasslem10.a	|- A e. X
ipasslem10.b	|- B e. X
ipasslem10.6	|- N = (norm` U)

Assertion

Ref	Expression
ipasslem10	|- ((iSA)PB) = (i x. (APB))

Proof of Theorem ipasslem10

Step	Hyp	Ref	Expression
1		ip1i.9	. . . . . . . . . . . . . . . . 17 |- U e. CPreHil
2	1	phnvi 8419	. . . . . . . . . . . . . . . 16 |- U e. NrmCVec
3		axicn 5250	. . . . . . . . . . . . . . . . 17 |- i e. CC
4		ipasslem10.a	. . . . . . . . . . . . . . . . 17 |- A e. X
5	3, 3, 4	3pm3.2i 817	. . . . . . . . . . . . . . . 16 |- (i e. CC /\ i e. CC /\ A e. X)
6		ip1i.1	. . . . . . . . . . . . . . . . 17 |- X = (Base` U)
7		ip1i.4	. . . . . . . . . . . . . . . . 17 |- S = (.s` U)
8	6, 7	nvsass 8201	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ (i e. CC /\ i e. CC /\ A e. X)) -> ((i x. i)SA) = (iS(iSA)))
9	2, 5, 8	mp2an 696	. . . . . . . . . . . . . . 15 |- ((i x. i)SA) = (iS(iSA))
10		ixi 5662	. . . . . . . . . . . . . . . 16 |- (i x. i) = -u1
11	10	opreq1i 3962	. . . . . . . . . . . . . . 15 |- ((i x. i)SA) = (-u1SA)
12	9, 11	eqtr3 1494	. . . . . . . . . . . . . 14 |- (iS(iSA)) = (-u1SA)
13	12	opreq2i 3963	. . . . . . . . . . . . 13 |- (BG(iS(iSA))) = (BG(-u1SA))
14	13	fveq2i 3718	. . . . . . . . . . . 12 |- (N` (BG(iS(iSA)))) = (N` (BG(-u1SA)))
15	14	opreq1i 3962	. . . . . . . . . . 11 |- ((N` (BG(iS(iSA))))^2) = ((N` (BG(-u1SA)))^2)
16	3, 3	mulneg1 5425	. . . . . . . . . . . . . . . . 17 |- (-ui x. i) = -u(i x. i)
17	10	negeqi 5340	. . . . . . . . . . . . . . . . 17 |- -u(i x. i) = -u-u1
18		ax1cn 5249	. . . . . . . . . . . . . . . . . 18 |- 1 e. CC
19	18	negneg 5370	. . . . . . . . . . . . . . . . 17 |- -u-u1 = 1
20	16, 17, 19	3eqtr 1496	. . . . . . . . . . . . . . . 16 |- (-ui x. i) = 1
21	20	opreq1i 3962	. . . . . . . . . . . . . . 15 |- ((-ui x. i)SA) = (1SA)
22	3	negcl 5349	. . . . . . . . . . . . . . . . 17 |- -ui e. CC
23	22, 3, 4	3pm3.2i 817	. . . . . . . . . . . . . . . 16 |- (-ui e. CC /\ i e. CC /\ A e. X)
24	6, 7	nvsass 8201	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ (-ui e. CC /\ i e. CC /\ A e. X)) -> ((-ui x. i)SA) = (-uiS(iSA)))
25	2, 23, 24	mp2an 696	. . . . . . . . . . . . . . 15 |- ((-ui x. i)SA) = (-uiS(iSA))
26	6, 7	nvsid 8200	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ A e. X) -> (1SA) = A)
27	2, 4, 26	mp2an 696	. . . . . . . . . . . . . . 15 |- (1SA) = A
28	21, 25, 27	3eqtr3 1500	. . . . . . . . . . . . . 14 |- (-uiS(iSA)) = A
29	28	opreq2i 3963	. . . . . . . . . . . . 13 |- (BG(-uiS(iSA))) = (BGA)
30	29	fveq2i 3718	. . . . . . . . . . . 12 |- (N` (BG(-uiS(iSA)))) = (N` (BGA))
31	30	opreq1i 3962	. . . . . . . . . . 11 |- ((N` (BG(-uiS(iSA))))^2) = ((N` (BGA))^2)
32	15, 31	opreq12i 3964	. . . . . . . . . 10 |- (((N` (BG(iS(iSA))))^2) - ((N` (BG(-uiS(iSA))))^2)) = (((N` (BG(-u1SA)))^2) - ((N` (BGA))^2))
33	32	opreq2i 3963	. . . . . . . . 9 |- (i x. (((N` (BG(iS(iSA))))^2) - ((N` (BG(-uiS(iSA))))^2))) = (i x. (((N` (BG(-u1SA)))^2) - ((N` (BGA))^2)))
34		ipasslem10.6	. . . . . . . . . . . . . . . . 17 |- N = (norm` U)
35		ipasslem10.b	. . . . . . . . . . . . . . . . . 18 |- B e. X
36		ip1i.2	. . . . . . . . . . . . . . . . . . 19 |- G = (+v` U)
37	6, 36	nvgcl 8191	. . . . . . . . . . . . . . . . . 18 |- ((U e. NrmCVec /\ B e. X /\ A e. X) -> (BGA) e. X)
38	2, 35, 4, 37	mp3an 914	. . . . . . . . . . . . . . . . 17 |- (BGA) e. X
39	6, 34, 2, 38	nvcli 8240	. . . . . . . . . . . . . . . 16 |- (N` (BGA)) e. RR
40	39	recn 5294	. . . . . . . . . . . . . . 15 |- (N` (BGA)) e. CC
41	40	sqcl 6553	. . . . . . . . . . . . . 14 |- ((N` (BGA))^2) e. CC
42	18	negcl 5349	. . . . . . . . . . . . . . . . . . 19 |- -u1 e. CC
43	6, 7	nvscl 8199	. . . . . . . . . . . . . . . . . . 19 |- ((U e. NrmCVec /\ -u1 e. CC /\ A e. X) -> (-u1SA) e. X)
44	2, 42, 4, 43	mp3an 914	. . . . . . . . . . . . . . . . . 18 |- (-u1SA) e. X
45	6, 36	nvgcl 8191	. . . . . . . . . . . . . . . . . 18 |- ((U e. NrmCVec /\ B e. X /\ (-u1SA) e. X) -> (BG(-u1SA)) e. X)
46	2, 35, 44, 45	mp3an 914	. . . . . . . . . . . . . . . . 17 |- (BG(-u1SA)) e. X
47	6, 34, 2, 46	nvcli 8240	. . . . . . . . . . . . . . . 16 |- (N` (BG(-u1SA))) e. RR
48	47	recn 5294	. . . . . . . . . . . . . . 15 |- (N` (BG(-u1SA))) e. CC
49	48	sqcl 6553	. . . . . . . . . . . . . 14 |- ((N` (BG(-u1SA)))^2) e. CC
50	41, 49	subcl 5346	. . . . . . . . . . . . 13 |- (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)) e. CC
51	50	mulm1 5452	. . . . . . . . . . . 12 |- (-u1 x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2))) = -u(((N` (BGA))^2) - ((N` (BG(-u1SA)))^2))
52	41, 49	negsubdi2 5430	. . . . . . . . . . . 12 |- -u(((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)) = (((N` (BG(-u1SA)))^2) - ((N` (BGA))^2))
53	51, 52	eqtr2 1493	. . . . . . . . . . 11 |- (((N` (BG(-u1SA)))^2) - ((N` (BGA))^2)) = (-u1 x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)))
54	53	opreq2i 3963	. . . . . . . . . 10 |- (i x. (((N` (BG(-u1SA)))^2) - ((N` (BGA))^2))) = (i x. (-u1 x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2))))
55	3, 42, 50	mulass 5305	. . . . . . . . . 10 |- ((i x. -u1) x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2))) = (i x. (-u1 x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2))))
56	54, 55	eqtr4 1495	. . . . . . . . 9 |- (i x. (((N` (BG(-u1SA)))^2) - ((N` (BGA))^2))) = ((i x. -u1) x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)))
57	3, 42	mulcom 5303	. . . . . . . . . . 11 |- (i x. -u1) = (-u1 x. i)
58	3	mulm1 5452	. . . . . . . . . . 11 |- (-u1 x. i) = -ui
59	57, 58	eqtr 1492	. . . . . . . . . 10 |- (i x. -u1) = -ui
60	59	opreq1i 3962	. . . . . . . . 9 |- ((i x. -u1) x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2))) = (-ui x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)))
61	33, 56, 60	3eqtr 1496	. . . . . . . 8 |- (i x. (((N` (BG(iS(iSA))))^2) - ((N` (BG(-uiS(iSA))))^2))) = (-ui x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)))
62	42, 3, 4	3pm3.2i 817	. . . . . . . . . . . . . . . 16 |- (-u1 e. CC /\ i e. CC /\ A e. X)
63	6, 7	nvsass 8201	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ (-u1 e. CC /\ i e. CC /\ A e. X)) -> ((-u1 x. i)SA) = (-u1S(iSA)))
64	2, 62, 63	mp2an 696	. . . . . . . . . . . . . . 15 |- ((-u1 x. i)SA) = (-u1S(iSA))
65	58	opreq1i 3962	. . . . . . . . . . . . . . 15 |- ((-u1 x. i)SA) = (-uiSA)
66	64, 65	eqtr3 1494	. . . . . . . . . . . . . 14 |- (-u1S(iSA)) = (-uiSA)
67	66	opreq2i 3963	. . . . . . . . . . . . 13 |- (BG(-u1S(iSA))) = (BG(-uiSA))
68	67	fveq2i 3718	. . . . . . . . . . . 12 |- (N` (BG(-u1S(iSA)))) = (N` (BG(-uiSA)))
69	68	opreq1i 3962	. . . . . . . . . . 11 |- ((N` (BG(-u1S(iSA))))^2) = ((N` (BG(-uiSA)))^2)
70	69	opreq2i 3963	. . . . . . . . . 10 |- (((N` (BG(iSA)))^2) - ((N` (BG(-u1S(iSA))))^2)) = (((N` (B