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 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 genpv 
|- ( ( A e. P. /\ B e. P. ) -> ( A F B ) = { f | E. g e. A E. h e. B f = ( 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 oveq1 
 |-  ( f = A -> ( f F g ) = ( A F g ) )
4 rexeq 
 |-  ( f = A -> ( E. y e. f E. z e. g x = ( y G z ) <-> E. y e. A E. z e. g x = ( y G z ) ) )
5 4 abbidv 
 |-  ( f = A -> { x | E. y e. f E. z e. g x = ( y G z ) } = { x | E. y e. A E. z e. g x = ( y G z ) } )
6 3 5 eqeq12d 
 |-  ( f = A -> ( ( f F g ) = { x | E. y e. f E. z e. g x = ( y G z ) } <-> ( A F g ) = { x | E. y e. A E. z e. g x = ( y G z ) } ) )
7 oveq2 
 |-  ( g = B -> ( A F g ) = ( A F B ) )
8 rexeq 
 |-  ( g = B -> ( E. z e. g x = ( y G z ) <-> E. z e. B x = ( y G z ) ) )
9 8 rexbidv 
 |-  ( g = B -> ( E. y e. A E. z e. g x = ( y G z ) <-> E. y e. A E. z e. B x = ( y G z ) ) )
10 9 abbidv 
 |-  ( g = B -> { x | E. y e. A E. z e. g x = ( y G z ) } = { x | E. y e. A E. z e. B x = ( y G z ) } )
11 7 10 eqeq12d 
 |-  ( g = B -> ( ( A F g ) = { x | E. y e. A E. z e. g x = ( y G z ) } <-> ( A F B ) = { x | E. y e. A E. z e. B x = ( y G z ) } ) )
12 elprnq 
 |-  ( ( f e. P. /\ y e. f ) -> y e. Q. )
13 elprnq 
 |-  ( ( g e. P. /\ z e. g ) -> z e. Q. )
14 eleq1 
 |-  ( x = ( y G z ) -> ( x e. Q. <-> ( y G z ) e. Q. ) )
15 2 14 syl5ibrcom 
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( x = ( y G z ) -> x e. Q. ) )
16 12 13 15 syl2an 
 |-  ( ( ( f e. P. /\ y e. f ) /\ ( g e. P. /\ z e. g ) ) -> ( x = ( y G z ) -> x e. Q. ) )
17 16 an4s 
 |-  ( ( ( f e. P. /\ g e. P. ) /\ ( y e. f /\ z e. g ) ) -> ( x = ( y G z ) -> x e. Q. ) )
18 17 rexlimdvva 
 |-  ( ( f e. P. /\ g e. P. ) -> ( E. y e. f E. z e. g x = ( y G z ) -> x e. Q. ) )
19 18 abssdv 
 |-  ( ( f e. P. /\ g e. P. ) -> { x | E. y e. f E. z e. g x = ( y G z ) } C_ Q. )
20 nqex 
 |-  Q. e. _V
21 ssexg 
 |-  ( ( { x | E. y e. f E. z e. g x = ( y G z ) } C_ Q. /\ Q. e. _V ) -> { x | E. y e. f E. z e. g x = ( y G z ) } e. _V )
22 19 20 21 sylancl 
 |-  ( ( f e. P. /\ g e. P. ) -> { x | E. y e. f E. z e. g x = ( y G z ) } e. _V )
23 rexeq 
 |-  ( w = f -> ( E. y e. w E. z e. v x = ( y G z ) <-> E. y e. f E. z e. v x = ( y G z ) ) )
24 23 abbidv 
 |-  ( w = f -> { x | E. y e. w E. z e. v x = ( y G z ) } = { x | E. y e. f E. z e. v x = ( y G z ) } )
25 rexeq 
 |-  ( v = g -> ( E. z e. v x = ( y G z ) <-> E. z e. g x = ( y G z ) ) )
26 25 rexbidv 
 |-  ( v = g -> ( E. y e. f E. z e. v x = ( y G z ) <-> E. y e. f E. z e. g x = ( y G z ) ) )
27 26 abbidv 
 |-  ( v = g -> { x | E. y e. f E. z e. v x = ( y G z ) } = { x | E. y e. f E. z e. g x = ( y G z ) } )
28 24 27 1 ovmpog 
 |-  ( ( f e. P. /\ g e. P. /\ { x | E. y e. f E. z e. g x = ( y G z ) } e. _V ) -> ( f F g ) = { x | E. y e. f E. z e. g x = ( y G z ) } )
29 22 28 mpd3an3 
 |-  ( ( f e. P. /\ g e. P. ) -> ( f F g ) = { x | E. y e. f E. z e. g x = ( y G z ) } )
30 6 11 29 vtocl2ga 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A F B ) = { x | E. y e. A E. z e. B x = ( y G z ) } )
31 eqeq1 
 |-  ( x = f -> ( x = ( y G z ) <-> f = ( y G z ) ) )
32 31 2rexbidv 
 |-  ( x = f -> ( E. y e. A E. z e. B x = ( y G z ) <-> E. y e. A E. z e. 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 
 |-  ( E. y e. A E. z e. B f = ( y G z ) <-> E. g e. A E. h e. B f = ( g G h ) )
38 32 37 bitrdi 
 |-  ( x = f -> ( E. y e. A E. z e. B x = ( y G z ) <-> E. g e. A E. h e. B f = ( g G h ) ) )
39 38 cbvabv 
 |-  { x | E. y e. A E. z e. B x = ( y G z ) } = { f | E. g e. A E. h e. B f = ( g G h ) }
40 30 39 eqtrdi 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A F B ) = { f | E. g e. A E. h e. B f = ( g G h ) } )