Theorem ipasslem2 8491

Description: Lemma for ipassi 8501. Show the inner product associative law for nonpositive integers.

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
ipasslem1.b	|- B e. X

Assertion

Ref	Expression
ipasslem2	|- ((N e. NN0 /\ A e. X) -> ((-uNSA)PB) = (-uN x. (APB)))

Proof of Theorem ipasslem2

Step	Hyp	Ref	Expression
1		ax1cn 5269	. . . . . . . . . . . . 13 |- 1 e. CC
2		mulneg2t 5452	. . . . . . . . . . . . 13 |- ((N e. CC /\ 1 e. CC) -> (N x. -u1) = -u(N x. 1))
3	1, 2	mpan2 696	. . . . . . . . . . . 12 |- (N e. CC -> (N x. -u1) = -u(N x. 1))
4		ax1id 5282	. . . . . . . . . . . . 13 |- (N e. CC -> (N x. 1) = N)
5	4	negeqd 5361	. . . . . . . . . . . 12 |- (N e. CC -> -u(N x. 1) = -uN)
6	3, 5	eqtr2d 1508	. . . . . . . . . . 11 |- (N e. CC -> -uN = (N x. -u1))
7	6	adantr 389	. . . . . . . . . 10 |- ((N e. CC /\ A e. X) -> -uN = (N x. -u1))
8	7	opreq1d 3975	. . . . . . . . 9 |- ((N e. CC /\ A e. X) -> (-uNSA) = ((N x. -u1)SA))
9	1	negcl 5369	. . . . . . . . . 10 |- -u1 e. CC
10		ip1i.9	. . . . . . . . . . . 12 |- U e. CPreHil
11	10	phnvi 8475	. . . . . . . . . . 11 |- U e. NrmCVec
12		ip1i.1	. . . . . . . . . . . 12 |- X = (Base` U)
13		ip1i.4	. . . . . . . . . . . 12 |- S = (.s` U)
14	12, 13	nvsass 8249	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ (N e. CC /\ -u1 e. CC /\ A e. X)) -> ((N x. -u1)SA) = (NS(-u1SA)))
15	11, 14	mpan 695	. . . . . . . . . 10 |- ((N e. CC /\ -u1 e. CC /\ A e. X) -> ((N x. -u1)SA) = (NS(-u1SA)))
16	9, 15	mp3an2 904	. . . . . . . . 9 |- ((N e. CC /\ A e. X) -> ((N x. -u1)SA) = (NS(-u1SA)))
17	8, 16	eqtrd 1507	. . . . . . . 8 |- ((N e. CC /\ A e. X) -> (-uNSA) = (NS(-u1SA)))
18		nn0cnt 6109	. . . . . . . 8 |- (N e. NN0 -> N e. CC)
19	17, 18	sylan 448	. . . . . . 7 |- ((N e. NN0 /\ A e. X) -> (-uNSA) = (NS(-u1SA)))
20	19	opreq1d 3975	. . . . . 6 |- ((N e. NN0 /\ A e. X) -> ((-uNSA)PB) = ((NS(-u1SA))PB))
21		ip1i.2	. . . . . . . 8 |- G = (+v` U)
22		ip1i.7	. . . . . . . 8 |- P = (.i` U)
23		ipasslem1.b	. . . . . . . 8 |- B e. X
24	12, 21, 13, 22, 10, 23	ipasslem1 8490	. . . . . . 7 |- ((N e. NN0 /\ (-u1SA) e. X) -> ((NS(-u1SA))PB) = (N x. ((-u1SA)PB)))
25	12, 13	nvscl 8247	. . . . . . . 8 |- ((U e. NrmCVec /\ -u1 e. CC /\ A e. X) -> (-u1SA) e. X)
26	11, 9, 25	mp3an12 906	. . . . . . 7 |- (A e. X -> (-u1SA) e. X)
27	24, 26	sylan2 451	. . . . . 6 |- ((N e. NN0 /\ A e. X) -> ((NS(-u1SA))PB) = (N x. ((-u1SA)PB)))
28	20, 27	eqtrd 1507	. . . . 5 |- ((N e. NN0 /\ A e. X) -> ((-uNSA)PB) = (N x. ((-u1SA)PB)))
29	28	opreq2d 3976	. . . 4 |- ((N e. NN0 /\ A e. X) -> ((-uN x. (APB)) - ((-uNSA)PB)) = ((-uN x. (APB)) - (N x. ((-u1SA)PB))))
30		negsubt 5382	. . . . 5 |- (((-uN x. (APB)) e. CC /\ (N x. ((-u1SA)PB)) e. CC) -> ((-uN x. (APB)) + -u(N x. ((-u1SA)PB))) = ((-uN x. (APB)) - (N x. ((-u1SA)PB))))
31		axmulcl 5273	. . . . . 6 |- ((-uN e. CC /\ (APB) e. CC) -> (-uN x. (APB)) e. CC)
32		negclt 5368	. . . . . . 7 |- (N e. CC -> -uN e. CC)
33	18, 32	syl 10	. . . . . 6 |- (N e. NN0 -> -uN e. CC)
34	12, 22	ipcl 8365	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) e. CC)
35	11, 23, 34	mp3an13 907	. . . . . 6 |- (A e. X -> (APB) e. CC)
36	31, 33, 35	syl2an 454	. . . . 5 |- ((N e. NN0 /\ A e. X) -> (-uN x. (APB)) e. CC)
37		axmulcl 5273	. . . . . 6 |- ((N e. CC /\ ((-u1SA)PB) e. CC) -> (N x. ((-u1SA)PB)) e. CC)
38	12, 22	ipcl 8365	. . . . . . . 8 |- ((U e. NrmCVec /\ (-u1SA) e. X /\ B e. X) -> ((-u1SA)PB) e. CC)
39	11, 23, 38	mp3an13 907	. . . . . . 7 |- ((-u1SA) e. X -> ((-u1SA)PB) e. CC)
40	26, 39	syl 10	. . . . . 6 |- (A e. X -> ((-u1SA)PB) e. CC)
41	37, 18, 40	syl2an 454	. . . . 5 |- ((N e. NN0 /\ A e. X) -> (N x. ((-u1SA)PB)) e. CC)
42	30, 36, 41	sylanc 471	. . . 4 |- ((N e. NN0 /\ A e. X) -> ((-uN x. (APB)) + -u(N x. ((-u1SA)PB))) = ((-uN x. (APB)) - (N x. ((-u1SA)PB))))
43		axdistr 5279	. . . . . 6 |- ((-uN e. CC /\ (APB) e. CC /\ ((-u1SA)PB) e. CC) -> (-uN x. ((APB) + ((-u1SA)PB))) = ((-uN x. (APB)) + (-uN x. ((-u1SA)PB))))
44	33	adantr 389	. . . . . 6 |- ((N e. NN0 /\ A e. X) -> -uN e. CC)
45	35	adantl 388	. . . . . 6 |- ((N e. NN0 /\ A e. X) -> (APB) e. CC)
46	40	adantl 388	. . . . . 6 |- ((N e. NN0 /\ A e. X) -> ((-u1SA)PB) e. CC)
47	43, 44, 45, 46	syl3anc 858	. . . . 5 |- ((N e. NN0 /\ A e. X) -> (-uN x. ((APB) + ((-u1SA)PB))) = ((-uN x. (APB)) + (-uN x. ((-u1SA)PB))))
48	12, 21, 13, 22, 10	ipdiri 8489	. . . . . . . . . 10 |- ((A e. X /\ (-u1SA) e. X /\ B e. X) -> ((AG(-u1SA))PB) = ((APB) + ((-u1SA)PB)))
49	23, 48	mp3an3 905	. . . . . . . . 9 |- ((A e. X /\ (-u1SA) e. X) -> ((AG(-u1SA))PB) = ((APB) + ((-u1SA)PB)))
50	26, 49	mpdan 704	. . . . . . . 8 |- (A e. X -> ((AG(-u1SA))PB) = ((APB) + ((-u1SA)PB)))
51		eqid 1475	. . . . . . . . . . . 12 |- (0v` U) = (0v` U)
52	12, 21, 13, 51	nvrinv 8273	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ A e. X) -> (AG(-u1SA)) = (0v` U))
53	11, 52	mpan 695	. . . . . . . . . 10 |- (A e. X -> (AG(-u1SA)) = (0v` U))
54	53	opreq1d 3975	. . . . . . . . 9 |- (A e. X -> ((AG(-u1SA))PB) = ((0v` U)PB))
55	12, 51, 22	ip0l 8371	. . . . . . . . . 10 |- ((U e. NrmCVec /\ B e. X) -> ((0v` U)PB) = 0)
56	11, 23, 55	mp2an 697	. . . . . . . . 9 |- ((0v` U)PB) = 0
57	54, 56	syl6eq 1523	. . . . . . . 8 |- (A e. X -> ((AG(-u1SA))PB) = 0)
58	50, 57	eqtr3d 1509	. . . . . . 7 |- (A e. X -> ((APB) + ((-u1SA)PB)) = 0)
59	58	opreq2d 3976	. . . . . 6 |- (A e. X -> (-uN x. ((APB) + ((-u1SA)PB))) = (-uN x. 0))
60		mul01t 5443	. . . . . . 7 |- (-uN e. CC -> (-uN x. 0) = 0)
61	33, 60	syl 10	. . . . . 6 |- (N e. NN0 -> (-uN x. 0) = 0)
62	59, 61	sylan9eqr 1529	. . . . 5 |- ((N e. NN0 /\ A e. X) -> (-uN x. ((APB) + ((-u1SA)PB))) = 0)
63		mulneg1t 5451	. . . . . . 7 |- ((N e. CC /\ ((-u1SA)PB) e. CC) -> (-uN x. ((-u1SA)PB)) = -u(N x. ((-u1SA)PB)))
64	63, 18, 40	syl2an 454	. . . . . 6 |- ((N e. NN0 /\ A e. X) -> (-uN x. ((-u1SA)PB)) = -u(N x. ((-u1SA)PB)))
65	64	opreq2d 3976	. . . . 5 |- ((N e. NN0 /\ A e. X) -> ((-uN x. (APB)) + (-uN x. ((-u1SA)PB))) = ((-uN x. (APB)) + -u(N x. ((-u1SA)PB))))
66	47, 62, 65	3eqtr3rd 1516	. . . 4 |- ((N e. NN0 /\ A e. X) -> ((-uN x. (APB)) + -u(N x. ((-u1SA)PB))) = 0)
67	29, 42, 66	3eqtr2d 1513	. . 3 |-