Metamath Proof Explorer

Theorem xdivval

Description: Value of division: the (unique) element x such that ( B x. x ) = A . This is meaningful only when B is nonzero. (Contributed by Thierry Arnoux, 17-Dec-2016)

Ref Expression
Assertion xdivval 
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( A /e B ) = ( iota_ x e. RR* ( B *e x ) = A ) )

Proof

Step Hyp Ref Expression
1 eldifsn 
 |-  ( B e. ( RR \ { 0 } ) <-> ( B e. RR /\ B =/= 0 ) )
2 simpl 
 |-  ( ( y = A /\ x e. RR* ) -> y = A )
3 2 eqeq2d 
 |-  ( ( y = A /\ x e. RR* ) -> ( ( z *e x ) = y <-> ( z *e x ) = A ) )
4 3 riotabidva 
 |-  ( y = A -> ( iota_ x e. RR* ( z *e x ) = y ) = ( iota_ x e. RR* ( z *e x ) = A ) )
5 simpl 
 |-  ( ( z = B /\ x e. RR* ) -> z = B )
6 5 oveq1d 
 |-  ( ( z = B /\ x e. RR* ) -> ( z *e x ) = ( B *e x ) )
7 6 eqeq1d 
 |-  ( ( z = B /\ x e. RR* ) -> ( ( z *e x ) = A <-> ( B *e x ) = A ) )
8 7 riotabidva 
 |-  ( z = B -> ( iota_ x e. RR* ( z *e x ) = A ) = ( iota_ x e. RR* ( B *e x ) = A ) )
9 df-xdiv 
 |-  /e = ( y e. RR* , z e. ( RR \ { 0 } ) |-> ( iota_ x e. RR* ( z *e x ) = y ) )
10 riotaex 
 |-  ( iota_ x e. RR* ( B *e x ) = A ) e. _V
11 4 8 9 10 ovmpo 
 |-  ( ( A e. RR* /\ B e. ( RR \ { 0 } ) ) -> ( A /e B ) = ( iota_ x e. RR* ( B *e x ) = A ) )
12 1 11 sylan2br 
 |-  ( ( A e. RR* /\ ( B e. RR /\ B =/= 0 ) ) -> ( A /e B ) = ( iota_ x e. RR* ( B *e x ) = A ) )
13 12 3impb 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( A /e B ) = ( iota_ x e. RR* ( B *e x ) = A ) )