This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem domneq0

Description: In a domain, a product is zero iff it has a zero factor. (Contributed by Mario Carneiro, 28-Mar-2015)

Ref Expression
Hypotheses domneq0.b 
|- B = ( Base ` R )
domneq0.t 
|- .x. = ( .r ` R )
domneq0.z 
|- .0. = ( 0g ` R )
Assertion domneq0 
|- ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )

Proof

Step Hyp Ref Expression
1 domneq0.b 
 |-  B = ( Base ` R )
2 domneq0.t 
 |-  .x. = ( .r ` R )
3 domneq0.z 
 |-  .0. = ( 0g ` R )
4 3simpc 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( X e. B /\ Y e. B ) )
5 1 2 3 isdomn 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A. x e. B A. y e. B ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )
6 5 simprbi 
 |-  ( R e. Domn -> A. x e. B A. y e. B ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) )
7 6 3ad2ant1 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> A. x e. B A. y e. B ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) )
8 oveq1 
 |-  ( x = X -> ( x .x. y ) = ( X .x. y ) )
9 8 eqeq1d 
 |-  ( x = X -> ( ( x .x. y ) = .0. <-> ( X .x. y ) = .0. ) )
10 eqeq1 
 |-  ( x = X -> ( x = .0. <-> X = .0. ) )
11 10 orbi1d 
 |-  ( x = X -> ( ( x = .0. \/ y = .0. ) <-> ( X = .0. \/ y = .0. ) ) )
12 9 11 imbi12d 
 |-  ( x = X -> ( ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) <-> ( ( X .x. y ) = .0. -> ( X = .0. \/ y = .0. ) ) ) )
13 oveq2 
 |-  ( y = Y -> ( X .x. y ) = ( X .x. Y ) )
14 13 eqeq1d 
 |-  ( y = Y -> ( ( X .x. y ) = .0. <-> ( X .x. Y ) = .0. ) )
15 eqeq1 
 |-  ( y = Y -> ( y = .0. <-> Y = .0. ) )
16 15 orbi2d 
 |-  ( y = Y -> ( ( X = .0. \/ y = .0. ) <-> ( X = .0. \/ Y = .0. ) ) )
17 14 16 imbi12d 
 |-  ( y = Y -> ( ( ( X .x. y ) = .0. -> ( X = .0. \/ y = .0. ) ) <-> ( ( X .x. Y ) = .0. -> ( X = .0. \/ Y = .0. ) ) ) )
18 12 17 rspc2va 
 |-  ( ( ( X e. B /\ Y e. B ) /\ A. x e. B A. y e. B ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) -> ( ( X .x. Y ) = .0. -> ( X = .0. \/ Y = .0. ) ) )
19 4 7 18 syl2anc 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) = .0. -> ( X = .0. \/ Y = .0. ) ) )
20 domnring 
 |-  ( R e. Domn -> R e. Ring )
21 20 3ad2ant1 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> R e. Ring )
22 simp3 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> Y e. B )
23 1 2 3 ringlz 
 |-  ( ( R e. Ring /\ Y e. B ) -> ( .0. .x. Y ) = .0. )
24 21 22 23 syl2anc 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( .0. .x. Y ) = .0. )
25 oveq1 
 |-  ( X = .0. -> ( X .x. Y ) = ( .0. .x. Y ) )
26 25 eqeq1d 
 |-  ( X = .0. -> ( ( X .x. Y ) = .0. <-> ( .0. .x. Y ) = .0. ) )
27 24 26 syl5ibrcom 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( X = .0. -> ( X .x. Y ) = .0. ) )
28 simp2 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> X e. B )
29 1 2 3 ringrz 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = .0. )
30 21 28 29 syl2anc 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( X .x. .0. ) = .0. )
31 oveq2 
 |-  ( Y = .0. -> ( X .x. Y ) = ( X .x. .0. ) )
32 31 eqeq1d 
 |-  ( Y = .0. -> ( ( X .x. Y ) = .0. <-> ( X .x. .0. ) = .0. ) )
33 30 32 syl5ibrcom 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( Y = .0. -> ( X .x. Y ) = .0. ) )
34 27 33 jaod 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( ( X = .0. \/ Y = .0. ) -> ( X .x. Y ) = .0. ) )
35 19 34 impbid 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )