Metamath Proof Explorer

Theorem isdomn

Description: Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015)

Ref Expression
Hypotheses isdomn.b 
|- B = ( Base ` R )
isdomn.t 
|- .x. = ( .r ` R )
isdomn.z 
|- .0. = ( 0g ` R )
Assertion isdomn 
|- ( R e. Domn <-> ( R e. NzRing /\ A. x e. B A. y e. B ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )

Proof

Step Hyp Ref Expression
1 isdomn.b 
 |-  B = ( Base ` R )
2 isdomn.t 
 |-  .x. = ( .r ` R )
3 isdomn.z 
 |-  .0. = ( 0g ` R )
4 fvexd 
 |-  ( r = R -> ( Base ` r ) e. _V )
5 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
6 5 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
7 fvexd 
 |-  ( ( r = R /\ b = B ) -> ( 0g ` r ) e. _V )
8 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
9 8 adantr 
 |-  ( ( r = R /\ b = B ) -> ( 0g ` r ) = ( 0g ` R ) )
10 9 3 eqtr4di 
 |-  ( ( r = R /\ b = B ) -> ( 0g ` r ) = .0. )
11 simplr 
 |-  ( ( ( r = R /\ b = B ) /\ z = .0. ) -> b = B )
12 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
13 12 2 eqtr4di 
 |-  ( r = R -> ( .r ` r ) = .x. )
14 13 oveqdr 
 |-  ( ( r = R /\ b = B ) -> ( x ( .r ` r ) y ) = ( x .x. y ) )
15 id 
 |-  ( z = .0. -> z = .0. )
16 14 15 eqeqan12d 
 |-  ( ( ( r = R /\ b = B ) /\ z = .0. ) -> ( ( x ( .r ` r ) y ) = z <-> ( x .x. y ) = .0. ) )
17 eqeq2 
 |-  ( z = .0. -> ( x = z <-> x = .0. ) )
18 eqeq2 
 |-  ( z = .0. -> ( y = z <-> y = .0. ) )
19 17 18 orbi12d 
 |-  ( z = .0. -> ( ( x = z \/ y = z ) <-> ( x = .0. \/ y = .0. ) ) )
20 19 adantl 
 |-  ( ( ( r = R /\ b = B ) /\ z = .0. ) -> ( ( x = z \/ y = z ) <-> ( x = .0. \/ y = .0. ) ) )
21 16 20 imbi12d 
 |-  ( ( ( r = R /\ b = B ) /\ z = .0. ) -> ( ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) <-> ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )
22 11 21 raleqbidv 
 |-  ( ( ( r = R /\ b = B ) /\ z = .0. ) -> ( A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) <-> A. y e. B ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )
23 11 22 raleqbidv 
 |-  ( ( ( r = R /\ b = B ) /\ z = .0. ) -> ( A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) <-> A. x e. B A. y e. B ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )
24 7 10 23 sbcied2 
 |-  ( ( r = R /\ b = B ) -> ( [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) <-> A. x e. B A. y e. B ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )
25 4 6 24 sbcied2 
 |-  ( r = R -> ( [. ( Base ` r ) / b ]. [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) <-> A. x e. B A. y e. B ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )
26 df-domn 
 |-  Domn = { r e. NzRing | [. ( Base ` r ) / b ]. [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) }
27 25 26 elrab2 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A. x e. B A. y e. B ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )