Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem ipval2 8291

Description: Expansion of the inner product value ipval 8287. Warning: The HTML proof page is 0.5MB in size.

Hypotheses

Ref	Expression
ipfval.1	Base
ipfval.2
ipfval.4
ipfval.6
ipfval.7

Assertion

Ref	Expression
ipval2	NrmCVec

---

Proof of Theorem ipval2

Step	Hyp	Ref	Expression
1		ipfval.1	. . 3 Base
2		ipfval.2	. . 3
3		ipfval.4	. . 3
4		ipfval.6	. . 3
5		ipfval.7	. . 3
6	1, 2, 3, 4, 5	ipval 8287	. 2 NrmCVec
7		negsubt 5354	. . . . . . 7
8		subclt 5339	. . . . . . . 8
9		axicn 5242	. . . . . . . . . 10
10	1, 2, 3, 4, 5	ipval2lem4 8290	. . . . . . . . . 10 NrmCVec
11	9, 10	mpan2 694	. . . . . . . . 9 NrmCVec
12		axmulcl 5245	. . . . . . . . . 10
13	9, 12	mpan 693	. . . . . . . . 9
14	11, 13	syl 10	. . . . . . . 8 NrmCVec
15		ax1cn 5241	. . . . . . . . . 10
16	15	negcl 5341	. . . . . . . . 9
17	1, 2, 3, 4, 5	ipval2lem4 8290	. . . . . . . . 9 NrmCVec
18	16, 17	mpan2 694	. . . . . . . 8 NrmCVec
19	8, 14, 18	sylanc 471	. . . . . . 7 NrmCVec
20	9	negcl 5341	. . . . . . . . 9
21	1, 2, 3, 4, 5	ipval2lem4 8290	. . . . . . . . 9 NrmCVec
22	20, 21	mpan2 694	. . . . . . . 8 NrmCVec
23		axmulcl 5245	. . . . . . . . 9
24	9, 23	mpan 693	. . . . . . . 8
25	22, 24	syl 10	. . . . . . 7 NrmCVec
26	7, 19, 25	sylanc 471	. . . . . 6 NrmCVec
27		mulm1t 5443	. . . . . . . . . 10
28	18, 27	syl 10	. . . . . . . . 9 NrmCVec
29	28	opreq2d 3961	. . . . . . . 8 NrmCVec
30		negsubt 5354	. . . . . . . . 9
31	30, 14, 18	sylanc 471	. . . . . . . 8 NrmCVec
32	29, 31	eqtrd 1499	. . . . . . 7 NrmCVec
33		mulneg1t 5423	. . . . . . . . 9
34	9, 33	mpan 693	. . . . . . . 8
35	22, 34	syl 10	. . . . . . 7 NrmCVec
36	32, 35	opreq12d 3963	. . . . . 6 NrmCVec