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 ˙ = 0 R
drngmuleq0.t · ˙ = R
drngmuleq0.r φ R DivRing
drngmuleq0.x φ X B
drngmuleq0.y φ Y B
Assertion drngmul0or φ X · ˙ Y = 0 ˙ X = 0 ˙ Y = 0 ˙

Proof

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