Theorem vci 8167

Description: The properties of a complex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. The variable W was chosen because V is already used for the universal class.

Hypotheses

Ref	Expression
vci.1	|- G = (1st` W)
vci.2	|- S = (2nd` W)
vci.3	|- X = ran G

Assertion

Ref	Expression
vci	|- (W e. CVec -> (G e. Abel /\ S:(CC X. X)-->X /\ A.x e. X ((1Sx) = x /\ A.y e. CC (A.z e. X (yS(xGz)) = ((ySx)G(ySz)) /\ A.z e. CC (((y + z)Sx) = ((ySx)G(zSx)) /\ ((y x. z)Sx) = (yS(zSx)))))))

Distinct variable groups:   x,y,z,G   x,S,y,z   x,X,y,z

Proof of Theorem vci

Step	Hyp	Ref	Expression
1		df-vc 8165	. . 3 |- 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))))))}
2	1	eleq2i 1538	. 2 |- (W e. CVec <-> W e. {<.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))))))})
3		vci.1	. . . . 5 |- G = (1st` W)
4	3	eqeq2i 1485	. . . 4 |- (g = G <-> g = (1st` W))
5		eleq1 1534	. . . . 5 |- (g = G -> (g e. Abel <-> G e. Abel))
6		rneq 3339	. . . . . . 7 |- (g = G -> ran g = ran G)
7		vci.3	. . . . . . 7 |- X = ran G
8	6, 7	syl6eqr 1525	. . . . . 6 |- (g = G -> ran g = X)
9		xpeq2 3201	. . . . . . . 8 |- (ran g = X -> (CC X. ran g) = (CC X. X))
10		feq2 3621	. . . . . . . 8 |- ((CC X. ran g) = (CC X. X) -> (s:(CC X. ran g)-->ran g <-> s:(CC X. X)-->ran g))
11	9, 10	syl 10	. . . . . . 7 |- (ran g = X -> (s:(CC X. ran g)-->ran g <-> s:(CC X. X)-->ran g))
12		feq3 3622	. . . . . . 7 |- (ran g = X -> (s:(CC X. X)-->ran g <-> s:(CC X. X)-->X))
13	11, 12	bitrd 528	. . . . . 6 |- (ran g = X -> (s:(CC X. ran g)-->ran g <-> s:(CC X. X)-->X))
14	8, 13	syl 10	. . . . 5 |- (g = G -> (s:(CC X. ran g)-->ran g <-> s:(CC X. X)-->X))
15		opreq 3967	. . . . . . . . . . . 12 |- (g = G -> (xgz) = (xGz))
16	15	opreq2d 3976	. . . . . . . . . . 11 |- (g = G -> (ys(xgz)) = (ys(xGz)))
17		opreq 3967	. . . . . . . . . . 11 |- (g = G -> ((ysx)g(ysz)) = ((ysx)G(ysz)))
18	16, 17	eqeq12d 1489	. . . . . . . . . 10 |- (g = G -> ((ys(xgz)) = ((ysx)g(ysz)) <-> (ys(xGz)) = ((ysx)G(ysz))))
19	8, 18	raleq12d 1794	. . . . . . . . 9 |- (g = G -> (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) <-> A.z e. X (ys(xGz)) = ((ysx)G(ysz))))
20		opreq 3967	. . . . . . . . . . . 12 |- (g = G -> ((ysx)g(zsx)) = ((ysx)G(zsx)))
21	20	eqeq2d 1486	. . . . . . . . . . 11 |- (g = G -> (((y + z)sx) = ((ysx)g(zsx)) <-> ((y + z)sx) = ((ysx)G(zsx))))
22	21	anbi1d 617	. . . . . . . . . 10 |- (g = G -> ((((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx))) <-> (((y + z)sx) = ((ysx)G(zsx)) /\ ((y x. z)sx) = (ys(zsx)))))
23	22	ralbidv 1663	. . . . . . . . 9 |- (g = G -> (A.z e. CC (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx))) <-> A.z e. CC (((y + z)sx) = ((ysx)G(zsx)) /\ ((y x. z)sx) = (ys(zsx)))))
24	19, 23	anbi12d 628	. . . . . . . 8 |- (g = G -> ((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)))) <-> (A.z e. X (ys(xGz)) = ((ysx)G(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)G(zsx)) /\ ((y x. z)sx) = (ys(zsx))))))
25	24	ralbidv 1663	. . . . . . 7 |- (g = G -> (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)))) <-> A.y e. CC (A.z e. X (ys(xGz)) = ((ysx)G(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)G(zsx)) /\ ((y x. z)sx) = (ys(zsx))))))
26	25	anbi2d 616	. . . . . 6 |- (g = 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))))) <-> ((1sx) = x /\ A.y e. CC (A.z e. X (ys(xGz)) = ((ysx)G(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)G(zsx)) /\ ((y x. z)sx) = (ys(zsx)))))))
27	8, 26	raleq12d 1794	. . . . 5 |- (g = 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))))) <-> A.x e. X ((1sx) = x /\ A.y e. CC (A.z e. X (ys(xGz)) = ((ysx)G(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)G(zsx)) /\ ((y x. z)sx) = (ys(zsx)))))))
28	5, 14, 27	3anbi123d 893	. . . 4 |- (g = G -> ((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)))))) <-> (G e. Abel /\ s:(CC X. X)-->X /\ A.x e. X ((1sx) = x /\ A.y e. CC (A.z e. X (ys(xGz)) = ((ysx)G(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)G(zsx)) /\ ((y x. z)sx) = (ys(zsx))))))))
29	4, 28	sylbir 201	. . 3 |- (g = (1st` W) -> ((g e. Abel /\ s:(CC X. ran g)-->ran g /\ A.x e. ran g((1