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 \in NrmCVec, w \in NrmCVec ⟼ \{t \in ({BaseSet (w)}^{BaseSet (u)}) \| \forall x \in ℂ \forall y \in BaseSet (u) \forall z \in BaseSet (u) t ((x \cdot_{𝑠OLD} (u) y) +_{v} (u) z) = (x \cdot_{𝑠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 \cdot_{𝑠OLD}$
19	9 18	cfv	$class \cdot_{𝑠OLD} (u)$
20	14	cv	$setvar y$
21	17 20 19	co	$class (x \cdot_{𝑠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 \cdot_{𝑠OLD} (u) y) +_{v} (u) z)$
26	25 16	cfv	$class t ((x \cdot_{𝑠OLD} (u) y) +_{v} (u) z)$
27	6 18	cfv	$class \cdot_{𝑠OLD} (w)$
28	20 16	cfv	$class t (y)$
29	17 28 27	co	$class (x \cdot_{𝑠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 \cdot_{𝑠OLD} (w) t (y)) +_{v} (w) t (z))$
33	26 32	wceq	$wff t ((x \cdot_{𝑠OLD} (u) y) +_{v} (u) z) = (x \cdot_{𝑠OLD} (w) t (y)) +_{v} (w) t (z)$
34	33 15 10	wral	$wff \forall z \in BaseSet (u) t ((x \cdot_{𝑠OLD} (u) y) +_{v} (u) z) = (x \cdot_{𝑠OLD} (w) t (y)) +_{v} (w) t (z)$
35	34 14 10	wral	$wff \forall y \in BaseSet (u) \forall z \in BaseSet (u) t ((x \cdot_{𝑠OLD} (u) y) +_{v} (u) z) = (x \cdot_{𝑠OLD} (w) t (y)) +_{v} (w) t (z)$
36	35 12 13	wral	$wff \forall x \in ℂ \forall y \in BaseSet (u) \forall z \in BaseSet (u) t ((x \cdot_{𝑠OLD} (u) y) +_{v} (u) z) = (x \cdot_{𝑠OLD} (w) t (y)) +_{v} (w) t (z)$
37	36 4 11	crab	$class \{t \in ({BaseSet (w)}^{BaseSet (u)}) \| \forall x \in ℂ \forall y \in BaseSet (u) \forall z \in BaseSet (u) t ((x \cdot_{𝑠OLD} (u) y) +_{v} (u) z) = (x \cdot_{𝑠OLD} (w) t (y)) +_{v} (w) t (z)\}$
38	1 3 2 2 37	cmpo	$class (u \in NrmCVec, w \in NrmCVec ⟼ \{t \in ({BaseSet (w)}^{BaseSet (u)}) \| \forall x \in ℂ \forall y \in BaseSet (u) \forall z \in BaseSet (u) t ((x \cdot_{𝑠OLD} (u) y) +_{v} (u) z) = (x \cdot_{𝑠OLD} (w) t (y)) +_{v} (w) t (z)\})$
39	0 38	wceq	$wff LnOp = (u \in NrmCVec, w \in NrmCVec ⟼ \{t \in ({BaseSet (w)}^{BaseSet (u)}) \| \forall x \in ℂ \forall y \in BaseSet (u) \forall z \in BaseSet (u) t ((x \cdot_{𝑠OLD} (u) y) +_{v} (u) z) = (x \cdot_{𝑠OLD} (w) t (y)) +_{v} (w) t (z)\})$

Metamath Proof Explorer

Definition df-lno

Detailed syntax breakdown