Metamath Proof Explorer

Theorem sca2rab

Description: If B is a scale of A by C , then A is a scale of B by 1 / C . (Contributed by Mario Carneiro, 22-Mar-2014)

Ref Expression
Hypotheses ovolsca.1 
|- ( ph -> A C_ RR )
ovolsca.2 
|- ( ph -> C e. RR+ )
ovolsca.3 
|- ( ph -> B = { x e. RR | ( C x. x ) e. A } )
Assertion sca2rab 
|- ( ph -> A = { y e. RR | ( ( 1 / C ) x. y ) e. B } )

Proof

Step Hyp Ref Expression
1 ovolsca.1 
 |-  ( ph -> A C_ RR )
2 ovolsca.2 
 |-  ( ph -> C e. RR+ )
3 ovolsca.3 
 |-  ( ph -> B = { x e. RR | ( C x. x ) e. A } )
4 1 sseld 
 |-  ( ph -> ( y e. A -> y e. RR ) )
5 4 pm4.71rd 
 |-  ( ph -> ( y e. A <-> ( y e. RR /\ y e. A ) ) )
6 3 adantr 
 |-  ( ( ph /\ y e. RR ) -> B = { x e. RR | ( C x. x ) e. A } )
7 6 eleq2d 
 |-  ( ( ph /\ y e. RR ) -> ( ( ( 1 / C ) x. y ) e. B <-> ( ( 1 / C ) x. y ) e. { x e. RR | ( C x. x ) e. A } ) )
8 2 adantr 
 |-  ( ( ph /\ y e. RR ) -> C e. RR+ )
9 8 rprecred 
 |-  ( ( ph /\ y e. RR ) -> ( 1 / C ) e. RR )
10 remulcl 
 |-  ( ( ( 1 / C ) e. RR /\ y e. RR ) -> ( ( 1 / C ) x. y ) e. RR )
11 9 10 sylancom 
 |-  ( ( ph /\ y e. RR ) -> ( ( 1 / C ) x. y ) e. RR )
12 oveq2 
 |-  ( x = ( ( 1 / C ) x. y ) -> ( C x. x ) = ( C x. ( ( 1 / C ) x. y ) ) )
13 12 eleq1d 
 |-  ( x = ( ( 1 / C ) x. y ) -> ( ( C x. x ) e. A <-> ( C x. ( ( 1 / C ) x. y ) ) e. A ) )
14 13 elrab3 
 |-  ( ( ( 1 / C ) x. y ) e. RR -> ( ( ( 1 / C ) x. y ) e. { x e. RR | ( C x. x ) e. A } <-> ( C x. ( ( 1 / C ) x. y ) ) e. A ) )
15 11 14 syl 
 |-  ( ( ph /\ y e. RR ) -> ( ( ( 1 / C ) x. y ) e. { x e. RR | ( C x. x ) e. A } <-> ( C x. ( ( 1 / C ) x. y ) ) e. A ) )
16 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
17 16 recnd 
 |-  ( ( ph /\ y e. RR ) -> y e. CC )
18 8 rpcnd 
 |-  ( ( ph /\ y e. RR ) -> C e. CC )
19 8 rpne0d 
 |-  ( ( ph /\ y e. RR ) -> C =/= 0 )
20 17 18 19 divrec2d 
 |-  ( ( ph /\ y e. RR ) -> ( y / C ) = ( ( 1 / C ) x. y ) )
21 20 oveq2d 
 |-  ( ( ph /\ y e. RR ) -> ( C x. ( y / C ) ) = ( C x. ( ( 1 / C ) x. y ) ) )
22 17 18 19 divcan2d 
 |-  ( ( ph /\ y e. RR ) -> ( C x. ( y / C ) ) = y )
23 21 22 eqtr3d 
 |-  ( ( ph /\ y e. RR ) -> ( C x. ( ( 1 / C ) x. y ) ) = y )
24 23 eleq1d 
 |-  ( ( ph /\ y e. RR ) -> ( ( C x. ( ( 1 / C ) x. y ) ) e. A <-> y e. A ) )
25 7 15 24 3bitrd 
 |-  ( ( ph /\ y e. RR ) -> ( ( ( 1 / C ) x. y ) e. B <-> y e. A ) )
26 25 pm5.32da 
 |-  ( ph -> ( ( y e. RR /\ ( ( 1 / C ) x. y ) e. B ) <-> ( y e. RR /\ y e. A ) ) )
27 5 26 bitr4d 
 |-  ( ph -> ( y e. A <-> ( y e. RR /\ ( ( 1 / C ) x. y ) e. B ) ) )
28 27 abbi2dv 
 |-  ( ph -> A = { y | ( y e. RR /\ ( ( 1 / C ) x. y ) e. B ) } )
29 df-rab 
 |-  { y e. RR | ( ( 1 / C ) x. y ) e. B } = { y | ( y e. RR /\ ( ( 1 / C ) x. y ) e. B ) }
30 28 29 eqtr4di 
 |-  ( ph -> A = { y e. RR | ( ( 1 / C ) x. y ) e. B } )