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 ⊢ 𝑄 = ( ℂfld ↾s ℚ )
Assertion qrngdiv ( ( 𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0 ) → ( 𝑋 ( /r ‘ 𝑄 ) 𝑌 ) = ( 𝑋 / 𝑌 ) )

Proof

Step Hyp Ref Expression
1 qrng.q ⊢ 𝑄 = ( ℂfld ↾s ℚ )
2 qsubdrg ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing )
3 2 simpli ⊢ ℚ ∈ ( SubRing ‘ ℂfld )
4 simp1 ⊢ ( ( 𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0 ) → 𝑋 ∈ ℚ )
5 3simpc ⊢ ( ( 𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0 ) → ( 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0 ) )
6 eldifsn ⊢ ( 𝑌 ∈ ( ℚ ∖ { 0 } ) ↔ ( 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0 ) )
7 5 6 sylibr ⊢ ( ( 𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0 ) → 𝑌 ∈ ( ℚ ∖ { 0 } ) )
8 cnflddiv ⊢ / = ( /r ‘ ℂfld )
9 1 qrngbas ⊢ ℚ = ( Base ‘ 𝑄 )
10 1 qrng0 ⊢ 0 = ( 0g ‘ 𝑄 )
11 1 qdrng ⊢ 𝑄 ∈ DivRing
12 9 10 11 drngui ⊢ ( ℚ ∖ { 0 } ) = ( Unit ‘ 𝑄 )
13 eqid ⊢ ( /r ‘ 𝑄 ) = ( /r ‘ 𝑄 )
14 1 8 12 13 subrgdv ⊢ ( ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ 𝑋 ∈ ℚ ∧ 𝑌 ∈ ( ℚ ∖ { 0 } ) ) → ( 𝑋 / 𝑌 ) = ( 𝑋 ( /r ‘ 𝑄 ) 𝑌 ) )
15 3 4 7 14 mp3an2i ⊢ ( ( 𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 ( /r ‘ 𝑄 ) 𝑌 ) )
16 15 eqcomd ⊢ ( ( 𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0 ) → ( 𝑋 ( /r ‘ 𝑄 ) 𝑌 ) = ( 𝑋 / 𝑌 ) )