Definition df-vc 27414

Description: Define the class of all complex vector spaces. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
df-vc	|- CVecOLD = { <. g , s >. | ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) }

Distinct variable group:   g, s, x, y, z

Detailed syntax breakdown of Definition df-vc

Step	Hyp	Ref	Expression
1		cvc 27413	. 2 class CVecOLD
2		vg	. . . . . 6 setvar g
3	2	cv 1482	. . . . 5 class g
4		cablo 27398	. . . . 5 class AbelOp
5	3, 4	wcel 1990	. . . 4 wff g e. AbelOp
6		cc 9934	. . . . . 6 class CC
7	3	crn 5115	. . . . . 6 class ran g
8	6, 7	cxp 5112	. . . . 5 class ( CC X. ran g )
9		vs	. . . . . 6 setvar s
10	9	cv 1482	. . . . 5 class s
11	8, 7, 10	wf 5884	. . . 4 wff s : ( CC X. ran g ) --> ran g
12		c1 9937	. . . . . . . 8 class 1
13		vx	. . . . . . . . 9 setvar x
14	13	cv 1482	. . . . . . . 8 class x
15	12, 14, 10	co 6650	. . . . . . 7 class ( 1 s x )
16	15, 14	wceq 1483	. . . . . 6 wff ( 1 s x ) = x
17		vy	. . . . . . . . . . . 12 setvar y
18	17	cv 1482	. . . . . . . . . . 11 class y
19		vz	. . . . . . . . . . . . 13 setvar z
20	19	cv 1482	. . . . . . . . . . . 12 class z
21	14, 20, 3	co 6650	. . . . . . . . . . 11 class ( x g z )
22	18, 21, 10	co 6650	. . . . . . . . . 10 class ( y s ( x g z ) )
23	18, 14, 10	co 6650	. . . . . . . . . . 11 class ( y s x )
24	18, 20, 10	co 6650	. . . . . . . . . . 11 class ( y s z )
25	23, 24, 3	co 6650	. . . . . . . . . 10 class ( ( y s x ) g ( y s z ) )
26	22, 25	wceq 1483	. . . . . . . . 9 wff ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) )
27	26, 19, 7	wral 2912	. . . . . . . 8 wff A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) )
28		caddc 9939	. . . . . . . . . . . . 13 class +
29	18, 20, 28	co 6650	. . . . . . . . . . . 12 class ( y + z )
30	29, 14, 10	co 6650	. . . . . . . . . . 11 class ( ( y + z ) s x )
31	20, 14, 10	co 6650	. . . . . . . . . . . 12 class ( z s x )
32	23, 31, 3	co 6650	. . . . . . . . . . 11 class ( ( y s x ) g ( z s x ) )
33	30, 32	wceq 1483	. . . . . . . . . 10 wff ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) )
34		cmul 9941	. . . . . . . . . . . . 13 class x.
35	18, 20, 34	co 6650	. . . . . . . . . . . 12 class ( y x. z )
36	35, 14, 10	co 6650	. . . . . . . . . . 11 class ( ( y x. z ) s x )
37	18, 31, 10	co 6650	. . . . . . . . . . 11 class ( y s ( z s x ) )
38	36, 37	wceq 1483	. . . . . . . . . 10 wff ( ( y x. z ) s x ) = ( y s ( z s x ) )
39	33, 38	wa 384	. . . . . . . . 9 wff ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) )
40	39, 19, 6	wral 2912	. . . . . . . 8 wff A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) )
41	27, 40	wa 384	. . . . . . 7 wff ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) )
42	41, 17, 6	wral 2912	. . . . . 6 wff A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) )
43	16, 42	wa 384	. . . . 5 wff ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) )
44	43, 13, 7	wral 2912	. . . 4 wff A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) )
45	5, 11, 44	w3a 1037	. . 3 wff ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) )
46	45, 2, 9	copab 4712	. 2 class { <. g , s >. | ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) }
47	1, 46	wceq 1483	1 wff CVecOLD = { <. g , s >. | ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) }

This definition is referenced by:  vcrel  27415  vciOLD  27416  isvclem  27432