Definition df-lno 30730

Description: Define the class of linear operators between two normed complex vector spaces. In the literature, an operator may be a partial function, i.e., the domain of an operator is not necessarily the entire vector space. However, since the domain of a linear operator is a vector subspace, we define it with a complete function for convenience and will use subset relations to specify the partial function case. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)

Assertion

Ref	Expression
df-lno	⊢ LnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))})

Distinct variable group:   𝑢,𝑡,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-lno

Step	Hyp	Ref	Expression
1		clno 30726	. 2 class LnOp
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 30570	. . 3 class NrmCVec
5		vx	. . . . . . . . . . . 12 setvar 𝑥
6	5	cv 1539	. . . . . . . . . . 11 class 𝑥
7		vy	. . . . . . . . . . . 12 setvar 𝑦
8	7	cv 1539	. . . . . . . . . . 11 class 𝑦
9	2	cv 1539	. . . . . . . . . . . 12 class 𝑢
10		cns 30573	. . . . . . . . . . . 12 class ·𝑠OLD
11	9, 10	cfv 6536	. . . . . . . . . . 11 class ( ·𝑠OLD ‘𝑢)
12	6, 8, 11	co 7410	. . . . . . . . . 10 class (𝑥( ·𝑠OLD ‘𝑢)𝑦)
13		vz	. . . . . . . . . . 11 setvar 𝑧
14	13	cv 1539	. . . . . . . . . 10 class 𝑧
15		cpv 30571	. . . . . . . . . . 11 class +𝑣
16	9, 15	cfv 6536	. . . . . . . . . 10 class ( +𝑣 ‘𝑢)
17	12, 14, 16	co 7410	. . . . . . . . 9 class ((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)
18		vt	. . . . . . . . . 10 setvar 𝑡
19	18	cv 1539	. . . . . . . . 9 class 𝑡
20	17, 19	cfv 6536	. . . . . . . 8 class (𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧))
21	8, 19	cfv 6536	. . . . . . . . . 10 class (𝑡‘𝑦)
22	3	cv 1539	. . . . . . . . . . 11 class 𝑤
23	22, 10	cfv 6536	. . . . . . . . . 10 class ( ·𝑠OLD ‘𝑤)
24	6, 21, 23	co 7410	. . . . . . . . 9 class (𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))
25	14, 19	cfv 6536	. . . . . . . . 9 class (𝑡‘𝑧)
26	22, 15	cfv 6536	. . . . . . . . 9 class ( +𝑣 ‘𝑤)
27	24, 25, 26	co 7410	. . . . . . . 8 class ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))
28	20, 27	wceq 1540	. . . . . . 7 wff (𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))
29		cba 30572	. . . . . . . 8 class BaseSet
30	9, 29	cfv 6536	. . . . . . 7 class (BaseSet‘𝑢)
31	28, 13, 30	wral 3052	. . . . . 6 wff ∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))
32	31, 7, 30	wral 3052	. . . . 5 wff ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))
33		cc 11132	. . . . 5 class ℂ
34	32, 5, 33	wral 3052	. . . 4 wff ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))
35	22, 29	cfv 6536	. . . . 5 class (BaseSet‘𝑤)
36		cmap 8845	. . . . 5 class ↑m
37	35, 30, 36	co 7410	. . . 4 class ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢))
38	34, 18, 37	crab 3420	. . 3 class {𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))}
39	2, 3, 4, 4, 38	cmpo 7412	. 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))})
40	1, 39	wceq 1540	1 wff LnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))})

This definition is referenced by:  lnoval  30738