Metamath Proof Explorer

Theorem qrngdiv

Description: The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypothesis qrng.q 
|- Q = ( CCfld |`s QQ )
Assertion qrngdiv 
|- ( ( X e. QQ /\ Y e. QQ /\ Y =/= 0 ) -> ( X ( /r ` Q ) Y ) = ( X / Y ) )

Proof

Step Hyp Ref Expression
1 qrng.q 
 |-  Q = ( CCfld |`s QQ )
2 qsubdrg 
 |-  ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing )
3 2 simpli 
 |-  QQ e. ( SubRing ` CCfld )
4 simp1 
 |-  ( ( X e. QQ /\ Y e. QQ /\ Y =/= 0 ) -> X e. QQ )
5 3simpc 
 |-  ( ( X e. QQ /\ Y e. QQ /\ Y =/= 0 ) -> ( Y e. QQ /\ Y =/= 0 ) )
6 eldifsn 
 |-  ( Y e. ( QQ \ { 0 } ) <-> ( Y e. QQ /\ Y =/= 0 ) )
7 5 6 sylibr 
 |-  ( ( X e. QQ /\ Y e. QQ /\ Y =/= 0 ) -> Y e. ( QQ \ { 0 } ) )
8 cnflddiv 
 |-  / = ( /r ` CCfld )
9 1 qrngbas 
 |-  QQ = ( Base ` Q )
10 1 qrng0 
 |-  0 = ( 0g ` Q )
11 1 qdrng 
 |-  Q e. DivRing
12 9 10 11 drngui 
 |-  ( QQ \ { 0 } ) = ( Unit ` Q )
13 eqid 
 |-  ( /r ` Q ) = ( /r ` Q )
14 1 8 12 13 subrgdv 
 |-  ( ( QQ e. ( SubRing ` CCfld ) /\ X e. QQ /\ Y e. ( QQ \ { 0 } ) ) -> ( X / Y ) = ( X ( /r ` Q ) Y ) )
15 3 4 7 14 mp3an2i 
 |-  ( ( X e. QQ /\ Y e. QQ /\ Y =/= 0 ) -> ( X / Y ) = ( X ( /r ` Q ) Y ) )
16 15 eqcomd 
 |-  ( ( X e. QQ /\ Y e. QQ /\ Y =/= 0 ) -> ( X ( /r ` Q ) Y ) = ( X / Y ) )