Metamath Proof Explorer


Theorem genpv

Description: Value of general operation (addition or multiplication) on positive reals. (Contributed by NM, 10-Mar-1996) (Revised by Mario Carneiro, 17-Nov-2014) (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 𝑸
Assertion genpv A 𝑷 B 𝑷 A F B = f | g A h B f = g G h

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 oveq1 f = A f F g = A F g
4 rexeq f = A y f z g x = y G z y A z g x = y G z
5 4 abbidv f = A x | y f z g x = y G z = x | y A z g x = y G z
6 3 5 eqeq12d f = A f F g = x | y f z g x = y G z A F g = x | y A z g x = y G z
7 oveq2 g = B A F g = A F B
8 rexeq g = B z g x = y G z z B x = y G z
9 8 rexbidv g = B y A z g x = y G z y A z B x = y G z
10 9 abbidv g = B x | y A z g x = y G z = x | y A z B x = y G z
11 7 10 eqeq12d g = B A F g = x | y A z g x = y G z A F B = x | y A z B x = y G z
12 elprnq f 𝑷 y f y 𝑸
13 elprnq g 𝑷 z g z 𝑸
14 eleq1 x = y G z x 𝑸 y G z 𝑸
15 2 14 syl5ibrcom y 𝑸 z 𝑸 x = y G z x 𝑸
16 12 13 15 syl2an f 𝑷 y f g 𝑷 z g x = y G z x 𝑸
17 16 an4s f 𝑷 g 𝑷 y f z g x = y G z x 𝑸
18 17 rexlimdvva f 𝑷 g 𝑷 y f z g x = y G z x 𝑸
19 18 abssdv f 𝑷 g 𝑷 x | y f z g x = y G z 𝑸
20 nqex 𝑸 V
21 ssexg x | y f z g x = y G z 𝑸 𝑸 V x | y f z g x = y G z V
22 19 20 21 sylancl f 𝑷 g 𝑷 x | y f z g x = y G z V
23 rexeq w = f y w z v x = y G z y f z v x = y G z
24 23 abbidv w = f x | y w z v x = y G z = x | y f z v x = y G z
25 rexeq v = g z v x = y G z z g x = y G z
26 25 rexbidv v = g y f z v x = y G z y f z g x = y G z
27 26 abbidv v = g x | y f z v x = y G z = x | y f z g x = y G z
28 24 27 1 ovmpog f 𝑷 g 𝑷 x | y f z g x = y G z V f F g = x | y f z g x = y G z
29 22 28 mpd3an3 f 𝑷 g 𝑷 f F g = x | y f z g x = y G z
30 6 11 29 vtocl2ga A 𝑷 B 𝑷 A F B = x | y A z B x = y G z
31 eqeq1 x = f x = y G z f = y G z
32 31 2rexbidv x = f y A z B x = y G z y A z B f = y G z
33 oveq1 y = g y G z = g G z
34 33 eqeq2d y = g f = y G z f = g G z
35 oveq2 z = h g G z = g G h
36 35 eqeq2d z = h f = g G z f = g G h
37 34 36 cbvrex2vw y A z B f = y G z g A h B f = g G h
38 32 37 bitrdi x = f y A z B x = y G z g A h B f = g G h
39 38 cbvabv x | y A z B x = y G z = f | g A h B f = g G h
40 30 39 eqtrdi A 𝑷 B 𝑷 A F B = f | g A h B f = g G h