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 ) )