Theorem dvrval 20205

Description: Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)

Hypotheses

Ref	Expression
dvrval.b	⊢ 𝐵 = (Base‘𝑅)
dvrval.t	⊢ · = (.r‘𝑅)
dvrval.u	⊢ 𝑈 = (Unit‘𝑅)
dvrval.i	⊢ 𝐼 = (invr‘𝑅)
dvrval.d	⊢ / = (/r‘𝑅)

Assertion

Ref	Expression
dvrval	⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋 · (𝐼‘𝑌)))

Proof of Theorem dvrval

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7410	. 2 ⊢ (𝑥 = 𝑋 → (𝑥 · (𝐼‘𝑦)) = (𝑋 · (𝐼‘𝑦)))
2		fveq2 6887	. . 3 ⊢ (𝑦 = 𝑌 → (𝐼‘𝑦) = (𝐼‘𝑌))
3	2	oveq2d 7419	. 2 ⊢ (𝑦 = 𝑌 → (𝑋 · (𝐼‘𝑦)) = (𝑋 · (𝐼‘𝑌)))
4		dvrval.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
5		dvrval.t	. . 3 ⊢ · = (.r‘𝑅)
6		dvrval.u	. . 3 ⊢ 𝑈 = (Unit‘𝑅)
7		dvrval.i	. . 3 ⊢ 𝐼 = (invr‘𝑅)
8		dvrval.d	. . 3 ⊢ / = (/r‘𝑅)
9	4, 5, 6, 7, 8	dvrfval 20204	. 2 ⊢ / = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))
10		ovex 7436	. 2 ⊢ (𝑋 · (𝐼‘𝑌)) ∈ V
11	1, 3, 9, 10	ovmpo 7562	1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋 · (𝐼‘𝑌)))

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ‘cfv 6539  (class class class)co 7403  Basecbs 17139  ._rcmulr 17193  Unitcui 20157  inv_rcinvr 20189  /_rcdvr 20202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5283  ax-sep 5297  ax-nul 5304  ax-pow 5361  ax-pr 5425  ax-un 7719

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4527  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4907  df-iun 4997  df-br 5147  df-opab 5209  df-mpt 5230  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6491  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7406  df-oprab 7407  df-mpo 7408  df-1st 7969  df-2nd 7970  df-dvr 20203

This theorem is referenced by:  dvrcl  20206  unitdvcl  20207  dvrid  20208  dvr1  20209  dvrass  20210  dvrcan1  20211  dvrdir  20214  rdivmuldivd  20215  ringinvdv  20216  subrgdv  20367  abvdiv  20432  cnflddiv  20959  nmdvr  24168  sum2dchr  26756  dvrcan5  32359