Metamath Proof Explorer

Theorem drngmul0or

Description: A product is zero iff one of its factors is zero. (Contributed by NM, 8-Oct-2014)

Ref Expression
Hypotheses drngmuleq0.b 
|- B = ( Base ` R )
drngmuleq0.o 
|- .0. = ( 0g ` R )
drngmuleq0.t 
|- .x. = ( .r ` R )
drngmuleq0.r 
|- ( ph -> R e. DivRing )
drngmuleq0.x 
|- ( ph -> X e. B )
drngmuleq0.y 
|- ( ph -> Y e. B )
Assertion drngmul0or 
|- ( ph -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )

Proof

Step Hyp Ref Expression
1 drngmuleq0.b 
 |-  B = ( Base ` R )
2 drngmuleq0.o 
 |-  .0. = ( 0g ` R )
3 drngmuleq0.t 
 |-  .x. = ( .r ` R )
4 drngmuleq0.r 
 |-  ( ph -> R e. DivRing )
5 drngmuleq0.x 
 |-  ( ph -> X e. B )
6 drngmuleq0.y 
 |-  ( ph -> Y e. B )
7 df-ne 
 |-  ( X =/= .0. <-> -. X = .0. )
8 oveq2 
 |-  ( ( X .x. Y ) = .0. -> ( ( ( invr ` R ) ` X ) .x. ( X .x. Y ) ) = ( ( ( invr ` R ) ` X ) .x. .0. ) )
9 8 ad2antlr 
 |-  ( ( ( ph /\ ( X .x. Y ) = .0. ) /\ X =/= .0. ) -> ( ( ( invr ` R ) ` X ) .x. ( X .x. Y ) ) = ( ( ( invr ` R ) ` X ) .x. .0. ) )
10 4 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> R e. DivRing )
11 5 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> X e. B )
12 simpr 
 |-  ( ( ph /\ X =/= .0. ) -> X =/= .0. )
13 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
14 eqid 
 |-  ( invr ` R ) = ( invr ` R )
15 1 2 3 13 14 drnginvrl 
 |-  ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( ( ( invr ` R ) ` X ) .x. X ) = ( 1r ` R ) )
16 10 11 12 15 syl3anc 
 |-  ( ( ph /\ X =/= .0. ) -> ( ( ( invr ` R ) ` X ) .x. X ) = ( 1r ` R ) )
17 16 oveq1d 
 |-  ( ( ph /\ X =/= .0. ) -> ( ( ( ( invr ` R ) ` X ) .x. X ) .x. Y ) = ( ( 1r ` R ) .x. Y ) )
18 drngring 
 |-  ( R e. DivRing -> R e. Ring )
19 4 18 syl 
 |-  ( ph -> R e. Ring )
20 19 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> R e. Ring )
21 1 2 14 drnginvrcl 
 |-  ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( ( invr ` R ) ` X ) e. B )
22 10 11 12 21 syl3anc 
 |-  ( ( ph /\ X =/= .0. ) -> ( ( invr ` R ) ` X ) e. B )
23 6 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> Y e. B )
24 1 3 ringass 
 |-  ( ( R e. Ring /\ ( ( ( invr ` R ) ` X ) e. B /\ X e. B /\ Y e. B ) ) -> ( ( ( ( invr ` R ) ` X ) .x. X ) .x. Y ) = ( ( ( invr ` R ) ` X ) .x. ( X .x. Y ) ) )
25 20 22 11 23 24 syl13anc 
 |-  ( ( ph /\ X =/= .0. ) -> ( ( ( ( invr ` R ) ` X ) .x. X ) .x. Y ) = ( ( ( invr ` R ) ` X ) .x. ( X .x. Y ) ) )
26 1 3 13 ringlidm 
 |-  ( ( R e. Ring /\ Y e. B ) -> ( ( 1r ` R ) .x. Y ) = Y )
27 19 6 26 syl2anc 
 |-  ( ph -> ( ( 1r ` R ) .x. Y ) = Y )
28 27 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> ( ( 1r ` R ) .x. Y ) = Y )
29 17 25 28 3eqtr3d 
 |-  ( ( ph /\ X =/= .0. ) -> ( ( ( invr ` R ) ` X ) .x. ( X .x. Y ) ) = Y )
30 29 adantlr 
 |-  ( ( ( ph /\ ( X .x. Y ) = .0. ) /\ X =/= .0. ) -> ( ( ( invr ` R ) ` X ) .x. ( X .x. Y ) ) = Y )
31 19 adantr 
 |-  ( ( ph /\ ( X .x. Y ) = .0. ) -> R e. Ring )
32 31 adantr 
 |-  ( ( ( ph /\ ( X .x. Y ) = .0. ) /\ X =/= .0. ) -> R e. Ring )
33 22 adantlr 
 |-  ( ( ( ph /\ ( X .x. Y ) = .0. ) /\ X =/= .0. ) -> ( ( invr ` R ) ` X ) e. B )
34 1 3 2 ringrz 
 |-  ( ( R e. Ring /\ ( ( invr ` R ) ` X ) e. B ) -> ( ( ( invr ` R ) ` X ) .x. .0. ) = .0. )
35 32 33 34 syl2anc 
 |-  ( ( ( ph /\ ( X .x. Y ) = .0. ) /\ X =/= .0. ) -> ( ( ( invr ` R ) ` X ) .x. .0. ) = .0. )
36 9 30 35 3eqtr3d 
 |-  ( ( ( ph /\ ( X .x. Y ) = .0. ) /\ X =/= .0. ) -> Y = .0. )
37 36 ex 
 |-  ( ( ph /\ ( X .x. Y ) = .0. ) -> ( X =/= .0. -> Y = .0. ) )
38 7 37 syl5bir 
 |-  ( ( ph /\ ( X .x. Y ) = .0. ) -> ( -. X = .0. -> Y = .0. ) )
39 38 orrd 
 |-  ( ( ph /\ ( X .x. Y ) = .0. ) -> ( X = .0. \/ Y = .0. ) )
40 39 ex 
 |-  ( ph -> ( ( X .x. Y ) = .0. -> ( X = .0. \/ Y = .0. ) ) )
41 1 3 2 ringlz 
 |-  ( ( R e. Ring /\ Y e. B ) -> ( .0. .x. Y ) = .0. )
42 19 6 41 syl2anc 
 |-  ( ph -> ( .0. .x. Y ) = .0. )
43 oveq1 
 |-  ( X = .0. -> ( X .x. Y ) = ( .0. .x. Y ) )
44 43 eqeq1d 
 |-  ( X = .0. -> ( ( X .x. Y ) = .0. <-> ( .0. .x. Y ) = .0. ) )
45 42 44 syl5ibrcom 
 |-  ( ph -> ( X = .0. -> ( X .x. Y ) = .0. ) )
46 1 3 2 ringrz 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = .0. )
47 19 5 46 syl2anc 
 |-  ( ph -> ( X .x. .0. ) = .0. )
48 oveq2 
 |-  ( Y = .0. -> ( X .x. Y ) = ( X .x. .0. ) )
49 48 eqeq1d 
 |-  ( Y = .0. -> ( ( X .x. Y ) = .0. <-> ( X .x. .0. ) = .0. ) )
50 47 49 syl5ibrcom 
 |-  ( ph -> ( Y = .0. -> ( X .x. Y ) = .0. ) )
51 45 50 jaod 
 |-  ( ph -> ( ( X = .0. \/ Y = .0. ) -> ( X .x. Y ) = .0. ) )
52 40 51 impbid 
 |-  ( ph -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )