Definition df-vc 8165

Description: Define the class of all complex vector spaces.

Assertion

Ref	Expression
df-vc	|- CVec = {<.g, s>. | (g e. Abel /\ s:(CC X. ran g)-->ran g /\ A.x e. ran g((1sx) = x /\ A.y e. CC (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx))))))}

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

Detailed syntax breakdown of Definition df-vc

Step	Hyp	Ref	Expression
1		cvc 8164	. 2 class CVec
2		vg	. . . . . 6 set g
3	2	cv 955	. . . . 5 class g
4		cabl 8099	. . . . 5 class Abel
5	3, 4	wcel 958	. . . 4 wff g e. Abel
6		cc 5232	. . . . . 6 class CC
7	3	crn 3171	. . . . . 6 class ran g
8	6, 7	cxp 3168	. . . . 5 class (CC X. ran g)
9		vs	. . . . . 6 set s
10	9	cv 955	. . . . 5 class s
11	8, 7, 10	wf 3178	. . . 4 wff s:(CC X. ran g)-->ran g
12		c1 5235	. . . . . . . 8 class 1
13		vx	. . . . . . . . 9 set x
14	13	cv 955	. . . . . . . 8 class x
15	12, 14, 10	co 3963	. . . . . . 7 class (1sx)
16	15, 14	wceq 956	. . . . . 6 wff (1sx) = x
17		vy	. . . . . . . . . . . 12 set y
18	17	cv 955	. . . . . . . . . . 11 class y
19		vz	. . . . . . . . . . . . 13 set z
20	19	cv 955	. . . . . . . . . . . 12 class z
21	14, 20, 3	co 3963	. . . . . . . . . . 11 class (xgz)
22	18, 21, 10	co 3963	. . . . . . . . . 10 class (ys(xgz))
23	18, 14, 10	co 3963	. . . . . . . . . . 11 class (ysx)
24	18, 20, 10	co 3963	. . . . . . . . . . 11 class (ysz)
25	23, 24, 3	co 3963	. . . . . . . . . 10 class ((ysx)g(ysz))
26	22, 25	wceq 956	. . . . . . . . 9 wff (ys(xgz)) = ((ysx)g(ysz))
27	26, 19, 7	wral 1645	. . . . . . . 8 wff A.z e. ran g(ys(xgz)) = ((ysx)g(ysz))
28		caddc 5237	. . . . . . . . . . . . 13 class +
29	18, 20, 28	co 3963	. . . . . . . . . . . 12 class (y + z)
30	29, 14, 10	co 3963	. . . . . . . . . . 11 class ((y + z)sx)
31	20, 14, 10	co 3963	. . . . . . . . . . . 12 class (zsx)
32	23, 31, 3	co 3963	. . . . . . . . . . 11 class ((ysx)g(zsx))
33	30, 32	wceq 956	. . . . . . . . . 10 wff ((y + z)sx) = ((ysx)g(zsx))
34		cmul 5239	. . . . . . . . . . . . 13 class x.
35	18, 20, 34	co 3963	. . . . . . . . . . . 12 class (y x. z)
36	35, 14, 10	co 3963	. . . . . . . . . . 11 class ((y x. z)sx)
37	18, 31, 10	co 3963	. . . . . . . . . . 11 class (ys(zsx))
38	36, 37	wceq 956	. . . . . . . . . 10 wff ((y x. z)sx) = (ys(zsx))
39	33, 38	wa 223	. . . . . . . . 9 wff (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx)))
40	39, 19, 6	wral 1645	. . . . . . . 8 wff A.z e. CC (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx)))
41	27, 40	wa 223	. . . . . . 7 wff (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx))))
42	41, 17, 6	wral 1645	. . . . . 6 wff A.y e. CC (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx))))
43	16, 42	wa 223	. . . . 5 wff ((1sx) = x /\ A.y e. CC (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx)))))
44	43, 13, 7	wral 1645	. . . 4 wff A.x e. ran g((1sx) = x /\ A.y e. CC (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx)))))
45	5, 11, 44	w3a 775	. . 3 wff (g e. Abel /\ s:(CC X. ran g)-->ran g /\ A.x e. ran g((1sx) = x /\ A.y e. CC (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx))))))
46	45, 2, 9	copab 2666	. 2 class {<.g, s>. | (g e. Abel /\ s:(CC X. ran g)-->ran g /\ A.x e. ran g((1sx) = x /\ A.y e. CC (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx))))))}
47	1, 46	wceq 956	1 wff CVec = {<.g, s>. | (g e. Abel /\ s:(CC X. ran g)-->ran g /\ A.x e. ran g((1sx) = x /\ A.y e. CC (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx))))))}

This definition is referenced by:  vcrel 8166  vci 8167  isvclem 8196

Copyright terms: Public domain