Theorem 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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	ipblnfi.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
	ipblnfi.9	⊢ 𝑈 ∈ CPreHilOLD
	ipblnfi.c	⊢ 𝐶 = ⟨ ⟨ + , · ⟩ , abs ⟩
	ipblnfi.l	⊢ 𝐵 = ( 𝑈 BLnOp 𝐶 )
	ipblnfi.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝑃 𝐴 ) )
Assertion	ipblnfi	⊢ ( 𝐴 ∈ 𝑋 → 𝐹 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ipblnfi.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		ipblnfi.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
3		ipblnfi.9	⊢ 𝑈 ∈ CPreHilOLD
4		ipblnfi.c	⊢ 𝐶 = ⟨ ⟨ + , · ⟩ , abs ⟩
5		ipblnfi.l	⊢ 𝐵 = ( 𝑈 BLnOp 𝐶 )
6		ipblnfi.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝑃 𝐴 ) )
7	3	phnvi	⊢ 𝑈 ∈ NrmCVec
8	1 2	dipcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 𝑃 𝐴 ) ∈ ℂ )
9	7 8	mp3an1	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 𝑃 𝐴 ) ∈ ℂ )
10	9	ancoms	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝑃 𝐴 ) ∈ ℂ )
11	10 6	fmptd	⊢ ( 𝐴 ∈ 𝑋 → 𝐹 : 𝑋 ⟶ ℂ )
12		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
13	1 12	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 )
14	7 13	mp3an1	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 )
15	14	ad2ant2lr	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 )
16		simprr	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑤 ∈ 𝑋 )
17		simpll	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
18		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
19	1 18 2	dipdir	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) = ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) 𝑃 𝐴 ) + ( 𝑤 𝑃 𝐴 ) ) )
20	3 19	mpan	⊢ ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) = ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) 𝑃 𝐴 ) + ( 𝑤 𝑃 𝐴 ) ) )
21	15 16 17 20	syl3anc	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) = ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) 𝑃 𝐴 ) + ( 𝑤 𝑃 𝐴 ) ) )
22		simplr	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑦 ∈ ℂ )
23		simprl	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
24	1 18 12 2 3	ipassi	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) 𝑃 𝐴 ) = ( 𝑦 · ( 𝑧 𝑃 𝐴 ) ) )
25	22 23 17 24	syl3anc	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) 𝑃 𝐴 ) = ( 𝑦 · ( 𝑧 𝑃 𝐴 ) ) )
26	25	oveq1d	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) 𝑃 𝐴 ) + ( 𝑤 𝑃 𝐴 ) ) = ( ( 𝑦 · ( 𝑧 𝑃 𝐴 ) ) + ( 𝑤 𝑃 𝐴 ) ) )
27	21 26	eqtrd	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) = ( ( 𝑦 · ( 𝑧 𝑃 𝐴 ) ) + ( 𝑤 𝑃 𝐴 ) ) )
28	14	adantll	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 )
29	1 18	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 )
30	7 29	mp3an1	⊢ ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 )
31	28 30	sylan	⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 )
32	31	anasss	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 )
33		oveq1	⊢ ( 𝑥 = ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) → ( 𝑥 𝑃 𝐴 ) = ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) )
34		ovex	⊢ ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) ∈ V
35	33 6 34	fvmpt	⊢ ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 → ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) )
36	32 35	syl	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) )
37		oveq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝑃 𝐴 ) = ( 𝑧 𝑃 𝐴 ) )
38		ovex	⊢ ( 𝑧 𝑃 𝐴 ) ∈ V
39	37 6 38	fvmpt	⊢ ( 𝑧 ∈ 𝑋 → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝑃 𝐴 ) )
40	39	ad2antrl	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝑃 𝐴 ) )
41	40	oveq2d	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) = ( 𝑦 · ( 𝑧 𝑃 𝐴 ) ) )
42		oveq1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 𝑃 𝐴 ) = ( 𝑤 𝑃 𝐴 ) )
43		ovex	⊢ ( 𝑤 𝑃 𝐴 ) ∈ V
44	42 6 43	fvmpt	⊢ ( 𝑤 ∈ 𝑋 → ( 𝐹 ‘ 𝑤 ) = ( 𝑤 𝑃 𝐴 ) )
45	44	ad2antll	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝑤 𝑃 𝐴 ) )
46	41 45	oveq12d	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) + ( 𝐹 ‘ 𝑤 ) ) = ( ( 𝑦 · ( 𝑧 𝑃 𝐴 ) ) + ( 𝑤 𝑃 𝐴 ) ) )
47	27 36 46	3eqtr4d	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) + ( 𝐹 ‘ 𝑤 ) ) )
48	47	ralrimivva	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) + ( 𝐹 ‘ 𝑤 ) ) )
49	48	ralrimiva	⊢ ( 𝐴 ∈ 𝑋 → ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) + ( 𝐹 ‘ 𝑤 ) ) )
50	4	cnnv	⊢ 𝐶 ∈ NrmCVec
51	4	cnnvba	⊢ ℂ = ( BaseSet ‘ 𝐶 )
52	4	cnnvg	⊢ + = ( +𝑣 ‘ 𝐶 )
53	4	cnnvs	⊢ · = ( ·𝑠OLD ‘ 𝐶 )
54		eqid	⊢ ( 𝑈 LnOp 𝐶 ) = ( 𝑈 LnOp 𝐶 )
55	1 51 18 52 12 53 54	islno	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐶 ∈ NrmCVec ) → ( 𝐹 ∈ ( 𝑈 LnOp 𝐶 ) ↔ ( 𝐹 : 𝑋 ⟶ ℂ ∧ ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) + ( 𝐹 ‘ 𝑤 ) ) ) ) )
56	7 50 55	mp2an	⊢ ( 𝐹 ∈ ( 𝑈 LnOp 𝐶 ) ↔ ( 𝐹 : 𝑋 ⟶ ℂ ∧ ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) + ( 𝐹 ‘ 𝑤 ) ) ) )
57	11 49 56	sylanbrc	⊢ ( 𝐴 ∈ 𝑋 → 𝐹 ∈ ( 𝑈 LnOp 𝐶 ) )
58		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
59	1 58	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ∈ ℝ )
60	7 59	mpan	⊢ ( 𝐴 ∈ 𝑋 → ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ∈ ℝ )
61	1 58 2 3	sii	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( abs ‘ ( 𝑧 𝑃 𝐴 ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ) )
62	61	ancoms	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( abs ‘ ( 𝑧 𝑃 𝐴 ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ) )
63	39	adantl	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝑃 𝐴 ) )
64	63	fveq2d	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) = ( abs ‘ ( 𝑧 𝑃 𝐴 ) ) )
65	60	recnd	⊢ ( 𝐴 ∈ 𝑋 → ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ∈ ℂ )
66	1 58	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℝ )
67	7 66	mpan	⊢ ( 𝑧 ∈ 𝑋 → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℝ )
68	67	recnd	⊢ ( 𝑧 ∈ 𝑋 → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℂ )
69		mulcom	⊢ ( ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ∈ ℂ ∧ ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℂ ) → ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) = ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ) )
70	65 68 69	syl2an	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) = ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ) )
71	62 64 70	3brtr4d	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
72	71	ralrimiva	⊢ ( 𝐴 ∈ 𝑋 → ∀ 𝑧 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
73	4	cnnvnm	⊢ abs = ( normCV ‘ 𝐶 )
74	1 58 73 54 5 7 50	blo3i	⊢ ( ( 𝐹 ∈ ( 𝑈 LnOp 𝐶 ) ∧ ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) → 𝐹 ∈ 𝐵 )
75	57 60 72 74	syl3anc	⊢ ( 𝐴 ∈ 𝑋 → 𝐹 ∈ 𝐵 )