Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem ipasslem2 8422

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

Hypotheses

Ref	Expression
ip1i.1	Base
ip1i.2
ip1i.4
ip1i.7
ip1i.9	CPreHil
ipasslem1.b

Assertion

Ref	Expression
ipasslem2

---

Proof of Theorem ipasslem2

Step	Hyp	Ref	Expression
1		ax1cn 5241	. . . . . . . . . . . . 13
2		mulneg2t 5424	. . . . . . . . . . . . 13
3	1, 2	mpan2 694	. . . . . . . . . . . 12
4		ax1id 5254	. . . . . . . . . . . . 13
5	4	negeqd 5333	. . . . . . . . . . . 12
6	3, 5	eqtr2d 1500	. . . . . . . . . . 11
7	6	adantr 389	. . . . . . . . . 10
8	7	opreq1d 3960	. . . . . . . . 9
9	1	negcl 5341	. . . . . . . . . 10
10		ip1i.9	. . . . . . . . . . . 12 CPreHil
11	10	phnvi 8406	. . . . . . . . . . 11 NrmCVec
12		ip1i.1	. . . . . . . . . . . 12 Base
13		ip1i.4	. . . . . . . . . . . 12
14	12, 13	nvsass 8189	. . . . . . . . . . 11 NrmCVec
15	11, 14	mpan 693	. . . . . . . . . 10
16	9, 15	mp3an2 901	. . . . . . . . 9
17	8, 16	eqtrd 1499	. . . . . . . 8
18		nn0cnt 6056	. . . . . . . 8
19	17, 18	sylan 448	. . . . . . 7
20	19	opreq1d 3960	. . . . . 6
21		ip1i.2	. . . . . . . 8
22		ip1i.7	. . . . . . . 8
23		ipasslem1.b	. . . . . . . 8
24	12, 21, 13, 22, 10, 23	ipasslem1 8421	. . . . . . 7
25	12, 13	nvscl 8187	. . . . . . . 8 NrmCVec
26	11, 9, 25	mp3an12 903	. . . . . . 7
27	24, 26	sylan2 451	. . . . . 6
28	20, 27	eqtrd 1499	. . . . 5
29	28	opreq2d 3961	. . . 4
30		negsubt 5354	. . . . 5
31		axmulcl 5245	. . . . . 6
32		negclt 5340	. . . . . . 7
33	18, 32	syl 10	. . . . . 6
34	12, 22	ipcl 8299	. . . . . . 7 NrmCVec
35	11, 23, 34	mp3an13 904	. . . . . 6
36	31, 33, 35	syl2an 454	. . . . 5
37		axmulcl 5245	. . . . . 6
38	12, 22	ipcl 8299	. . . . . . . 8 NrmCVec
39	11, 23, 38	mp3an13 904	. . . . . . 7
40	26, 39	syl 10	. . . . . 6
41	37, 18, 40	syl2an 454	. . . . 5
42	30, 36, 41	sylanc 471	. . . 4
43		axdistr 5251	. . . . . 6
44	33	adantr 389	. . . . . 6
45	35	adantl 388	. . . . . 6
46	40	adantl 388	. . . . . 6
47	43, 44, 45, 46	syl3anc 856	. . . . 5
48	12, 21, 13, 22, 10	ipdiri 8420	. . . . . . . . . 10
49	23, 48	mp3an3 902	. . . . . . . . 9
50	26, 49	mpdan 702	. . . . . . . 8
51		eqid 1468	. . . . . . . . . . . 12
52	12, 21, 13, 51	nvrinv 8213	. . . . . . . . . . 11 NrmCVec
53	11, 52	mpan 693	. . . . . . . . . 10
54	53	opreq1d 3960	. . . . . . . . 9
55	12, 51, 22	ip0l 8305	. . . . . . . . . 10 NrmCVec
56	11, 23, 55	mp2an 695	. . . . . . . . 9
57	54, 56	syl6eq 1515	. . . . . . . 8
58	50, 57	eqtr3d 1501	. . . . . . 7
59	58	opreq2d 3961	. . . . . 6
60		mul01t 5415	. . . . . . 7
61	33, 60	syl 10	. . . . . 6
62	59, 61	sylan9eqr 1521	. . . . 5
63		mulneg1t 5423	. . . . . . 7
64	63, 18, 40	syl2an 454	. . . . . 6
65	64	opreq2d 3961	. . . . 5
66	47, 62, 65	3eqtr3rd 1508	. . . 4
67	29, 42, 66	3eqtr2d 1505	. . 3