df-dvr

Description: Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014)

		Ref	Expression
	Assertion	df-dvr	$⊢ /_{r} = (r \in V ⟼ (x \in {Base}_{r}, y \in Unit (r) ⟼ x \cdot_{r} {inv}_{r} (r) (y)))$

Step	Hyp	Ref	Expression
0		cdvr	$class /_{r}$
1		vr	$setvar r$
2		cvv	$class V$
3		vx	$setvar x$
4		cbs	$class Base$
5	1	cv	$setvar r$
6	5 4	cfv	$class {Base}_{r}$
7		vy	$setvar y$
8		cui	$class Unit$
9	5 8	cfv	$class Unit (r)$
10	3	cv	$setvar x$
11		cmulr	$class \cdot_{𝑟}$
12	5 11	cfv	$class \cdot_{r}$
13		cinvr	$class {inv}_{r}$
14	5 13	cfv	$class {inv}_{r} (r)$
15	7	cv	$setvar y$
16	15 14	cfv	$class {inv}_{r} (r) (y)$
17	10 16 12	co	$class (x \cdot_{r} {inv}_{r} (r) (y))$
18	3 7 6 9 17	cmpo	$class (x \in {Base}_{r}, y \in Unit (r) ⟼ x \cdot_{r} {inv}_{r} (r) (y))$
19	1 2 18	cmpt	$class (r \in V ⟼ (x \in {Base}_{r}, y \in Unit (r) ⟼ x \cdot_{r} {inv}_{r} (r) (y)))$
20	0 19	wceq	$wff /_{r} = (r \in V ⟼ (x \in {Base}_{r}, y \in Unit (r) ⟼ x \cdot_{r} {inv}_{r} (r) (y)))$

Metamath Proof Explorer