Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-zd Unicode version

Definition df-zd 25442
Description: Definition of the zero divisors of a ring. Experimental. (Contributed by FL, 27-Jun-2011.)
Assertion
Ref Expression
df-zd  |-  zeroDiv  =  { <. r ,  y >.  |  y  =  {
a  e.  ran  ( 1st `  r )  |  ( a  =/=  (GId `  ( 1st `  r
) )  /\  E. b  e.  ran  ( 1st `  r ) ( b  =/=  (GId `  ( 1st `  r ) )  /\  ( a ( 2nd `  r ) b )  =  (GId
`  ( 1st `  r
) ) ) ) } }
Distinct variable group:    y, r, a, b

Detailed syntax breakdown of Definition df-zd
StepHypRef Expression
1 czerodiv 25441 . 2  class  zeroDiv
2 vy . . . . 5  set  y
32cv 1622 . . . 4  class  y
4 va . . . . . . . 8  set  a
54cv 1622 . . . . . . 7  class  a
6 vr . . . . . . . . . 10  set  r
76cv 1622 . . . . . . . . 9  class  r
8 c1st 6120 . . . . . . . . 9  class  1st
97, 8cfv 5255 . . . . . . . 8  class  ( 1st `  r )
10 cgi 20854 . . . . . . . 8  class GId
119, 10cfv 5255 . . . . . . 7  class  (GId `  ( 1st `  r ) )
125, 11wne 2446 . . . . . 6  wff  a  =/=  (GId `  ( 1st `  r ) )
13 vb . . . . . . . . . 10  set  b
1413cv 1622 . . . . . . . . 9  class  b
1514, 11wne 2446 . . . . . . . 8  wff  b  =/=  (GId `  ( 1st `  r ) )
16 c2nd 6121 . . . . . . . . . . 11  class  2nd
177, 16cfv 5255 . . . . . . . . . 10  class  ( 2nd `  r )
185, 14, 17co 5858 . . . . . . . . 9  class  ( a ( 2nd `  r
) b )
1918, 11wceq 1623 . . . . . . . 8  wff  ( a ( 2nd `  r
) b )  =  (GId `  ( 1st `  r ) )
2015, 19wa 358 . . . . . . 7  wff  ( b  =/=  (GId `  ( 1st `  r ) )  /\  ( a ( 2nd `  r ) b )  =  (GId
`  ( 1st `  r
) ) )
219crn 4690 . . . . . . 7  class  ran  ( 1st `  r )
2220, 13, 21wrex 2544 . . . . . 6  wff  E. b  e.  ran  ( 1st `  r
) ( b  =/=  (GId `  ( 1st `  r ) )  /\  ( a ( 2nd `  r ) b )  =  (GId `  ( 1st `  r ) ) )
2312, 22wa 358 . . . . 5  wff  ( a  =/=  (GId `  ( 1st `  r ) )  /\  E. b  e. 
ran  ( 1st `  r
) ( b  =/=  (GId `  ( 1st `  r ) )  /\  ( a ( 2nd `  r ) b )  =  (GId `  ( 1st `  r ) ) ) )
2423, 4, 21crab 2547 . . . 4  class  { a  e.  ran  ( 1st `  r )  |  ( a  =/=  (GId `  ( 1st `  r ) )  /\  E. b  e.  ran  ( 1st `  r
) ( b  =/=  (GId `  ( 1st `  r ) )  /\  ( a ( 2nd `  r ) b )  =  (GId `  ( 1st `  r ) ) ) ) }
253, 24wceq 1623 . . 3  wff  y  =  { a  e.  ran  ( 1st `  r )  |  ( a  =/=  (GId `  ( 1st `  r ) )  /\  E. b  e.  ran  ( 1st `  r ) ( b  =/=  (GId `  ( 1st `  r ) )  /\  ( a ( 2nd `  r
) b )  =  (GId `  ( 1st `  r ) ) ) ) }
2625, 6, 2copab 4076 . 2  class  { <. r ,  y >.  |  y  =  { a  e. 
ran  ( 1st `  r
)  |  ( a  =/=  (GId `  ( 1st `  r ) )  /\  E. b  e. 
ran  ( 1st `  r
) ( b  =/=  (GId `  ( 1st `  r ) )  /\  ( a ( 2nd `  r ) b )  =  (GId `  ( 1st `  r ) ) ) ) } }
271, 26wceq 1623 1  wff  zeroDiv  =  { <. r ,  y >.  |  y  =  {
a  e.  ran  ( 1st `  r )  |  ( a  =/=  (GId `  ( 1st `  r
) )  /\  E. b  e.  ran  ( 1st `  r ) ( b  =/=  (GId `  ( 1st `  r ) )  /\  ( a ( 2nd `  r ) b )  =  (GId
`  ( 1st `  r
) ) ) ) } }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator