Theorem ipasslem10 10709

Description: Lemma for ipassi 10711. Show the inner product associative law for the imaginary number _i.

Hypotheses

Ref	Expression
ip1i.1	|- X = (BaseSet` 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 10685	. . . . . . . . . . . . . . . 16 |- U e. NrmCVec
3		axicn 6788	. . . . . . . . . . . . . . . . 17 |- _i e. CC
4		ipasslem10.a	. . . . . . . . . . . . . . . . 17 |- A e. X
5	3, 3, 4	3pm3.2i 1298	. . . . . . . . . . . . . . . 16 |- (_i e. CC /\ _i e. CC /\ A e. X)
6		ip1i.1	. . . . . . . . . . . . . . . . 17 |- X = (BaseSet` U)
7		ip1i.4	. . . . . . . . . . . . . . . . 17 |- S = (.s` U)
8	6, 7	nvsass 10450	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ (_i e. CC /\ _i e. CC /\ A e. X)) -> ((_i x. _i)SA) = (_iS(_iSA)))
9	2, 5, 8	mp2an 681	. . . . . . . . . . . . . . 15 |- ((_i x. _i)SA) = (_iS(_iSA))
10		ixi 7205	. . . . . . . . . . . . . . . 16 |- (_i x. _i) = -u1
11	10	opreq1i 4989	. . . . . . . . . . . . . . 15 |- ((_i x. _i)SA) = (-u1SA)
12	9, 11	eqtr3i 2163	. . . . . . . . . . . . . 14 |- (_iS(_iSA)) = (-u1SA)
13	12	opreq2i 4990	. . . . . . . . . . . . 13 |- (BG(_iS(_iSA))) = (BG(-u1SA))
14	13	fveq2i 4768	. . . . . . . . . . . 12 |- (N` (BG(_iS(_iSA)))) = (N` (BG(-u1SA)))
15	14	opreq1i 4989	. . . . . . . . . . 11 |- ((N` (BG(_iS(_iSA))))^2) = ((N` (BG(-u1SA)))^2)
16	3, 3	mulneg1i 7082	. . . . . . . . . . . . . . . . 17 |- (-u_i x. _i) = -u(_i x. _i)
17	10	negeqi 7013	. . . . . . . . . . . . . . . . 17 |- -u(_i x. _i) = -u-u1
18		ax1cn 6787	. . . . . . . . . . . . . . . . . 18 |- 1 e. CC
19	18	negnegi 7043	. . . . . . . . . . . . . . . . 17 |- -u-u1 = 1
20	16, 17, 19	3eqtri 2165	. . . . . . . . . . . . . . . 16 |- (-u_i x. _i) = 1
21	20	opreq1i 4989	. . . . . . . . . . . . . . 15 |- ((-u_i x. _i)SA) = (1SA)
22	3	negcli 7022	. . . . . . . . . . . . . . . . 17 |- -u_i e. CC
23	22, 3, 4	3pm3.2i 1298	. . . . . . . . . . . . . . . 16 |- (-u_i e. CC /\ _i e. CC /\ A e. X)
24	6, 7	nvsass 10450	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ (-u_i e. CC /\ _i e. CC /\ A e. X)) -> ((-u_i x. _i)SA) = (-u_iS(_iSA)))
25	2, 23, 24	mp2an 681	. . . . . . . . . . . . . . 15 |- ((-u_i x. _i)SA) = (-u_iS(_iSA))
26	6, 7	nvsid 10449	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ A e. X) -> (1SA) = A)
27	2, 4, 26	mp2an 681	. . . . . . . . . . . . . . 15 |- (1SA) = A
28	21, 25, 27	3eqtr3i 2169	. . . . . . . . . . . . . 14 |- (-u_iS(_iSA)) = A
29	28	opreq2i 4990	. . . . . . . . . . . . 13 |- (BG(-u_iS(_iSA))) = (BGA)
30	29	fveq2i 4768	. . . . . . . . . . . 12 |- (N` (BG(-u_iS(_iSA)))) = (N` (BGA))
31	30	opreq1i 4989	. . . . . . . . . . 11 |- ((N` (BG(-u_iS(_iSA))))^2) = ((N` (BGA))^2)
32	15, 31	opreq12i 4991	. . . . . . . . . 10 |- (((N` (BG(_iS(_iSA))))^2) - ((N` (BG(-u_iS(_iSA))))^2)) = (((N` (BG(-u1SA)))^2) - ((N` (BGA))^2))
33	32	opreq2i 4990	. . . . . . . . 9 |- (_i x. (((N` (BG(_iS(_iSA))))^2) - ((N` (BG(-u_iS(_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 10440	. . . . . . . . . . . . . . . . . 18 |- ((U e. NrmCVec /\ B e. X /\ A e. X) -> (BGA) e. X)
38	2, 35, 4, 37	mp3an 1466	. . . . . . . . . . . . . . . . 17 |- (BGA) e. X
39	6, 34, 2, 38	nvcli 10489	. . . . . . . . . . . . . . . 16 |- (N` (BGA)) e. RR
40	39	recni 6818	. . . . . . . . . . . . . . 15 |- (N` (BGA)) e. CC
41	40	sqcli 8244	. . . . . . . . . . . . . 14 |- ((N` (BGA))^2) e. CC
42	18	negcli 7022	. . . . . . . . . . . . . . . . . . 19 |- -u1 e. CC
43	6, 7	nvscl 10448	. . . . . . . . . . . . . . . . . . 19 |- ((U e. NrmCVec /\ -u1 e. CC /\ A e. X) -> (-u1SA) e. X)
44	2, 42, 4, 43	mp3an 1466	. . . . . . . . . . . . . . . . . 18 |- (-u1SA) e. X
45	6, 36	nvgcl 10440	. . . . . . . . . . . . . . . . . 18 |- ((U e. NrmCVec /\ B e. X /\ (-u1SA) e. X) -> (BG(-u1SA)) e. X)
46	2, 35, 44, 45	mp3an 1466	. . . . . . . . . . . . . . . . 17 |- (BG(-u1SA)) e. X
47	6, 34, 2, 46	nvcli 10489	. . . . . . . . . . . . . . . 16 |- (N` (BG(-u1SA))) e. RR
48	47	recni 6818	. . . . . . . . . . . . . . 15 |- (N` (BG(-u1SA))) e. CC
49	48	sqcli 8244	. . . . . . . . . . . . . 14 |- ((N` (BG(-u1SA)))^2) e. CC
50	41, 49	subcli 7019	. . . . . . . . . . . . 13 |- (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)) e. CC
51	50	mulm1i 7109	. . . . . . . . . . . 12 |- (-u1 x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2))) = -u(((N` (BGA))^2) - ((N` (BG(-u1SA)))^2))
52	41, 49	negsubdi2i 7087	. . . . . . . . . . . 12 |- -u(((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)) = (((N` (BG(-u1SA)))^2) - ((N` (BGA))^2))
53	51, 52	eqtr2i 2162	. . . . . . . . . . 11 |- (((N` (BG(-u1SA)))^2) - ((N` (BGA))^2)) = (-u1 x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)))
54	53	opreq2i 4990	. . . . . . . . . 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	mulassi 6828	. . . . . . . . . 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	eqtr4i 2164	. . . . . . . . 9 |- (_i x. (((N` (BG(-u1SA)))^2) - ((N` (BGA))^2))) = ((_i x. -u1) x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)))
57	3, 42	mulcomi 6826	. . . . . . . . . . 11 |- (_i x. -u1) = (-u1 x. _i)
58	3	mulm1i 7109	. . . . . . . . . . 11 |- (-u1 x. _i) = -u_i
59	57, 58	eqtri 2161	. . . . . . . . . 10 |- (_i x. -u1) = -u_i
60	59	opreq1i 4989	. . . . . . . . 9 |- ((_i x. -u1) x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2))) = (-u_i x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)))
61	33, 56, 60	3eqtri 2165	. . . . . . . 8 |- (_i x. (((N` (BG(_iS(_iSA))))^2) - ((N` (BG(-u_iS(_iSA))))^2))) = (-u_i x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)))
62	42, 3, 4	3pm3.2i 1298	. . . . . . . . . . . . . . . 16 |- (-u1 e. CC /\ _i e. CC /\ A e. X)
63	6, 7	nvsass 10450	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ (-u1 e. CC /\ _i e. CC /\ A e. X)) -> ((-u1 x. _i)SA) = (-u1S(_iSA)))
64	2, 62, 63	mp2an 681	. . . . . . . . . . . . . . 15 |- ((-u1 x. _i)SA) = (-u1S(_iSA))
65	58	opreq1i 4989	. . . . . . . . . . . . . . 15 |- ((-u1 x. _i)SA) = (-u_iSA)
66	64, 65	eqtr3i 2163	. . . . . . . . . . . . . 14 |- (-u1S(_iSA)) = (-u_iSA)
67	66	opreq2i 4990	. . . . . . . . . . . . 13 |- (BG(-u1S(_iSA))) = (BG(-u_iSA))
68	67	fveq2i 4768	. . . . . . . . . . . 12 |- (N` (BG(-u1S(_iSA)))) = (N` (BG(-u_iSA)))
69	68	opreq1i 4989	. . . . . . . . . . 11 |- ((N` (BG(-u1S(_iSA))))^2) = ((N` (BG(-u_iSA)))^2)
70	69	opreq2i 4990	. . . . . . . . . 10 |- (((N` (BG(_iSA)))^2) - ((N` (BG(-u1S(_iSA))))^2)) = (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2))
71	6, 7	nvscl 10448	. . . . . . . . . . . . . . . . 17 |- ((U e. NrmCVec /\ _i e. CC /\ A e. X) -> (_iSA) e. X)
72	2, 3, 4, 71	mp3an 1466	. . . . . . . . . . . . . . . 16 |- (_iSA) e. X
73	6, 36	nvgcl 10440	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ B e. X /\ (_iSA) e. X) -> (BG(_iSA)) e. X)
74	2, 35, 72, 73	mp3an 1466	. . . . . . . . . . . . . . 15 |- (BG(_iSA)) e. X
75	6, 34, 2, 74	nvcli 10489	. . . . . . . . . . . . . 14 |- (N` (BG(_iSA))) e. RR
76	75	recni 6818	. . . . . . . . . . . . 13 |- (N` (BG(_iSA))) e. CC
77	76	sqcli 8244	. . . . . . . . . . . 12 |- ((N` (BG(_iSA)))^2) e. CC
78	6, 7	nvscl 10448	. . . . . . . . . . . . . . . . 17 |- ((U e. NrmCVec /\ -u_i e. CC /\ A e. X) -> (-u_iSA) e. X)
79	2, 22, 4, 78	mp3an 1466	. . . . . . . . . . . . . . . 16 |- (-u_iSA) e. X
80	6, 36	nvgcl 10440	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ B e. X /\ (-u_iSA) e. X) -> (BG(-u_iSA)) e. X)
81	2, 35, 79, 80	mp3an 1466	. . . . . . . . . . . . . . 15 |- (BG(-u_iSA)) e. X
82	6, 34, 2, 81	nvcli 10489	. . . . . . . . . . . . . 14 |- (N` (BG(-u_iSA))) e. RR
83	82	recni 6818	. . . . . . . . . . . . 13 |- (N` (BG(-u_iSA))) e. CC
84	83	sqcli 8244	. . . . . . . . . . . 12 |- ((N` (BG(-u_iSA)))^2) e. CC
85	77, 84	subcli 7019	. . . . . . . . . . 11 |- (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2)) e. CC
86	85	mulid2i 6834	. . . . . . . . . 10 |- (1 x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2))) = (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2))
87	70, 86	eqtr4i 2164	. . . . . . . . 9 |- (((N` (BG(_iSA)))^2) - ((N` (BG(-u1S(_iSA))))^2)) = (1 x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2)))
88	20	opreq1i 4989	. . . . . . . . 9 |- ((-u_i x. _i) x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2))) = (1 x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2)))
89	22, 3, 85	mulassi 6828	. . . . . . . . 9 |- ((-u_i x. _i) x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2))) = (-u_i x. (_i x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2))))
90	87, 88, 89	3eqtr2i 2167	. . . . . . . 8 |- (((N` (BG(_iSA)))^2) - ((N` (BG(-u1S(_iSA))))^2)) = (-u_i x. (_i x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2))))
91	61, 90	opreq12i 4991	. . . . . . 7 |- ((_i x. (((N` (BG(_iS(_iSA))))^2) - ((N` (BG(-u_iS(_iSA))))^2))) + (((N` (BG(_iSA)))^2) - ((N` (BG(-u1S(_iSA))))^2))) = ((-u_i x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2))) + (-u_i x. (_i x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2)))))
92	6, 7	nvscl 10448	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ -u1 e. CC /\ (_iSA) e. X) -> (-u1S(_iSA)) e. X)
93	2, 42, 72, 92	mp3an 1466	. . . . . . . . . . . . 13 |- (-u1S(_iSA)) e. X
94	6, 36	nvgcl 10440	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ B e. X /\ (-u1S(_iSA)) e. X) -> (BG(-u1S(_iSA))) e. X)
95	2, 35, 93, 94	mp3an 1466	. . . . . . . . . . . 12 |- (BG(-u1S(_iSA))) e. X
96	6, 34, 2, 95	nvcli 10489	. . . . . . . . . . 11 |- (N` (BG(-u1S(_iSA)))) e. RR
97	96	recni 6818	. . . . . . . . . 10 |- (N` (BG(-u1S(_iSA)))) e. CC
98	97	sqcli 8244	. . . . . . . . 9 |- ((N` (BG(-u1S(_iSA))))^2) e. CC
99	77, 98	subcli 7019	. . . . . . . 8 |- (((N` (BG(_iSA)))^2) - ((N` (BG(-u1S(_iSA))))^2)) e. CC
100	6, 7	nvscl 10448	. . . . . . . . . . . . . . 15 |- ((U e. NrmCVec /\ _i e. CC /\ (_iSA) e. X) -> (_iS(_iSA)) e. X)
101	2, 3, 72, 100	mp3an 1466	. . . . . . . . . . . . . 14 |- (_iS(_iSA)) e. X
102	6, 36	nvgcl 10440	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ B e. X /\ (_iS(_iSA)) e. X) -> (BG(_iS(_iSA))) e. X)
103	2, 35, 101, 102	mp3an 1466	. . . . . . . . . . . . 13 |- (BG(_iS(_iSA))) e. X
104	6, 34, 2, 103	nvcli 10489	. . . . . . . . . . . 12 |- (N` (BG(_iS(_iSA)))) e. RR
105	104	recni 6818	. . . . . . . . . . 11 |- (N` (BG(_iS(_iSA)))) e. CC
106	105	sqcli 8244	. . . . . . . . . 10 |- ((N` (BG(_iS(_iSA))))^2) e. CC
107	6, 7	nvscl 10448	. . . . . . . . . . . . . . 15 |- ((U e. NrmCVec /\ -u_i e. CC /\ (_iSA) e. X) -> (-u_iS(_iSA)) e. X)
108	2, 22, 72, 107	mp3an 1466	. . . . . . . . . . . . . 14 |- (-u_iS(_iSA)) e. X
109	6, 36	nvgcl 10440	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ B e. X /\ (-u_iS(_iSA)) e. X) -> (BG(-u_iS(_iSA))) e. X)
110	2, 35, 108, 109	mp3an 1466	. . . . . . . . . . . . 13 |- (BG(-u_iS(_iSA))) e. X
111	6, 34, 2, 110	nvcli 10489	. . . . . . . . . . . 12 |- (N` (BG(-u_iS(_iSA)))) e. RR
112	111	recni 6818	. . . . . . . . . . 11 |- (N` (BG(-u_iS(_iSA)))) e. CC
113	112	sqcli 8244	. . . . . . . . . 10 |- ((N` (BG(-u_iS(_iSA))))^2) e. CC
114	106, 113	subcli 7019	. . . . . . . . 9 |- (((N` (BG(_iS(_iSA))))^2) - ((N` (BG(-u_iS(_iSA))))^2)) e. CC
115	3, 114	mulcli 6825	. . . . . . . 8 |- (_i x. (((N` (BG(_iS(_iSA))))^2) - ((N` (BG(-u_iS(_iSA))))^2))) e. CC
116	99, 115	addcomi 6987	. . . . . . 7 |- ((((N` (BG(_iSA)))^2) - ((N` (BG(-u1S(_iSA))))^2)) + (_i x. (((N` (BG(_iS(_iSA))))^2) - ((N` (BG(-u_iS(_iSA))))^2)))) = ((_i x. (((N` (BG(_iS(_iSA))))^2) - ((N` (BG(-u_iS(_iSA))))^2))) + (((N` (BG(_iSA)))^2) - ((N` (BG(-u1S(_iSA))))^2)))
117	3, 85	mulcli 6825	. . . . . . . 8 |- (_i x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2))) e. CC
118	22, 50, 117	adddii 6829	. . . . . . 7 |- (-u_i x. ((((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)) + (_i x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2))))) = ((-u_i x. (((N` (BGA))^2) - ((N` (BG(-u1SA)))^2))) + (-u_i x. (_i x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2)))))
119	91, 116, 118	3eqtr4i 2171	. . . . . 6 |- ((((N` (BG(_iSA)))^2) - ((N` (BG(-u1S(_iSA))))^2)) + (_i x. (((N` (BG(_iS(_iSA))))^2) - ((N` (BG(-u_iS(_iSA))))^2)))) = (-u_i x. ((((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)) + (_i x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2)))))
120		ip1i.7	. . . . . . . . 9 |- P = (.i` U)
121	6, 36, 7, 34, 120	4ipval2 10566	. . . . . . . 8 |- ((U e. NrmCVec /\ B e. X /\ A e. X) -> (4 x. (BPA)) = ((((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)) + (_i x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2)))))
122	2, 35, 4, 121	mp3an 1466	. . . . . . 7 |- (4 x. (BPA)) = ((((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)) + (_i x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2))))
123	122	opreq2i 4990	. . . . . 6 |- (-u_i x. (4 x. (BPA))) = (-u_i x. ((((N` (BGA))^2) - ((N` (BG(-u1SA)))^2)) + (_i x. (((N` (BG(_iSA)))^2) - ((N` (BG(-u_iSA)))^2)))))
124	119, 123	eqtr4i 2164	. . . . 5 |- ((((N` (BG(_iSA)))^2) - ((N` (BG(-u1S(_iSA))))^2)) + (_i x. (((N` (BG(_iS(_iSA))))^2) - ((N` (BG(-u_iS(_iSA))))^2)))) = (-u_i x. (4 x. (BPA)))
125	6, 36, 7, 34, 120	4ipval2 10566	. . . . . 6 |- ((U e. NrmCVec /\ B e. X /\ (_iSA) e. X) -> (4 x. (BP(_iSA))) = ((((N` (BG(_iSA)))^2) - ((N` (BG(-u1S(_iSA))))^2)) + (_i x. (((N` (BG(_iS(_iSA))))^2) - ((N` (BG(-u_iS(_iSA))))^2)))))
126	2, 35, 72, 125	mp3an 1466	. . . . 5 |- (4 x. (BP(_iSA))) = ((((N` (BG(_iSA)))^2) - ((N` (BG(-u1S(_iSA))))^2)) + (_i x. (((N` (BG(_iS(_iSA))))^2) - ((N` (BG(-u_iS(_iSA))))^2))))
127		4re 7499	. . . . . . 7 |- 4 e. RR
128	127	recni 6818	. . . . . 6 |- 4 e. CC
129	6, 120	ipcl 10573	. . . . . . 7 |- ((U e. NrmCVec /\ B e. X /\ A e. X) -> (BPA) e. CC)
130	2, 35, 4, 129	mp3an 1466	. . . . . 6 |- (BPA) e. CC
131	128, 22, 130	mul12i 6963	. . . . 5 |- (4 x. (-u_i x. (BPA))) = (-u_i x. (4 x. (BPA)))
132	124, 126, 131	3eqtr4i 2171	. . . 4 |- (4 x. (BP(_iSA))) = (4 x. (-u_i x. (BPA)))
133	6, 120	ipcl 10573	. . . . . 6 |- ((U e. NrmCVec /\ B e. X /\ (_iSA) e. X) -> (BP(_iSA)) e. CC)
134	2, 35, 72, 133	mp3an 1466	. . . . 5 |- (BP(_iSA)) e. CC
135	22, 130	mulcli 6825	. . . . 5 |- (-u_i x. (BPA)) e. CC
136		4pos 7509	. . . . . 6 |- 0 < 4
137	127, 136	gt0ne0ii 7143	. . . . 5 |- 4 =/= 0
138	134, 135, 128, 137	mulcani 7210	. . . 4 |- ((4 x. (BP(_iSA))) = (4 x. (-u_i x. (BPA))) <-> (BP(_iSA)) = (-u_i x. (BPA)))
139	132, 138	mpbi 272	. . 3 |- (BP(_iSA)) = (-u_i x. (BPA))
140	139	fveq2i 4768	. 2 |- (*` (BP(_iSA))) = (*` (-u_i x. (BPA)))
141	6, 120	ipcj 10575	. . 3 |- ((U e. NrmCVec /\ B e. X /\ (_iSA) e. X) -> (*` (BP(_iSA))) = ((_iSA)PB))
142	2, 35, 72, 141	mp3an 1466	. 2 |- (*` (BP(_iSA))) = ((_iSA)PB)
143	22, 130	cjmuli 8423	. . 3 |- (*` (-u_i x. (BPA))) = ((*` -u_i) x. (*` (BPA)))
144	58	fveq2i 4768	. . . . . 6 |- (*` (-u1 x. _i)) = (*` -u_i)
145	42, 3	cjmuli 8423	. . . . . 6 |- (*` (-u1 x. _i)) = ((*` -u1) x. (*` _i))
146	144, 145	eqtr3i 2163	. . . . 5 |- (*` -u_i) = ((*` -u1) x. (*` _i))
147		1re 6839	. . . . . . . 8 |- 1 e. RR
148	147	renegcli 7069	. . . . . . 7 |- -u1 e. RR
149	42	cjrebi 8415	. . . . . . 7 |- (-u1 e. RR <-> (*` -u1) = -u1)
150	148, 149	mpbi 272	. . . . . 6 |- (*` -u1) = -u1
151		cji 8461	. . . . . 6 |- (*` _i) = -u_i
152	150, 151	opreq12i 4991	. . . . 5 |- ((*` -u1) x. (*` _i)) = (-u1 x. -u_i)
153	18, 3	mul2negi 7084	. . . . . 6 |- (-u1 x. -u_i) = (1 x. _i)
154	3	mulid2i 6834	. . . . . 6 |- (1 x. _i) = _i
155	153, 154	eqtri 2161	. . . . 5 |- (-u1 x. -u_i) = _i
156	146, 152, 155	3eqtri 2165	. . . 4 |- (*` -u_i) = _i
157	6, 120	ipcj 10575	. . . . 5 |- ((U e. NrmCVec /\ B e. X /\ A e. X) -> (*` (BPA)) = (APB))
158	2, 35, 4, 157	mp3an 1466	. . . 4 |- (*` (BPA)) = (APB)
159	156, 158	opreq12i 4991	. . 3 |- ((*` -u_i) x. (*` (BPA))) = (_i x. (APB))
160	143, 159	eqtri 2161	. 2 |- (*` (-u_i x. (BPA))) = (_i x. (APB))
161	140, 142, 160	3eqtr3i 2169	1 |- ((_iSA)PB) = (_i x. (APB))

Syntax hints:   /\ w3a 1102   = wceq 1586   e. wcel 1588  ` cfv 4131  (class class class)co 4981  CCcc 6750  RRcr 6751  1c1 6753  _ici 6754   + caddc 6755   x. cmul 6757   - cmin 6989  -ucneg 6990  2c2 7478  4c4 7480  ^cexp 8195  *ccj 8383  NrmCVeccnv 10404  +vcpv 10405  BaseSetcba 10406  .scns 10407  normcnm 10410  .icip 10557  CPreHilcphl 10681

This theorem is referenced by:  ipasslem11 10710

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1590  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-mpt 5099  df-1st 5126  df-2nd 5127  df-iota 5219  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-en 5588  df-dom 5589  df-sdom 5590  df-undef 5725  df-riota 5729  df-sup 5888  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-sub 7009  df-neg 7011  df-div 7223  df-n 7441  df-2 7487  df-3 7488  df-4 7489  df-n0 7649  df-z 7686  df-uz 7934  df-fz 7999  df-seq1 8094  df-shft 8129  df-seqz 8151  df-exp 8196  df-sqr 8304  df-re 8385  df-im 8386  df-cj 8387  df-abs 8388  df-sum 8636  df-grpo 10182  df-gid 10183  df-ginv 10184  df-ablo 10277  df-vc 10366  df-nv 10412  df-va 10415  df-ba 10416  df-sm 10417  df-0v 10418  df-nm 10420  df-ip 10558  df-ph 10682

Copyright terms: Public domain