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

Metamath Proof Explorer

Theorem ringinvnzdiv

Description: In a unital ring, a left invertible element is not a zero divisor. (Contributed by FL, 18-Apr-2010) (Revised by Jeff Madsen, 18-Apr-2010) (Revised by AV, 24-Aug-2021)

Ref Expression
Hypotheses ringinvnzdiv.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringinvnzdiv.t ⊢ · = ( .r ‘ 𝑅 )
ringinvnzdiv.u ⊢ 1 = ( 1r ‘ 𝑅 )
ringinvnzdiv.z ⊢ 0 = ( 0g ‘ 𝑅 )
ringinvnzdiv.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ringinvnzdiv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
ringinvnzdiv.a ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝐵 ( 𝑎 · 𝑋 ) = 1 )
ringinvnzdiv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion ringinvnzdiv ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ 𝑌 = 0 ) )

Proof

Step Hyp Ref Expression
1 ringinvnzdiv.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringinvnzdiv.t ⊢ · = ( .r ‘ 𝑅 )
3 ringinvnzdiv.u ⊢ 1 = ( 1r ‘ 𝑅 )
4 ringinvnzdiv.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 ringinvnzdiv.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 ringinvnzdiv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 ringinvnzdiv.a ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝐵 ( 𝑎 · 𝑋 ) = 1 )
8 ringinvnzdiv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 1 2 3 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) → ( 1 · 𝑌 ) = 𝑌 )
10 5 8 9 syl2anc ⊢ ( 𝜑 → ( 1 · 𝑌 ) = 𝑌 )
11 10 eqcomd ⊢ ( 𝜑 → 𝑌 = ( 1 · 𝑌 ) )
12 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) ∧ ( 𝑋 · 𝑌 ) = 0 ) → 𝑌 = ( 1 · 𝑌 ) )
13 oveq1 ⊢ ( 1 = ( 𝑎 · 𝑋 ) → ( 1 · 𝑌 ) = ( ( 𝑎 · 𝑋 ) · 𝑌 ) )
14 13 eqcoms ⊢ ( ( 𝑎 · 𝑋 ) = 1 → ( 1 · 𝑌 ) = ( ( 𝑎 · 𝑋 ) · 𝑌 ) )
15 14 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) → ( 1 · 𝑌 ) = ( ( 𝑎 · 𝑋 ) · 𝑌 ) )
16 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑅 ∈ Ring )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
18 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
19 8 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
20 17 18 19 3jca ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
21 16 20 jca ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑅 ∈ Ring ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) )
22 21 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) → ( 𝑅 ∈ Ring ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) )
23 1 2 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑎 · 𝑋 ) · 𝑌 ) = ( 𝑎 · ( 𝑋 · 𝑌 ) ) )
24 22 23 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) → ( ( 𝑎 · 𝑋 ) · 𝑌 ) = ( 𝑎 · ( 𝑋 · 𝑌 ) ) )
25 15 24 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) → ( 1 · 𝑌 ) = ( 𝑎 · ( 𝑋 · 𝑌 ) ) )
26 25 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) ∧ ( 𝑋 · 𝑌 ) = 0 ) → ( 1 · 𝑌 ) = ( 𝑎 · ( 𝑋 · 𝑌 ) ) )
27 oveq2 ⊢ ( ( 𝑋 · 𝑌 ) = 0 → ( 𝑎 · ( 𝑋 · 𝑌 ) ) = ( 𝑎 · 0 ) )
28 1 2 4 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 · 0 ) = 0 )
29 5 28 sylan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 · 0 ) = 0 )
30 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) → ( 𝑎 · 0 ) = 0 )
31 27 30 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) ∧ ( 𝑋 · 𝑌 ) = 0 ) → ( 𝑎 · ( 𝑋 · 𝑌 ) ) = 0 )
32 12 26 31 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) ∧ ( 𝑋 · 𝑌 ) = 0 ) → 𝑌 = 0 )
33 32 exp31 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑎 · 𝑋 ) = 1 → ( ( 𝑋 · 𝑌 ) = 0 → 𝑌 = 0 ) ) )
34 33 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐵 ( 𝑎 · 𝑋 ) = 1 → ( ( 𝑋 · 𝑌 ) = 0 → 𝑌 = 0 ) ) )
35 7 34 mpd ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 → 𝑌 = 0 ) )
36 oveq2 ⊢ ( 𝑌 = 0 → ( 𝑋 · 𝑌 ) = ( 𝑋 · 0 ) )
37 1 2 4 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · 0 ) = 0 )
38 5 6 37 syl2anc ⊢ ( 𝜑 → ( 𝑋 · 0 ) = 0 )
39 36 38 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑌 = 0 ) → ( 𝑋 · 𝑌 ) = 0 )
40 39 ex ⊢ ( 𝜑 → ( 𝑌 = 0 → ( 𝑋 · 𝑌 ) = 0 ) )
41 35 40 impbid ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ 𝑌 = 0 ) )