Metamath Proof Explorer

Theorem idomnzd

Description: A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by AV, 12-Jul-2026)

Ref Expression
Hypotheses isidom3.b 
|- B = ( Base ` R )
isidom3.t 
|- .x. = ( .r ` R )
isidom3.0 
|- .0. = ( 0g ` R )
Assertion idomnzd 
|- ( ( R e. IDomn /\ ( X e. B /\ Y e. B /\ ( X .x. Y ) = .0. ) ) -> ( X = .0. \/ Y = .0. ) )

Proof

Step Hyp Ref Expression
1 isidom3.b 
 |-  B = ( Base ` R )
2 isidom3.t 
 |-  .x. = ( .r ` R )
3 isidom3.0 
 |-  .0. = ( 0g ` R )
4 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
5 1 2 3 4 isidom3 
 |-  ( R e. IDomn <-> ( R e. CRing /\ .0. =/= ( 1r ` R ) /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) )
6 5 simp3bi 
 |-  ( R e. IDomn -> A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) )
7 oveq1 
 |-  ( a = X -> ( a .x. b ) = ( X .x. b ) )
8 7 eqeq1d 
 |-  ( a = X -> ( ( a .x. b ) = .0. <-> ( X .x. b ) = .0. ) )
9 eqeq1 
 |-  ( a = X -> ( a = .0. <-> X = .0. ) )
10 9 orbi1d 
 |-  ( a = X -> ( ( a = .0. \/ b = .0. ) <-> ( X = .0. \/ b = .0. ) ) )
11 8 10 imbi12d 
 |-  ( a = X -> ( ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) <-> ( ( X .x. b ) = .0. -> ( X = .0. \/ b = .0. ) ) ) )
12 oveq2 
 |-  ( b = Y -> ( X .x. b ) = ( X .x. Y ) )
13 12 eqeq1d 
 |-  ( b = Y -> ( ( X .x. b ) = .0. <-> ( X .x. Y ) = .0. ) )
14 eqeq1 
 |-  ( b = Y -> ( b = .0. <-> Y = .0. ) )
15 14 orbi2d 
 |-  ( b = Y -> ( ( X = .0. \/ b = .0. ) <-> ( X = .0. \/ Y = .0. ) ) )
16 13 15 imbi12d 
 |-  ( b = Y -> ( ( ( X .x. b ) = .0. -> ( X = .0. \/ b = .0. ) ) <-> ( ( X .x. Y ) = .0. -> ( X = .0. \/ Y = .0. ) ) ) )
17 11 16 rspc2v 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) -> ( ( X .x. Y ) = .0. -> ( X = .0. \/ Y = .0. ) ) ) )
18 6 17 syl5com 
 |-  ( R e. IDomn -> ( ( X e. B /\ Y e. B ) -> ( ( X .x. Y ) = .0. -> ( X = .0. \/ Y = .0. ) ) ) )
19 18 expd 
 |-  ( R e. IDomn -> ( X e. B -> ( Y e. B -> ( ( X .x. Y ) = .0. -> ( X = .0. \/ Y = .0. ) ) ) ) )
20 19 3imp2 
 |-  ( ( R e. IDomn /\ ( X e. B /\ Y e. B /\ ( X .x. Y ) = .0. ) ) -> ( X = .0. \/ Y = .0. ) )