ipblnfi

Description: A function F generated by varying the first argument of an inner product (with its second argument a fixed vector A ) is a bounded linear functional, i.e. a bounded linear operator from the vector space to CC . (Contributed by NM, 12-Jan-2008) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ipblnfi.1	$⊢ X = BaseSet (U)$
	ipblnfi.7	$⊢ P = \cdot_{𝑖OLD} (U)$
	ipblnfi.9	$⊢ U \in {CPreHil}_{OLD}$
	ipblnfi.c	$⊢ C = ⟨⟨+ \times⟩, abs⟩$
	ipblnfi.l	$⊢ B = U BLnOp C$
	ipblnfi.f	$⊢ F = (x \in X ⟼ x P A)$
Assertion	ipblnfi	$⊢ A \in X \to F \in B$

Proof

Step	Hyp	Ref	Expression
1		ipblnfi.1	$⊢ X = BaseSet (U)$
2		ipblnfi.7	$⊢ P = \cdot_{𝑖OLD} (U)$
3		ipblnfi.9	$⊢ U \in {CPreHil}_{OLD}$
4		ipblnfi.c	$⊢ C = ⟨⟨+ \times⟩, abs⟩$
5		ipblnfi.l	$⊢ B = U BLnOp C$
6		ipblnfi.f	$⊢ F = (x \in X ⟼ x P A)$
7	3	phnvi	$⊢ U \in NrmCVec$
8	1 2	dipcl	$⊢ (U \in NrmCVec \land x \in X \land A \in X) \to x P A \in ℂ$
9	7 8	mp3an1	$⊢ (x \in X \land A \in X) \to x P A \in ℂ$
10	9	ancoms	$⊢ (A \in X \land x \in X) \to x P A \in ℂ$
11	10 6	fmptd	$⊢ A \in X \to F : X ⟶ ℂ$
12		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
13	1 12	nvscl	$⊢ (U \in NrmCVec \land y \in ℂ \land z \in X) \to y \cdot_{𝑠OLD} (U) z \in X$
14	7 13	mp3an1	$⊢ (y \in ℂ \land z \in X) \to y \cdot_{𝑠OLD} (U) z \in X$
15	14	ad2ant2lr	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to y \cdot_{𝑠OLD} (U) z \in X$
16		simprr	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to w \in X$
17		simpll	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to A \in X$
18		eqid	$⊢ +_{v} (U) = +_{v} (U)$
19	1 18 2	dipdir	$⊢ (U \in {CPreHil}_{OLD} \land (y \cdot_{𝑠OLD} (U) z \in X \land w \in X \land A \in X)) \to ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) P A = ((y \cdot_{𝑠OLD} (U) z) P A) + (w P A)$
20	3 19	mpan	$⊢ (y \cdot_{𝑠OLD} (U) z \in X \land w \in X \land A \in X) \to ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) P A = ((y \cdot_{𝑠OLD} (U) z) P A) + (w P A)$
21	15 16 17 20	syl3anc	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) P A = ((y \cdot_{𝑠OLD} (U) z) P A) + (w P A)$
22		simplr	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to y \in ℂ$
23		simprl	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to z \in X$
24	1 18 12 2 3	ipassi	$⊢ (y \in ℂ \land z \in X \land A \in X) \to (y \cdot_{𝑠OLD} (U) z) P A = y (z P A)$
25	22 23 17 24	syl3anc	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to (y \cdot_{𝑠OLD} (U) z) P A = y (z P A)$
26	25	oveq1d	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to ((y \cdot_{𝑠OLD} (U) z) P A) + (w P A) = y (z P A) + (w P A)$
27	21 26	eqtrd	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) P A = y (z P A) + (w P A)$
28	14	adantll	$⊢ ((A \in X \land y \in ℂ) \land z \in X) \to y \cdot_{𝑠OLD} (U) z \in X$
29	1 18	nvgcl	$⊢ (U \in NrmCVec \land y \cdot_{𝑠OLD} (U) z \in X \land w \in X) \to (y \cdot_{𝑠OLD} (U) z) +_{v} (U) w \in X$
30	7 29	mp3an1	$⊢ (y \cdot_{𝑠OLD} (U) z \in X \land w \in X) \to (y \cdot_{𝑠OLD} (U) z) +_{v} (U) w \in X$
31	28 30	sylan	$⊢ (((A \in X \land y \in ℂ) \land z \in X) \land w \in X) \to (y \cdot_{𝑠OLD} (U) z) +_{v} (U) w \in X$
32	31	anasss	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to (y \cdot_{𝑠OLD} (U) z) +_{v} (U) w \in X$
33		oveq1	$⊢ x = (y \cdot_{𝑠OLD} (U) z) +_{v} (U) w \to x P A = ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) P A$
34		ovex	$⊢ ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) P A \in V$
35	33 6 34	fvmpt	$⊢ (y \cdot_{𝑠OLD} (U) z) +_{v} (U) w \in X \to F ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) = ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) P A$
36	32 35	syl	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to F ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) = ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) P A$
37		oveq1	$⊢ x = z \to x P A = z P A$
38		ovex	$⊢ z P A \in V$
39	37 6 38	fvmpt	$⊢ z \in X \to F (z) = z P A$
40	39	ad2antrl	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to F (z) = z P A$
41	40	oveq2d	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to y F (z) = y (z P A)$
42		oveq1	$⊢ x = w \to x P A = w P A$
43		ovex	$⊢ w P A \in V$
44	42 6 43	fvmpt	$⊢ w \in X \to F (w) = w P A$
45	44	ad2antll	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to F (w) = w P A$
46	41 45	oveq12d	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to y F (z) + F (w) = y (z P A) + (w P A)$
47	27 36 46	3eqtr4d	$⊢ ((A \in X \land y \in ℂ) \land (z \in X \land w \in X)) \to F ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) = y F (z) + F (w)$
48	47	ralrimivva	$⊢ (A \in X \land y \in ℂ) \to \forall z \in X \forall w \in X F ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) = y F (z) + F (w)$
49	48	ralrimiva	$⊢ A \in X \to \forall y \in ℂ \forall z \in X \forall w \in X F ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) = y F (z) + F (w)$
50	4	cnnv	$⊢ C \in NrmCVec$
51	4	cnnvba	$⊢ ℂ = BaseSet (C)$
52	4	cnnvg	$⊢ + = +_{v} (C)$
53	4	cnnvs	$⊢ \times = \cdot_{𝑠OLD} (C)$
54		eqid	$⊢ U LnOp C = U LnOp C$
55	1 51 18 52 12 53 54	islno	$⊢ (U \in NrmCVec \land C \in NrmCVec) \to (F \in (U LnOp C) \leftrightarrow (F : X ⟶ ℂ \land \forall y \in ℂ \forall z \in X \forall w \in X F ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) = y F (z) + F (w)))$
56	7 50 55	mp2an	$⊢ F \in (U LnOp C) \leftrightarrow (F : X ⟶ ℂ \land \forall y \in ℂ \forall z \in X \forall w \in X F ((y \cdot_{𝑠OLD} (U) z) +_{v} (U) w) = y F (z) + F (w))$
57	11 49 56	sylanbrc	$⊢ A \in X \to F \in (U LnOp C)$
58		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
59	1 58	nvcl	$⊢ (U \in NrmCVec \land A \in X) \to {norm}_{CV} (U) (A) \in ℝ$
60	7 59	mpan	$⊢ A \in X \to {norm}_{CV} (U) (A) \in ℝ$
61	1 58 2 3	sii	$⊢ (z \in X \land A \in X) \to \|z P A\| \leq {norm}_{CV} (U) (z) {norm}_{CV} (U) (A)$
62	61	ancoms	$⊢ (A \in X \land z \in X) \to \|z P A\| \leq {norm}_{CV} (U) (z) {norm}_{CV} (U) (A)$
63	39	adantl	$⊢ (A \in X \land z \in X) \to F (z) = z P A$
64	63	fveq2d	$⊢ (A \in X \land z \in X) \to \|F (z)\| = \|z P A\|$
65	60	recnd	$⊢ A \in X \to {norm}_{CV} (U) (A) \in ℂ$
66	1 58	nvcl	$⊢ (U \in NrmCVec \land z \in X) \to {norm}_{CV} (U) (z) \in ℝ$
67	7 66	mpan	$⊢ z \in X \to {norm}_{CV} (U) (z) \in ℝ$
68	67	recnd	$⊢ z \in X \to {norm}_{CV} (U) (z) \in ℂ$
69		mulcom	$⊢ ({norm}_{CV} (U) (A) \in ℂ \land {norm}_{CV} (U) (z) \in ℂ) \to {norm}_{CV} (U) (A) {norm}_{CV} (U) (z) = {norm}_{CV} (U) (z) {norm}_{CV} (U) (A)$
70	65 68 69	syl2an	$⊢ (A \in X \land z \in X) \to {norm}_{CV} (U) (A) {norm}_{CV} (U) (z) = {norm}_{CV} (U) (z) {norm}_{CV} (U) (A)$
71	62 64 70	3brtr4d	$⊢ (A \in X \land z \in X) \to \|F (z)\| \leq {norm}_{CV} (U) (A) {norm}_{CV} (U) (z)$
72	71	ralrimiva	$⊢ A \in X \to \forall z \in X \|F (z)\| \leq {norm}_{CV} (U) (A) {norm}_{CV} (U) (z)$
73	4	cnnvnm	$⊢ abs = {norm}_{CV} (C)$
74	1 58 73 54 5 7 50	blo3i	$⊢ (F \in (U LnOp C) \land {norm}_{CV} (U) (A) \in ℝ \land \forall z \in X \|F (z)\| \leq {norm}_{CV} (U) (A) {norm}_{CV} (U) (z)) \to F \in B$
75	57 60 72 74	syl3anc	$⊢ A \in X \to F \in B$

Metamath Proof Explorer

Theorem ipblnfi

Proof