Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem 4ipval2 8292

Description: Four times the inner product value ipval3 8293, useful for simplifying certain proofs.

Hypotheses

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

Assertion

Ref	Expression
4ipval2	NrmCVec

---

Proof of Theorem 4ipval2

Step	Hyp	Ref	Expression
1		ipfval.1	. . . 4 Base
2		ipfval.2	. . . 4
3		ipfval.4	. . . 4
4		ipfval.6	. . . 4
5		ipfval.7	. . . 4
6	1, 2, 3, 4, 5	ipval2 8291	. . 3 NrmCVec
7	6	opreq2d 3961	. 2 NrmCVec
8		axaddcl 5243	. . . 4
9		subclt 5339	. . . . 5
10	1, 4	nvcl 8227	. . . . . . . 8 NrmCVec
11		3simp1 786	. . . . . . . 8 NrmCVec NrmCVec
12	1, 2	nvgcl 8179	. . . . . . . 8 NrmCVec
13	10, 11, 12	sylanc 471	. . . . . . 7 NrmCVec
14	13	recnd 5287	. . . . . 6 NrmCVec
15		sqclt 6542	. . . . . 6
16	14, 15	syl 10	. . . . 5 NrmCVec
17	1, 4	nvcl 8227	. . . . . . . 8 NrmCVec
18	1, 2	nvgcl 8179	. . . . . . . . 9 NrmCVec
19		ax1cn 5241	. . . . . . . . . . . 12
20	19	negcl 5341	. . . . . . . . . . 11
21	1, 3	nvscl 8187	. . . . . . . . . . 11 NrmCVec
22	20, 21	mp3an2 901	. . . . . . . . . 10 NrmCVec
23	22	3adant2 796	. . . . . . . . 9 NrmCVec
24	18, 23	syl3dan3 868	. . . . . . . 8 NrmCVec
25	17, 11, 24	sylanc 471	. . . . . . 7 NrmCVec
26	25	recnd 5287	. . . . . 6 NrmCVec
27		sqclt 6542	. . . . . 6
28	26, 27	syl 10	. . . . 5 NrmCVec
29	9, 16, 28	sylanc 471	. . . 4 NrmCVec
30		subclt 5339	. . . . . 6
31	1, 4	nvcl 8227	. . . . . . . . 9 NrmCVec
32	1, 2	nvgcl 8179	. . . . . . . . . 10 NrmCVec
33		axicn 5242	. . . . . . . . . . . 12
34	1, 3	nvscl 8187	. . . . . . . . . . . 12 NrmCVec
35	33, 34	mp3an2 901	. . . . . . . . . . 11 NrmCVec
36	35	3adant2 796	. . . . . . . . . 10 NrmCVec
37	32, 36	syl3dan3 868	. . . . . . . . 9 NrmCVec
38	31, 11, 37	sylanc 471	. . . . . . . 8 NrmCVec
39	38	recnd 5287	. . . . . . 7 NrmCVec
40		sqclt 6542	. . . . . . 7
41	39, 40	syl 10	. . . . . 6 NrmCVec
42	1, 4	nvcl 8227	. . . . . . . . 9 NrmCVec
43	1, 2	nvgcl 8179	. . . . . . . . . 10 NrmCVec
44	33	negcl 5341	. . . . . . . . . . . 12
45	1, 3	nvscl 8187	. . . . . . . . . . . 12 NrmCVec
46	44, 45	mp3an2 901	. . . . . . . . . . 11 NrmCVec
47	46	3adant2 796	. . . . . . . . . 10 NrmCVec
48	43, 47	syl3dan3 868	. . . . . . . . 9 NrmCVec
49	42, 11, 48	sylanc 471	. . . . . . . 8 NrmCVec
50	49	recnd 5287	. . . . . . 7 NrmCVec
51		sqclt 6542	. . . . . . 7
52	50, 51	syl 10	. . . . . 6 NrmCVec
53	30, 41, 52	sylanc 471	. . . . 5 NrmCVec
54		axmulcl 5245	. . . . . 6
55	33, 54	mpan 693	. . . . 5