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 𝐵 = ( Base ‘ 𝑅 )
drngmuleq0.o 0 = ( 0g𝑅 )
drngmuleq0.t · = ( .r𝑅 )
drngmuleq0.r ( 𝜑𝑅 ∈ DivRing )
drngmuleq0.x ( 𝜑𝑋𝐵 )
drngmuleq0.y ( 𝜑𝑌𝐵 )
Assertion drngmul0or ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0𝑌 = 0 ) ) )

Proof

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