Metamath Proof Explorer

Theorem ringinvnz1ne0

Description: In a unitary ring, a left invertible element is different from zero iff .1. =/= .0. . (Contributed by FL, 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 )
Assertion ringinvnz1ne0 ( 𝜑 → ( 𝑋 ≠ 0 ↔ 1 ≠ 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 oveq2 ⊢ ( 𝑋 = 0 → ( 𝑎 · 𝑋 ) = ( 𝑎 · 0 ) )
9 1 2 4 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 · 0 ) = 0 )
10 5 9 sylan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 · 0 ) = 0 )
11 eqeq12 ⊢ ( ( ( 𝑎 · 𝑋 ) = 1 ∧ ( 𝑎 · 0 ) = 0 ) → ( ( 𝑎 · 𝑋 ) = ( 𝑎 · 0 ) ↔ 1 = 0 ) )
12 11 biimpd ⊢ ( ( ( 𝑎 · 𝑋 ) = 1 ∧ ( 𝑎 · 0 ) = 0 ) → ( ( 𝑎 · 𝑋 ) = ( 𝑎 · 0 ) → 1 = 0 ) )
13 12 ex ⊢ ( ( 𝑎 · 𝑋 ) = 1 → ( ( 𝑎 · 0 ) = 0 → ( ( 𝑎 · 𝑋 ) = ( 𝑎 · 0 ) → 1 = 0 ) ) )
14 10 13 mpan9 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) → ( ( 𝑎 · 𝑋 ) = ( 𝑎 · 0 ) → 1 = 0 ) )
15 8 14 syl5 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) → ( 𝑋 = 0 → 1 = 0 ) )
16 oveq2 ⊢ ( 1 = 0 → ( 𝑋 · 1 ) = ( 𝑋 · 0 ) )
17 1 2 3 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · 1 ) = 𝑋 )
18 1 2 4 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · 0 ) = 0 )
19 17 18 eqeq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 · 1 ) = ( 𝑋 · 0 ) ↔ 𝑋 = 0 ) )
20 19 biimpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 · 1 ) = ( 𝑋 · 0 ) → 𝑋 = 0 ) )
21 5 6 20 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 · 1 ) = ( 𝑋 · 0 ) → 𝑋 = 0 ) )
22 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) → ( ( 𝑋 · 1 ) = ( 𝑋 · 0 ) → 𝑋 = 0 ) )
23 16 22 syl5 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) → ( 1 = 0 → 𝑋 = 0 ) )
24 15 23 impbid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑎 · 𝑋 ) = 1 ) → ( 𝑋 = 0 ↔ 1 = 0 ) )
25 24 7 r19.29a ⊢ ( 𝜑 → ( 𝑋 = 0 ↔ 1 = 0 ) )
26 25 necon3bid ⊢ ( 𝜑 → ( 𝑋 ≠ 0 ↔ 1 ≠ 0 ) )