Theorem genpass 5092

Description: Associativity of an operation on reals.

Hypotheses

Ref	Expression
genp.1	|- F = {<.<.w, v>., u>. | ((w e. P. /\ v e. P.) /\ u = {x | E.y e. w E.z e. v x = (yGz)})}
genpass.2	|- B e. V
genpass.3	|- C e. V
genpass.4	|- dom F = (P. X. P.)
genpass.5	|- ((f e. P. /\ g e. P.) -> (fFg) e. P.)
genpass.6	|- ((fGg)Gh) = (fG(gGh))

Assertion

Ref	Expression
genpass	|- ((AFB)FC) = (AF(BFC))

Distinct variable groups:   x,y,z,f,g,h,A   x,B,y,z,f,g,h   x,w,v,u,G,y,z,f,g,h   f,F,g   x,C,y,z,f,g,h   x,F,y,z,h

Proof of Theorem genpass

Step	Hyp	Ref	Expression
1		genp.1	. . . . . . . . . 10 |- F = {<.<.w, v>., u>. | ((w e. P. /\ v e. P.) /\ u = {x | E.y e. w E.z e. v x = (yGz)})}
2		visset 1809	. . . . . . . . . 10 |- t e. V
3	1, 2	genpelv 5083	. . . . . . . . 9 |- ((B e. P. /\ C e. P.) -> (t e. (BFC) <-> E.gE.h((g e. B /\ h e. C) /\ t = (gGh))))
4	3	3adant1 796	. . . . . . . 8 |- ((A e. P. /\ B e. P. /\ C e. P.) -> (t e. (BFC) <-> E.gE.h((g e. B /\ h e. C) /\ t = (gGh))))
5	4	anbi1d 616	. . . . . . 7 |- ((A e. P. /\ B e. P. /\ C e. P.) -> ((t e. (BFC) /\ (f e. A /\ x = (fGt))) <-> (E.gE.h((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt)))))
6		anass 439	. . . . . . . 8 |- (((f e. A /\ t e. (BFC)) /\ x = (fGt)) <-> (f e. A /\ (t e. (BFC) /\ x = (fGt))))
7		an12 484	. . . . . . . 8 |- ((f e. A /\ (t e. (BFC) /\ x = (fGt))) <-> (t e. (BFC) /\ (f e. A /\ x = (fGt))))
8	6, 7	bitr 173	. . . . . . 7 |- (((f e. A /\ t e. (BFC)) /\ x = (fGt)) <-> (t e. (BFC) /\ (f e. A /\ x = (fGt))))
9		19.41vv 1304	. . . . . . 7 |- (E.gE.h(((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt))) <-> (E.gE.h((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt))))
10	5, 8, 9	3bitr4g 554	. . . . . 6 |- ((A e. P. /\ B e. P. /\ C e. P.) -> (((f e. A /\ t e. (BFC)) /\ x = (fGt)) <-> E.gE.h(((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt)))))
11	10	2exbidv 1279	. . . . 5 |- ((A e. P. /\ B e. P. /\ C e. P.) -> (E.fE.t((f e. A /\ t e. (BFC)) /\ x = (fGt)) <-> E.fE.tE.gE.h(((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt)))))
12		exrot3 1097	. . . . . . 7 |- (E.tE.gE.h(((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt))) <-> E.gE.hE.t(((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt))))
13		an4 506	. . . . . . . . . . 11 |- ((((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt))) <-> (((g e. B /\ h e. C) /\ f e. A) /\ (t = (gGh) /\ x = (fGt))))
14		ancom 435	. . . . . . . . . . . 12 |- (((g e. B /\ h e. C) /\ f e. A) <-> (f e. A /\ (g e. B /\ h e. C)))
15		opreq2 3960	. . . . . . . . . . . . . 14 |- (t = (gGh) -> (fGt) = (fG(gGh)))
16	15	eqeq2d 1483	. . . . . . . . . . . . 13 |- (t = (gGh) -> (x = (fGt) <-> x = (fG(gGh))))
17	16	pm5.32i 644	. . . . . . . . . . . 12 |- ((t = (gGh) /\ x = (fGt)) <-> (t = (gGh) /\ x = (fG(gGh))))
18	14, 17	anbi12i 482	. . . . . . . . . . 11 |- ((((g e. B /\ h e. C) /\ f e. A) /\ (t = (gGh) /\ x = (fGt))) <-> ((f e. A /\ (g e. B /\ h e. C)) /\ (t = (gGh) /\ x = (fG(gGh)))))
19		an12 484	. . . . . . . . . . 11 |- (((f e. A /\ (g e. B /\ h e. C)) /\ (t = (gGh) /\ x = (fG(gGh)))) <-> (t = (gGh) /\ ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))))
20	13, 18, 19	3bitr 177	. . . . . . . . . 10 |- ((((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt))) <-> (t = (gGh) /\ ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))))
21	20	exbii 1049	. . . . . . . . 9 |- (E.t(((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt))) <-> E.t(t = (gGh) /\ ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))))
22		19.41v 1303	. . . . . . . . . 10 |- (E.t(t = (gGh) /\ ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))) <-> (E.t t = (gGh) /\ ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))))
23		oprex 3974	. . . . . . . . . . 11 |- (gGh) e. V
24	23	isseti 1811	. . . . . . . . . 10 |- E.t t = (gGh)
25	22, 24	mpbiran 727	. . . . . . . . 9 |- (E.t(t = (gGh) /\ ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))) <-> ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh))))
26	21, 25	bitr 173	. . . . . . . 8 |- (E.t(((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt))) <-> ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh))))
27	26	2exbii 1050	. . . . . . 7 |- (E.gE.hE.t(((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt))) <-> E.gE.h((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh))))
28	12, 27	bitr 173	. . . . . 6 |- (E.tE.gE.h(((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt))) <-> E.gE.h((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh))))
29	28	exbii 1049	. . . . 5 |- (E.fE.tE.gE.h(((g e. B /\ h e. C) /\ t = (gGh)) /\ (f e. A /\ x = (fGt))) <-> E.fE.gE.h((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh))))
30	11, 29	syl6bb 535	. . . 4 |- ((A e. P. /\ B e. P. /\ C e. P.) -> (E.fE.t((f e. A /\ t e. (BFC)) /\ x = (fGt)) <-> E.fE.gE.h((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))))
31		visset 1809	. . . . . . 7 |- x e. V
32	1, 31	genpelv 5083	. . . . . 6 |- ((A e. P. /\ (BFC) e. P.) -> (x e. (AF(BFC)) <-> E.fE.t((f e. A /\ t e. (BFC)) /\ x = (fGt))))
33		genpass.5	. . . . . . 7 |- ((f e. P. /\ g e. P.) -> (fFg) e. P.)
34	33	caoprcl 4044	. . . . . 6 |- ((B e. P. /\ C e. P.) -> (BFC) e. P.)
35	32, 34	sylan2 451	. . . . 5 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (x e. (AF(BFC)) <-> E.fE.t((f e. A /\ t e. (BFC)) <