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 e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )
genp.2 
|- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )
Assertion genpelv 
|- ( ( A e. P. /\ B e. P. ) -> ( C e. ( A F B ) <-> E. g e. A E. h e. B C = ( g G h ) ) )

Proof

Step Hyp Ref Expression
1 genp.1 
 |-  F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )
2 genp.2 
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )
3 1 2 genpv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A F B ) = { f | E. g e. A E. h e. B f = ( g G h ) } )
4 3 eleq2d 
 |-  ( ( A e. P. /\ B e. P. ) -> ( C e. ( A F B ) <-> C e. { f | E. g e. A E. h e. B f = ( g G h ) } ) )
5 id 
 |-  ( C = ( g G h ) -> C = ( g G h ) )
6 ovex 
 |-  ( g G h ) e. _V
7 5 6 eqeltrdi 
 |-  ( C = ( g G h ) -> C e. _V )
8 7 rexlimivw 
 |-  ( E. h e. B C = ( g G h ) -> C e. _V )
9 8 rexlimivw 
 |-  ( E. g e. A E. h e. B C = ( g G h ) -> C e. _V )
10 eqeq1 
 |-  ( f = C -> ( f = ( g G h ) <-> C = ( g G h ) ) )
11 10 2rexbidv 
 |-  ( f = C -> ( E. g e. A E. h e. B f = ( g G h ) <-> E. g e. A E. h e. B C = ( g G h ) ) )
12 9 11 elab3 
 |-  ( C e. { f | E. g e. A E. h e. B f = ( g G h ) } <-> E. g e. A E. h e. B C = ( g G h ) )
13 4 12 bitrdi 
 |-  ( ( A e. P. /\ B e. P. ) -> ( C e. ( A F B ) <-> E. g e. A E. h e. B C = ( g G h ) ) )