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 = u ∈ NrmCVec , w ∈ NrmCVec ⟼ t ∈ BaseSet ⁡ w BaseSet ⁡ u | ∀ x ∈ ℂ ∀ y ∈ BaseSet ⁡ u ∀ z ∈ BaseSet ⁡ u t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z

Detailed syntax breakdown

Step Hyp Ref Expression
0 clno class LnOp
1 vu setvar u
2 cnv class NrmCVec
3 vw setvar w
4 vt setvar t
5 cba class BaseSet
6 3 cv setvar w
7 6 5 cfv class BaseSet ⁡ w
8 cmap class ↑ 𝑚
9 1 cv setvar u
10 9 5 cfv class BaseSet ⁡ u
11 7 10 8 co class BaseSet ⁡ w BaseSet ⁡ u
12 vx setvar x
13 cc class ℂ
14 vy setvar y
15 vz setvar z
16 4 cv setvar t
17 12 cv setvar x
18 cns class ⋅ 𝑠OLD
19 9 18 cfv class ⋅ 𝑠OLD ⁡ u
20 14 cv setvar y
21 17 20 19 co class x ⋅ 𝑠OLD ⁡ u y
22 cpv class + v
23 9 22 cfv class + v ⁡ u
24 15 cv setvar z
25 21 24 23 co class x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z
26 25 16 cfv class t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z
27 6 18 cfv class ⋅ 𝑠OLD ⁡ w
28 20 16 cfv class t ⁡ y
29 17 28 27 co class x ⋅ 𝑠OLD ⁡ w t ⁡ y
30 6 22 cfv class + v ⁡ w
31 24 16 cfv class t ⁡ z
32 29 31 30 co class x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
33 26 32 wceq wff t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
34 33 15 10 wral wff ∀ z ∈ BaseSet ⁡ u t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
35 34 14 10 wral wff ∀ y ∈ BaseSet ⁡ u ∀ z ∈ BaseSet ⁡ u t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
36 35 12 13 wral wff ∀ x ∈ ℂ ∀ y ∈ BaseSet ⁡ u ∀ z ∈ BaseSet ⁡ u t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
37 36 4 11 crab class t ∈ BaseSet ⁡ w BaseSet ⁡ u | ∀ x ∈ ℂ ∀ y ∈ BaseSet ⁡ u ∀ z ∈ BaseSet ⁡ u t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
38 1 3 2 2 37 cmpo class u ∈ NrmCVec , w ∈ NrmCVec ⟼ t ∈ BaseSet ⁡ w BaseSet ⁡ u | ∀ x ∈ ℂ ∀ y ∈ BaseSet ⁡ u ∀ z ∈ BaseSet ⁡ u t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
39 0 38 wceq wff LnOp = u ∈ NrmCVec , w ∈ NrmCVec ⟼ t ∈ BaseSet ⁡ w BaseSet ⁡ u | ∀ x ∈ ℂ ∀ y ∈ BaseSet ⁡ u ∀ z ∈ BaseSet ⁡ u t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z