Metamath Proof Explorer


Theorem genpelv

Description: Membership in value of general operation (addition or multiplication) on positive reals. (Contributed by NM, 13-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 𝑸
Assertion genpelv A 𝑷 B 𝑷 C A F B g A h B C = 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 1 2 genpv A 𝑷 B 𝑷 A F B = f | g A h B f = g G h
4 3 eleq2d A 𝑷 B 𝑷 C A F B C f | g A h B f = g G h
5 id C = g G h C = g G h
6 ovex g G h V
7 5 6 eqeltrdi C = g G h C V
8 7 rexlimivw h B C = g G h C V
9 8 rexlimivw g A h B C = g G h C V
10 eqeq1 f = C f = g G h C = g G h
11 10 2rexbidv f = C g A h B f = g G h g A h B C = g G h
12 9 11 elab3 C f | g A h B f = g G h g A h B C = g G h
13 4 12 bitrdi A 𝑷 B 𝑷 C A F B g A h B C = g G h