This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. NrmCVec , w e. NrmCVec |-> { t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) | A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clno 
 |-  LnOp
1 vu 
 |-  u
2 cnv 
 |-  NrmCVec
3 vw 
 |-  w
4 vt 
 |-  t
5 cba 
 |-  BaseSet
6 3 cv 
 |-  w
7 6 5 cfv 
 |-  ( BaseSet ` w )
8 cmap 
 |-  ^m
9 1 cv 
 |-  u
10 9 5 cfv 
 |-  ( BaseSet ` u )
11 7 10 8 co 
 |-  ( ( BaseSet ` w ) ^m ( BaseSet ` u ) )
12 vx 
 |-  x
13 cc 
 |-  CC
14 vy 
 |-  y
15 vz 
 |-  z
16 4 cv 
 |-  t
17 12 cv 
 |-  x
18 cns 
 |-  .sOLD
19 9 18 cfv 
 |-  ( .sOLD ` u )
20 14 cv 
 |-  y
21 17 20 19 co 
 |-  ( x ( .sOLD ` u ) y )
22 cpv 
 |-  +v
23 9 22 cfv 
 |-  ( +v ` u )
24 15 cv 
 |-  z
25 21 24 23 co 
 |-  ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z )
26 25 16 cfv 
 |-  ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) )
27 6 18 cfv 
 |-  ( .sOLD ` w )
28 20 16 cfv 
 |-  ( t ` y )
29 17 28 27 co 
 |-  ( x ( .sOLD ` w ) ( t ` y ) )
30 6 22 cfv 
 |-  ( +v ` w )
31 24 16 cfv 
 |-  ( t ` z )
32 29 31 30 co 
 |-  ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) )
33 26 32 wceq 
 |-  ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) )
34 33 15 10 wral 
 |-  A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) )
35 34 14 10 wral 
 |-  A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) )
36 35 12 13 wral 
 |-  A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) )
37 36 4 11 crab 
 |-  { t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) | A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) }
38 1 3 2 2 37 cmpo 
 |-  ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) | A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) } )
39 0 38 wceq 
 |-  LnOp = ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) | A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) } )