Metamath Proof Explorer

Definition df-lno

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.)

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

Detailed syntax breakdown

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