Theorem isvclem 8192

Description: Lemma for isvc 8196.

Hypothesis

Ref	Expression
isvclem.1	|- X = ran G

Assertion

Ref	Expression
isvclem	|- ((G e. V /\ S e. V) -> (<.G, S>. 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,z

Proof of Theorem isvclem

Step	Hyp	Ref	Expression
1		eleq1 1537	. . . 4 |- (g = G -> (g e. Abel <-> G e. Abel))
2		rneq 3345	. . . . . 6 |- (g = G -> ran g = ran G)
3		isvclem.1	. . . . . 6 |- X = ran G
4	2, 3	syl6eqr 1528	. . . . 5 |- (g = G -> ran g = X)
5		xpeq2 3207	. . . . . . 7 |- (ran g = X -> (CC X. ran g) = (CC X. X))
6		feq2 3627	. . . . . . 7 |- ((CC X. ran g) = (CC X. X) -> (s:(CC X. ran g)-->ran g <-> s:(CC X. X)-->ran g))
7	5, 6	syl 10	. . . . . 6 |- (ran g = X -> (s:(CC X. ran g)-->ran g <-> s:(CC X. X)-->ran g))
8		feq3 3628	. . . . . 6 |- (ran g = X -> (s:(CC X. X)-->ran g <-> s:(CC X. X)-->X))
9	7, 8	bitrd 530	. . . . 5 |- (ran g = X -> (s:(CC X. ran g)-->ran g <-> s:(CC X. X)-->X))
10	4, 9	syl 10	. . . 4 |- (g = G -> (s:(CC X. ran g)-->ran g <-> s:(CC X. X)-->X))
11		opreq 3973	. . . . . . . . . . 11 |- (g = G -> (xgz) = (xGz))
12	11	opreq2d 3982	. . . . . . . . . 10 |- (g = G -> (ys(xgz)) = (ys(xGz)))
13		opreq 3973	. . . . . . . . . 10 |- (g = G -> ((ysx)g(ysz)) = ((ysx)G(ysz)))
14	12, 13	eqeq12d 1492	. . . . . . . . 9 |- (g = G -> ((ys(xgz)) = ((ysx)g(ysz)) <-> (ys(xGz)) = ((ysx)G(ysz))))
15	4, 14	raleq12d 1797	. . . . . . . 8 |- (g = G -> (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) <-> A.z e. X (ys(xGz)) = ((ysx)G(ysz))))
16		opreq 3973	. . . . . . . . . . 11 |- (g = G -> ((ysx)g(zsx)) = ((ysx)G(zsx)))
17	16	eqeq2d 1489	. . . . . . . . . 10 |- (g = G -> (((y + z)sx) = ((ysx)g(zsx)) <-> ((y + z)sx) = ((ysx)G(zsx))))
18	17	anbi1d 619	. . . . . . . . 9 |- (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)))))
19	18	ralbidv 1666	. . . . . . . 8 |- (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)))))
20	15, 19	anbi12d 630	. . . . . . 7 |- (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))))))
21	20	ralbidv 1666	. . . . . 6 |- (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))))))
22	21	anbi2d 618	. . . . 5 |- (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)))))))
23	4, 22	raleq12d 1797	. . . 4 |- (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)))))))
24	1, 10, 23	3anbi123d 895	. . 3 |- (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))))))))
25		feq1 3626	. . . 4 |- (s = S -> (s:(CC X. X)-->X <-> S:(CC X. X)-->X))
26		opreq 3973	. . . . . . 7 |- (s = S -> (1sx) = (1Sx))
27	26	eqeq1d 1486	. . . . . 6 |- (s = S -> ((1sx) = x <-> (1Sx) = x))
28		opreq 3973	. . . . . . . . . 10 |- (s = S -> (ys(xGz)) = (yS(xGz)))
29		opreq 3973	. . . . . . . . . . 11 |- (s = S -> (ysx) = (ySx))
30		opreq 3973	. . . . . . . . . . 11 |- (s = S -> (ysz) = (ySz))
31	29, 30	opreq12d 3984	. . . . . . . . . 10 |- (s = S -> ((ysx)G(ysz)) = ((ySx)G(ySz)))
32	28, 31	eqeq12d 1492	. . . . . . . . 9 |- (s = S -> ((ys(xGz)) = ((ysx)G(ysz)) <-> (yS(xGz)) = ((ySx)G(ySz))))
33	32	ralbidv 1666	. . . . . . . 8 |- (s = S -> (A.z e. X (ys(xGz)) = ((ysx)G(ysz)) <-> A.z e. X (yS(xGz)) = ((ySx)G(ySz))))
34		opreq 3973	. . . . . . . . . . 11 |- (s = S -> ((y + z)sx)