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

Metamath Proof Explorer

Theorem drngmul0orOLD

Description: Obsolete version of drngmul0or as of 25-Jun-2025. (Contributed by NM, 8-Oct-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses drngmuleq0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
drngmuleq0.o ⊢ 0 = ( 0g ‘ 𝑅 )
drngmuleq0.t ⊢ · = ( .r ‘ 𝑅 )
drngmuleq0.r ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
drngmuleq0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
drngmuleq0.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion drngmul0orOLD ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 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 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑋 · 𝑌 ) = 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 ) ) )