Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem ipblnfi 8447

Description: A function generated by varying the first argument of an inner product (with its second argument a fixed vector ) is a bounded linear functional, i.e. a bounded linear operator from the vector space to .

Hypotheses

Ref	Expression
ipblnfi.1	Base
ipblnfi.7
ipblnfi.9	CPreHil
ipblnfi.c
ipblnfi.l	BLnOp
ipblnfi.f

Assertion

Ref	Expression
ipblnfi

Distinct variable groups:   ,,   ,,   ,,   ,,

---

Proof of Theorem ipblnfi

Step	Hyp	Ref	Expression
1		ipblnfi.1	. . 3 Base
2		eqid 1468	. . 3
3		ipblnfi.c	. . . 4
4	3	cnnvnm 8250	. . 3
5		eqid 1468	. . 3 LnOp LnOp
6		ipblnfi.l	. . 3 BLnOp
7		ipblnfi.9	. . . 4 CPreHil
8	7	phnvi 8406	. . 3 NrmCVec
9	3	cnnv 8245	. . 3 NrmCVec
10	1, 2, 4, 5, 6, 8, 9	blo3i 8393	. 2 LnOp
11		ipblnfi.7	. . . . . . . . 9
12	1, 11	ipcl 8299	. . . . . . . 8 NrmCVec
13	8, 12	mp3an1 900	. . . . . . 7
14	13	ancoms 436	. . . . . 6
15	14	r19.21aiva 1706	. . . . 5
16		ipblnfi.f	. . . . . 6
17	16	fopab2 3808	. . . . 5
18	15, 17	sylib 198	. . . 4
19		eqid 1468	. . . . . . . . . . . . . 14
20	1, 19, 11	ipdir 8433	. . . . . . . . . . . . 13 CPreHil
21	7, 20	mpan 693	. . . . . . . . . . . 12
22		eqid 1468	. . . . . . . . . . . . . 14
23	1, 22	nvscl 8187	. . . . . . . . . . . . 13 NrmCVec
24	8, 23	mp3an1 900	. . . . . . . . . . . 12
25	21, 24	syl3an2 858	. . . . . . . . . . 11
26	25	3expa 831	. . . . . . . . . 10
27	1, 19	nvgcl 8179	. . . . . . . . . . . . . 14 NrmCVec
28	8, 27	mp3an1 900	. . . . . . . . . . . . 13
29	28, 24	sylan2 451	. . . . . . . . . . . 12
30		opreq1 3953	. . . . . . . . . . . . 13
31		oprex 3968	. . . . . . . . . . . . 13
32	30, 16, 31	fvopab4 3765	. . . . . . . . . . . 12
33	29, 32	syl 10	. . . . . . . . . . 11
34	33	adantr 389	. . . . . . . . . 10
35		opreq1 3953	. . . . . . . . . . . . 13
36		oprex 3968	. . . . . . . . . . . . 13
37	35, 16, 36	fvopab4 3765	. . . . . . . . . . . 12
38	37	ad2antrr 404	. . . . . . . . . . 11
39		opreq1 3953	. . . . . . . . . . . . . . . 16
40		oprex 3968	. . . . . . . . . . . . . . . 16
41	39, 16, 40	fvopab4 3765	. . . . . . . . . . . . . . 15
42	41	opreq2d 3961	. . . . . . . . . . . . . 14
43	42	adantl 388	. . . . . . . . . . . . 13
44	43	ad2antlr 405	. . . . . . . . . . . 12
45	1, 19, 22, 11, 7	ipassi 8432	. . . . . . . . . . . . . 14
46	45	3expa 831	. . . . . . . . . . . . 13
47	46	adantll 392	. . . . . . . . . . . 12
48	44, 47	eqtr4d 1502	. . . . . . . . . . 11
49	38, 48	opreq12d 3963	. . . . . . . . . 10
50	26, 34, 49	3eqtr4d 1509	. . . . . . . . 9
51	50	exp42 383	. . . . . . . 8
52	51	com4r 41	. . . . . . 7
53	52	imp3a 361	. . . . . 6
54	53	r19.21adv 1710	. . . . 5
55	54	r19.21aivv 1712	. . . 4
56	18, 55	jca 288	. . 3
57	3	cnnvba 8247	. . . . 5 Base
58	3	cnnvg 8246	. . . . 5
59	3	cnnvs 8249	. . . . 5