Definition df-ba 9547

Description: Define the base set of a normed complex vector space.

Assertion

Ref	Expression
df-ba	|- BaseSet = {<.x, y>. | y = ran (+v` x)}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-ba

Step	Hyp	Ref	Expression
1		cba 9537	. 2 class BaseSet
2		vy	. . . . 5 set y
3	2	cv 1297	. . . 4 class y
4		vx	. . . . . . 7 set x
5	4	cv 1297	. . . . . 6 class x
6		cpv 9536	. . . . . 6 class +v
7	5, 6	cfv 3998	. . . . 5 class (+v` x)
8	7	crn 3987	. . . 4 class ran (+v` x)
9	3, 8	wceq 1298	. . 3 wff y = ran (+v` x)
10	9, 4, 2	copab 3395	. 2 class {<.x, y>. | y = ran (+v` x)}
11	1, 10	wceq 1298	1 wff BaseSet = {<.x, y>. | y = ran (+v` x)}

This definition is referenced by:  bafval 9555

Copyright terms: Public domain