Theorem genpass 3906

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 group(s):   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	. . . . . . . . 9 |- F = {<.<.w, v>., u>. | ((w e. P. /\ v e. P.) /\ u = {x | E.y e. w E.z e. v x = (yGz)})}
2		visset 1350	. . . . . . . . 9 |- x e. V
3	1, 2	genpelv 3897	. . . . . . . 8 |- (((AFB) e. P. /\ C e. P.) -> (x e. ((AFB)FC) <-> E.tE.h((t e. (AFB) /\ h e. C) /\ x = (tGh))))
4		genpass.5	. . . . . . . . 9 |- ((f e. P. /\ g e. P.) -> (fFg) e. P.)
5	4	caoprcl 3066	. . . . . . . 8 |- ((A e. P. /\ B e. P.) -> (AFB) e. P.)
6	3, 5	sylan 343	. . . . . . 7 |- (((A e. P. /\ B e. P.) /\ C e. P.) -> (x e. ((AFB)FC) <-> E.tE.h((t e. (AFB) /\ h e. C) /\ x = (tGh))))
7	6	3impa 609	. . . . . 6 |- ((A e. P. /\ B e. P. /\ C e. P.) -> (x e. ((AFB)FC) <-> E.tE.h((t e. (AFB) /\ h e. C) /\ x = (tGh))))
8		visset 1350	. . . . . . . . . . 11 |- t e. V
9	1, 8	genpelv 3897	. . . . . . . . . 10 |- ((A e. P. /\ B e. P.) -> (t e. (AFB) <-> E.fE.g((f e. A /\ g e. B) /\ t = (fGg))))
10	9	3adant3 599	. . . . . . . . 9 |- ((A e. P. /\ B e. P. /\ C e. P.) -> (t e. (AFB) <-> E.fE.g((f e. A /\ g e. B) /\ t = (fGg))))
11	10	anbi1d 469	. . . . . . . 8 |- ((A e. P. /\ B e. P. /\ C e. P.) -> ((t e. (AFB) /\ (h e. C /\ x = (tGh))) <-> (E.fE.g((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh)))))
12		anass 336	. . . . . . . 8 |- (((t e. (AFB) /\ h e. C) /\ x = (tGh)) <-> (t e. (AFB) /\ (h e. C /\ x = (tGh))))
13		19.41vv 964	. . . . . . . 8 |- (E.fE.g(((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh))) <-> (E.fE.g((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh))))
14	11, 12, 13	3bitr4g 428	. . . . . . 7 |- ((A e. P. /\ B e. P. /\ C e. P.) -> (((t e. (AFB) /\ h e. C) /\ x = (tGh)) <-> E.fE.g(((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh)))))
15	14	bi2exdv 938	. . . . . 6 |- ((A e. P. /\ B e. P. /\ C e. P.) -> (E.tE.h((t e. (AFB) /\ h e. C) /\ x = (tGh)) <-> E.tE.hE.fE.g(((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh)))))
16	7, 15	bitrd 406	. . . . 5 |- ((A e. P. /\ B e. P. /\ C e. P.) -> (x e. ((AFB)FC) <-> E.tE.hE.fE.g(((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh)))))
17		exrot4 778	. . . . . 6 |- (E.tE.hE.fE.g(((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh))) <-> E.fE.gE.tE.h(((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh))))
18		excom 728	. . . . . . . 8 |- (E.tE.h(((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh))) <-> E.hE.t(((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh))))
19		an4 388	. . . . . . . . . . . 12 |- ((((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh))) <-> (((f e. A /\ g e. B) /\ h e. C) /\ (t = (fGg) /\ x = (tGh))))
20		anass 336	. . . . . . . . . . . . 13 |- (((f e. A /\ g e. B) /\ h e. C) <-> (f e. A /\ (g e. B /\ h e. C)))
21		opreq1 3006	. . . . . . . . . . . . . . . 16 |- (t = (fGg) -> (tGh) = ((fGg)Gh))
22		genpass.6	. . . . . . . . . . . . . . . 16 |- ((fGg)Gh) = (fG(gGh))
23	21, 22	syl6eq 1140	. . . . . . . . . . . . . . 15 |- (t = (fGg) -> (tGh) = (fG(gGh)))
24	23	cleq2d 1112	. . . . . . . . . . . . . 14 |- (t = (fGg) -> (x = (tGh) <-> x = (fG(gGh))))
25	24	pm5.32i 489	. . . . . . . . . . . . 13 |- ((t = (fGg) /\ x = (tGh)) <-> (t = (fGg) /\ x = (fG(gGh))))
26	20, 25	anbi12i 369	. . . . . . . . . . . 12 |- ((((f e. A /\ g e. B) /\ h e. C) /\ (t = (fGg) /\ x = (tGh))) <-> ((f e. A /\ (g e. B /\ h e. C)) /\ (t = (fGg) /\ x = (fG(gGh)))))
27		an12 370	. . . . . . . . . . . 12 |- (((f e. A /\ (g e. B /\ h e. C)) /\ (t = (fGg) /\ x = (fG(gGh)))) <-> (t = (fGg) /\ ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))))
28	19, 26, 27	3bitr 155	. . . . . . . . . . 11 |- ((((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh))) <-> (t = (fGg) /\ ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))))
29	28	biex 733	. . . . . . . . . 10 |- (E.t(((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh))) <-> E.t(t = (fGg) /\ ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))))
30		19.41v 963	. . . . . . . . . . 11 |- (E.t(t = (fGg) /\ ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))) <-> (E.t t = (fGg) /\ ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))))
31		oprex 3018	. . . . . . . . . . . 12 |- (fGg) e. V
32	31	isseti 1352	. . . . . . . . . . 11 |- E.t t = (fGg)
33	30, 32	mpbiran 547	. . . . . . . . . 10 |- (E.t(t = (fGg) /\ ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh)))) <-> ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh))))
34	29, 33	bitr 151	. . . . . . . . 9 |- (E.t(((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh))) <-> ((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh))))
35	34	biex 733	. . . . . . . 8 |- (E.hE.t(((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh))) <-> E.h((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh))))
36	18, 35	bitr 151	. . . . . . 7 |- (E.tE.h(((f e. A /\ g e. B) /\ t = (fGg)) /\ (h e. C /\ x = (tGh))) <-> E.h((f e. A /\ (g e. B /\ h e. C)) /\ x = (fG(gGh))))
37	36	bi2ex 734	. . . . . 6 |- (E.fE.gE.tE.h(((f e. A /\ g e. B) /\ t = (fGg)