Metamath Proof Explorer


Theorem genpass

Description: Associativity of an operation on reals. (Contributed by NM, 18-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 F = w 𝑷 , v 𝑷 x | y w z v x = y G z
genp.2 y 𝑸 z 𝑸 y G z 𝑸
genpass.4 dom F = 𝑷 × 𝑷
genpass.5 f 𝑷 g 𝑷 f F g 𝑷
genpass.6 f G g G h = f G g G h
Assertion genpass A F B F C = A F B F C

Proof

Step Hyp Ref Expression
1 genp.1 F = w 𝑷 , v 𝑷 x | y w z v x = y G z
2 genp.2 y 𝑸 z 𝑸 y G z 𝑸
3 genpass.4 dom F = 𝑷 × 𝑷
4 genpass.5 f 𝑷 g 𝑷 f F g 𝑷
5 genpass.6 f G g G h = f G g G h
6 1 2 genpelv B 𝑷 C 𝑷 t B F C g B h C t = g G h
7 6 3adant1 A 𝑷 B 𝑷 C 𝑷 t B F C g B h C t = g G h
8 7 anbi1d A 𝑷 B 𝑷 C 𝑷 t B F C x = f G t g B h C t = g G h x = f G t
9 8 exbidv A 𝑷 B 𝑷 C 𝑷 t t B F C x = f G t t g B h C t = g G h x = f G t
10 df-rex t B F C x = f G t t t B F C x = f G t
11 ovex g G h V
12 11 isseti t t = g G h
13 12 biantrur x = f G g G h t t = g G h x = f G g G h
14 19.41v t t = g G h x = f G g G h t t = g G h x = f G g G h
15 13 14 bitr4i x = f G g G h t t = g G h x = f G g G h
16 15 rexbii h C x = f G g G h h C t t = g G h x = f G g G h
17 rexcom4 h C t t = g G h x = f G g G h t h C t = g G h x = f G g G h
18 16 17 bitri h C x = f G g G h t h C t = g G h x = f G g G h
19 18 rexbii g B h C x = f G g G h g B t h C t = g G h x = f G g G h
20 rexcom4 g B t h C t = g G h x = f G g G h t g B h C t = g G h x = f G g G h
21 oveq2 t = g G h f G t = f G g G h
22 21 5 eqtr4di t = g G h f G t = f G g G h
23 22 eqeq2d t = g G h x = f G t x = f G g G h
24 23 pm5.32i t = g G h x = f G t t = g G h x = f G g G h
25 24 rexbii h C t = g G h x = f G t h C t = g G h x = f G g G h
26 r19.41v h C t = g G h x = f G t h C t = g G h x = f G t
27 25 26 bitr3i h C t = g G h x = f G g G h h C t = g G h x = f G t
28 27 rexbii g B h C t = g G h x = f G g G h g B h C t = g G h x = f G t
29 r19.41v g B h C t = g G h x = f G t g B h C t = g G h x = f G t
30 28 29 bitri g B h C t = g G h x = f G g G h g B h C t = g G h x = f G t
31 30 exbii t g B h C t = g G h x = f G g G h t g B h C t = g G h x = f G t
32 19 20 31 3bitri g B h C x = f G g G h t g B h C t = g G h x = f G t
33 9 10 32 3bitr4g A 𝑷 B 𝑷 C 𝑷 t B F C x = f G t g B h C x = f G g G h
34 33 rexbidv A 𝑷 B 𝑷 C 𝑷 f A t B F C x = f G t f A g B h C x = f G g G h
35 4 caovcl B 𝑷 C 𝑷 B F C 𝑷
36 1 2 genpelv A 𝑷 B F C 𝑷 x A F B F C f A t B F C x = f G t
37 35 36 sylan2 A 𝑷 B 𝑷 C 𝑷 x A F B F C f A t B F C x = f G t
38 37 3impb A 𝑷 B 𝑷 C 𝑷 x A F B F C f A t B F C x = f G t
39 4 caovcl A 𝑷 B 𝑷 A F B 𝑷
40 1 2 genpelv A F B 𝑷 C 𝑷 x A F B F C t A F B h C x = t G h
41 39 40 stoic3 A 𝑷 B 𝑷 C 𝑷 x A F B F C t A F B h C x = t G h
42 1 2 genpelv A 𝑷 B 𝑷 t A F B f A g B t = f G g
43 42 3adant3 A 𝑷 B 𝑷 C 𝑷 t A F B f A g B t = f G g
44 43 anbi1d A 𝑷 B 𝑷 C 𝑷 t A F B h C x = t G h f A g B t = f G g h C x = t G h
45 44 exbidv A 𝑷 B 𝑷 C 𝑷 t t A F B h C x = t G h t f A g B t = f G g h C x = t G h
46 df-rex t A F B h C x = t G h t t A F B h C x = t G h
47 19.41v t t = f G g h C x = f G g G h t t = f G g h C x = f G g G h
48 oveq1 t = f G g t G h = f G g G h
49 48 eqeq2d t = f G g x = t G h x = f G g G h
50 49 rexbidv t = f G g h C x = t G h h C x = f G g G h
51 50 pm5.32i t = f G g h C x = t G h t = f G g h C x = f G g G h
52 51 exbii t t = f G g h C x = t G h t t = f G g h C x = f G g G h
53 ovex f G g V
54 53 isseti t t = f G g
55 54 biantrur h C x = f G g G h t t = f G g h C x = f G g G h
56 47 52 55 3bitr4ri h C x = f G g G h t t = f G g h C x = t G h
57 56 rexbii g B h C x = f G g G h g B t t = f G g h C x = t G h
58 rexcom4 g B t t = f G g h C x = t G h t g B t = f G g h C x = t G h
59 57 58 bitri g B h C x = f G g G h t g B t = f G g h C x = t G h
60 59 rexbii f A g B h C x = f G g G h f A t g B t = f G g h C x = t G h
61 rexcom4 f A t g B t = f G g h C x = t G h t f A g B t = f G g h C x = t G h
62 r19.41vv f A g B t = f G g h C x = t G h f A g B t = f G g h C x = t G h
63 62 exbii t f A g B t = f G g h C x = t G h t f A g B t = f G g h C x = t G h
64 60 61 63 3bitri f A g B h C x = f G g G h t f A g B t = f G g h C x = t G h
65 45 46 64 3bitr4g A 𝑷 B 𝑷 C 𝑷 t A F B h C x = t G h f A g B h C x = f G g G h
66 41 65 bitrd A 𝑷 B 𝑷 C 𝑷 x A F B F C f A g B h C x = f G g G h
67 34 38 66 3bitr4rd A 𝑷 B 𝑷 C 𝑷 x A F B F C x A F B F C
68 67 eqrdv A 𝑷 B 𝑷 C 𝑷 A F B F C = A F B F C
69 0npr ¬ 𝑷
70 3 69 ndmovass ¬ A 𝑷 B 𝑷 C 𝑷 A F B F C = A F B F C
71 68 70 pm2.61i A F B F C = A F B F C