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	$$⊢B={\mathrm{Base}}_R$$
	ringinvnzdiv.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	ringinvnzdiv.u	$$⊢\underset{\dot{}}{1}=1_R$$
	ringinvnzdiv.z	$$⊢\underset{\dot{}}{0}=0_R$$
	ringinvnzdiv.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	ringinvnzdiv.x	$$⊢\phi \to X\in B$$
	ringinvnzdiv.a	$$⊢\phi \to \exists a\in Ba\underset{\dot{}}{·}X=\underset{\dot{}}{1}$$
	ringinvnzdiv.y	$$⊢\phi \to Y\in B$$
Assertion	ringinvnzdiv	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ringinvnzdiv.b	$$⊢B={\mathrm{Base}}_R$$
2		ringinvnzdiv.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		ringinvnzdiv.u	$$⊢\underset{\dot{}}{1}=1_R$$
4		ringinvnzdiv.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		ringinvnzdiv.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		ringinvnzdiv.x	$$⊢\phi \to X\in B$$
7		ringinvnzdiv.a	$$⊢\phi \to \exists a\in Ba\underset{\dot{}}{·}X=\underset{\dot{}}{1}$$
8		ringinvnzdiv.y	$$⊢\phi \to Y\in B$$
9	1 2 3	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}Y=Y$$
10	5 8 9	syl2anc	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}Y=Y$$
11	10	eqcomd	$$⊢\phi \to Y=\underset{\dot{}}{1}\underset{\dot{}}{·}Y$$
12	11	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\to Y=\underset{\dot{}}{1}\underset{\dot{}}{·}Y$$
13		oveq1	$$⊢\underset{\dot{}}{1}=a\underset{\dot{}}{·}X\to \underset{\dot{}}{1}\underset{\dot{}}{·}Y=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y$$
14	13	eqcoms	$$⊢a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\to \underset{\dot{}}{1}\underset{\dot{}}{·}Y=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y$$
15	14	adantl	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}Y=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y$$
16	5	adantr	$$⊢\left(\phi \wedge a\in B\right)\to R\in \mathrm{Ring}$$
17		simpr	$$⊢\left(\phi \wedge a\in B\right)\to a\in B$$
18	6	adantr	$$⊢\left(\phi \wedge a\in B\right)\to X\in B$$
19	8	adantr	$$⊢\left(\phi \wedge a\in B\right)\to Y\in B$$
20	17 18 19	3jca	$$⊢\left(\phi \wedge a\in B\right)\to \left(a\in B\wedge X\in B\wedge Y\in B\right)$$
21	16 20	jca	$$⊢\left(\phi \wedge a\in B\right)\to \left(R\in \mathrm{Ring}\wedge \left(a\in B\wedge X\in B\wedge Y\in B\right)\right)$$
22	21	adantr	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\to \left(R\in \mathrm{Ring}\wedge \left(a\in B\wedge X\in B\wedge Y\in B\right)\right)$$
23	1 2	ringass	$$⊢\left(R\in \mathrm{Ring}\wedge \left(a\in B\wedge X\in B\wedge Y\in B\right)\right)\to \left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y=a\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)$$
24	22 23	syl	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\to \left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y=a\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)$$
25	15 24	eqtrd	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}Y=a\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)$$
26	25	adantr	$$⊢\left(\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}Y=a\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)$$
27		oveq2	$$⊢X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to a\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)=a\underset{\dot{}}{·}\underset{\dot{}}{0}$$
28	1 2 4	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge a\in B\right)\to a\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
29	5 28	sylan	$$⊢\left(\phi \wedge a\in B\right)\to a\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
30	29	adantr	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\to a\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
31	27 30	sylan9eqr	$$⊢\left(\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\to a\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)=\underset{\dot{}}{0}$$
32	12 26 31	3eqtrd	$$⊢\left(\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\to Y=\underset{\dot{}}{0}$$
33	32	exp31	$$⊢\left(\phi \wedge a\in B\right)\to \left(a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to Y=\underset{\dot{}}{0}\right)\right)$$
34	33	rexlimdva	$$⊢\phi \to \left(\exists a\in Ba\underset{\dot{}}{·}X=\underset{\dot{}}{1}\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to Y=\underset{\dot{}}{0}\right)\right)$$
35	7 34	mpd	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to Y=\underset{\dot{}}{0}\right)$$
36		oveq2	$$⊢Y=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}\underset{\dot{}}{0}$$
37	1 2 4	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
38	5 6 37	syl2anc	$$⊢\phi \to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
39	36 38	sylan9eqr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}$$
40	39	ex	$$⊢\phi \to \left(Y=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
41	35 40	impbid	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$