Theorem ipasslem1 8490

Description: Lemma for ipassi 8501. Show the inner product associative law for nonnegative 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
ipasslem1	|- ((N e. NN0 /\ A e. X) -> ((NSA)PB) = (N x. (APB)))

Proof of Theorem ipasslem1

Step	Hyp	Ref	Expression
1		ip1i.9	. . . . . . . . . . . 12 |- U e. CPreHil
2	1	phnvi 8475	. . . . . . . . . . 11 |- U e. NrmCVec
3		ip1i.1	. . . . . . . . . . . 12 |- X = (Base` U)
4		ip1i.4	. . . . . . . . . . . 12 |- S = (.s` U)
5	3, 4	nvscl 8247	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ k e. CC /\ A e. X) -> (kSA) e. X)
6	2, 5	mp3an1 903	. . . . . . . . . 10 |- ((k e. CC /\ A e. X) -> (kSA) e. X)
7		nn0cnt 6109	. . . . . . . . . 10 |- (k e. NN0 -> k e. CC)
8	6, 7	sylan 448	. . . . . . . . 9 |- ((k e. NN0 /\ A e. X) -> (kSA) e. X)
9		ipasslem1.b	. . . . . . . . . 10 |- B e. X
10		ip1i.2	. . . . . . . . . . 11 |- G = (+v` U)
11		ip1i.7	. . . . . . . . . . 11 |- P = (.i` U)
12	3, 10, 4, 11, 1	ipdiri 8489	. . . . . . . . . 10 |- (((kSA) e. X /\ A e. X /\ B e. X) -> (((kSA)GA)PB) = (((kSA)PB) + (APB)))
13	9, 12	mp3an3 905	. . . . . . . . 9 |- (((kSA) e. X /\ A e. X) -> (((kSA)GA)PB) = (((kSA)PB) + (APB)))
14	8, 13	sylancom 475	. . . . . . . 8 |- ((k e. NN0 /\ A e. X) -> (((kSA)GA)PB) = (((kSA)PB) + (APB)))
15		ax1cn 5269	. . . . . . . . . . . 12 |- 1 e. CC
16	3, 10, 4	nvdir 8252	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ (k e. CC /\ 1 e. CC /\ A e. X)) -> ((k + 1)SA) = ((kSA)G(1SA)))
17	2, 16	mpan 695	. . . . . . . . . . . 12 |- ((k e. CC /\ 1 e. CC /\ A e. X) -> ((k + 1)SA) = ((kSA)G(1SA)))
18	15, 17	mp3an2 904	. . . . . . . . . . 11 |- ((k e. CC /\ A e. X) -> ((k + 1)SA) = ((kSA)G(1SA)))
19	18, 7	sylan 448	. . . . . . . . . 10 |- ((k e. NN0 /\ A e. X) -> ((k + 1)SA) = ((kSA)G(1SA)))
20	3, 4	nvsid 8248	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ A e. X) -> (1SA) = A)
21	2, 20	mpan 695	. . . . . . . . . . . 12 |- (A e. X -> (1SA) = A)
22	21	adantl 388	. . . . . . . . . . 11 |- ((k e. NN0 /\ A e. X) -> (1SA) = A)
23	22	opreq2d 3976	. . . . . . . . . 10 |- ((k e. NN0 /\ A e. X) -> ((kSA)G(1SA)) = ((kSA)GA))
24	19, 23	eqtrd 1507	. . . . . . . . 9 |- ((k e. NN0 /\ A e. X) -> ((k + 1)SA) = ((kSA)GA))
25	24	opreq1d 3975	. . . . . . . 8 |- ((k e. NN0 /\ A e. X) -> (((k + 1)SA)PB) = (((kSA)GA)PB))
26	3, 11	ipcl 8365	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) e. CC)
27	2, 9, 26	mp3an13 907	. . . . . . . . . . 11 |- (A e. X -> (APB) e. CC)
28		mulid2t 5417	. . . . . . . . . . 11 |- ((APB) e. CC -> (1 x. (APB)) = (APB))
29	27, 28	syl 10	. . . . . . . . . 10 |- (A e. X -> (1 x. (APB)) = (APB))
30	29	adantl 388	. . . . . . . . 9 |- ((k e. NN0 /\ A e. X) -> (1 x. (APB)) = (APB))
31	30	opreq2d 3976	. . . . . . . 8 |- ((k e. NN0 /\ A e. X) -> (((kSA)PB) + (1 x. (APB))) = (((kSA)PB) + (APB)))
32	14, 25, 31	3eqtr4d 1517	. . . . . . 7 |- ((k e. NN0 /\ A e. X) -> (((k + 1)SA)PB) = (((kSA)PB) + (1 x. (APB))))
33		opreq1 3968	. . . . . . 7 |- (((kSA)PB) = (k x. (APB)) -> (((kSA)PB) + (1 x. (APB))) = ((k x. (APB)) + (1 x. (APB))))
34	32, 33	sylan9eq 1527	. . . . . 6 |- (((k e. NN0 /\ A e. X) /\ ((kSA)PB) = (k x. (APB))) -> (((k + 1)SA)PB) = ((k x. (APB)) + (1 x. (APB))))
35		adddirt 5319	. . . . . . . . 9 |- ((k e. CC /\ 1 e. CC /\ (APB) e. CC) -> ((k + 1) x. (APB)) = ((k x. (APB)) + (1 x. (APB))))
36	15, 35	mp3an2 904	. . . . . . . 8 |- ((k e. CC /\ (APB) e. CC) -> ((k + 1) x. (APB)) = ((k x. (APB)) + (1 x. (APB))))
37	36, 7, 27	syl2an 454	. . . . . . 7 |- ((k e. NN0 /\ A e. X) -> ((k + 1) x. (APB)) = ((k x. (APB)) + (1 x. (APB))))
38	37	adantr 389	. . . . . 6 |- (((k e. NN0 /\ A e. X) /\ ((kSA)PB) = (k x. (APB))) -> ((k + 1) x. (APB)) = ((k x. (APB)) + (1 x. (APB))))
39	34, 38	eqtr4d 1510	. . . . 5 |- (((k e. NN0 /\ A e. X) /\ ((kSA)PB) = (k x. (APB))) -> (((k + 1)SA)PB) = ((k + 1) x. (APB)))
40	39	exp31 376	. . . 4 |- (k e. NN0 -> (A e. X -> (((kSA)PB) = (k x. (APB)) -> (((k + 1)SA)PB) = ((k + 1) x. (APB)))))
41	40	a2d 13	. . 3 |- (k e. NN0 -> ((A e. X -> ((kSA)PB) = (k x. (APB))) -> (A e. X -> (((k + 1)SA)PB) = ((k + 1) x. (APB)))))
42		eqid 1475	. . . . . 6 |- (0v` U) = (0v` U)
43	3, 42, 11	ip0l 8371	. . . . 5 |- ((U e. NrmCVec /\ B e. X) -> ((0v` U)PB) = 0)
44	2, 9, 43	mp2an 697	. . . 4 |- ((0v` U)PB) = 0
45	3, 4, 42	nv0 8258	. . . . . 6 |- ((U e. NrmCVec /\ A e. X) -> (0SA) = (0v` U))
46	2, 45	mpan 695	. . . . 5 |- (A e. X -> (0SA) = (0v` U))
47	46	opreq1d 3975	. . . 4 |- (A e. X -> ((0SA)PB) = ((0v` U)PB))
48		mul02t 5444	. . . . 5 |- ((APB) e. CC -> (0 x. (APB)) = 0)
49	27, 48	syl 10	. . . 4 |- (A e. X -> (0 x. (APB)) = 0)
50	44, 47, 49	3eqtr4a 1532	. . 3 |- (A e. X -> ((0SA)PB) = (0 x. (APB)))
51		opreq1 3968	. . . . . 6 |- (j = 0 -> (jSA) = (0SA))
52	51	opreq1d 3975	. . . . 5 |- (j = 0 -> ((jSA)PB) = ((0SA)PB))
53		opreq1 3968	. . . . 5 |- (j = 0 -> (j x. (APB)) = (0 x. (APB)))
54	52, 53	eqeq12d 1489	. . . 4 |- (j = 0 -> (((jSA)PB) = (j x. (APB)) <-> ((0SA)PB) = (0 x. (APB))))
55	54	imbi2d 612	. . 3 |- (j = 0 -> ((A e. X -> ((jSA)PB) = (j x. (APB))) <-> (A e. X -> ((0SA)PB) = (0 x. (APB)))))
56		opreq1 3968	. . . . . 6 |- (j = k -> (jSA) = (kSA))
57	56	opreq1d 3975	. . . . 5 |- (j = k -> ((jSA)PB) = ((kSA)PB))
58		opreq1 3968	. . . . 5 |- (j = k -> (j x. (APB)) = (k x. (APB)))
59	57, 58	eqeq12d 1489	. . . 4 |- (j = k -> (((jSA)PB) = (j x. (APB)) <-> ((kSA)PB) = (k x. (APB))))
60	59	imbi2d 612	. . 3 |- (j = k -> ((A e. X -> ((jSA)PB) = (j x. (APB))) <-> (A e. X -> ((kSA)PB) = (k x. (APB)))))
61		opreq1 3968	. . . . . 6 |- (j = (k + 1) -> (jSA) = ((k + 1)SA))
62	61	opreq1d 3975	. . . . 5 |- (j = (k + 1) -> ((jSA)PB) = (((k + 1)SA)PB))
63		opreq1 3968	. . . . 5 |- (j = (k + 1) -> (j x. (APB)) =