Definition df-apr 13961

Description: The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 13966. (Contributed by Jim Kingdon, 13-Feb-2025.)

Assertion

Ref	Expression
df-apr	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )

Distinct variable group:   x, w, y

Detailed syntax breakdown of Definition df-apr

Step	Hyp	Ref	Expression
1		capr 13960	. 2 class #r
2		vw	. . 3 setvar w
3		cvv 2771	. . 3 class _V
4		vx	. . . . . . . 8 setvar x
5	4	cv 1371	. . . . . . 7 class x
6	2	cv 1371	. . . . . . . 8 class w
7		cbs 12751	. . . . . . . 8 class Base
8	6, 7	cfv 5268	. . . . . . 7 class ( Base ` w )
9	5, 8	wcel 2175	. . . . . 6 wff x e. ( Base ` w )
10		vy	. . . . . . . 8 setvar y
11	10	cv 1371	. . . . . . 7 class y
12	11, 8	wcel 2175	. . . . . 6 wff y e. ( Base ` w )
13	9, 12	wa 104	. . . . 5 wff ( x e. ( Base ` w ) /\ y e. ( Base ` w ) )
14		csg 13252	. . . . . . . 8 class -g
15	6, 14	cfv 5268	. . . . . . 7 class ( -g ` w )
16	5, 11, 15	co 5934	. . . . . 6 class ( x ( -g ` w ) y )
17		cui 13767	. . . . . . 7 class Unit
18	6, 17	cfv 5268	. . . . . 6 class (Unit ` w )
19	16, 18	wcel 2175	. . . . 5 wff ( x ( -g ` w ) y ) e. (Unit ` w )
20	13, 19	wa 104	. . . 4 wff ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) )
21	20, 4, 10	copab 4103	. . 3 class { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) }
22	2, 3, 21	cmpt 4104	. 2 class ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
23	1, 22	wceq 1372	1 wff #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )

This definition is referenced by:  aprval  13962  aprap  13966