Theorem ringinvnz1ne0

Description: In a unital 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	$$⊢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}$$
Assertion	ringinvnz1ne0	$$⊢\phi \to \left(X\ne \underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{1}\ne \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		oveq2	$$⊢X=\underset{\dot{}}{0}\to a\underset{\dot{}}{·}X=a\underset{\dot{}}{·}\underset{\dot{}}{0}$$
9	1 2 4	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge a\in B\right)\to a\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
10	5 9	sylan	$$⊢\left(\phi \wedge a\in B\right)\to a\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
11		eqeq12	$$⊢\left(a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\wedge a\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)\to \left(a\underset{\dot{}}{·}X=a\underset{\dot{}}{·}\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
12	11	biimpd	$$⊢\left(a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\wedge a\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)\to \left(a\underset{\dot{}}{·}X=a\underset{\dot{}}{·}\underset{\dot{}}{0}\to \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
13	12	ex	$$⊢a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\to \left(a\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\to \left(a\underset{\dot{}}{·}X=a\underset{\dot{}}{·}\underset{\dot{}}{0}\to \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)\right)$$
14	10 13	mpan9	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\to \left(a\underset{\dot{}}{·}X=a\underset{\dot{}}{·}\underset{\dot{}}{0}\to \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
15	8 14	syl5	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\to \left(X=\underset{\dot{}}{0}\to \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
16		oveq2	$$⊢\underset{\dot{}}{1}=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}\underset{\dot{}}{1}=X\underset{\dot{}}{·}\underset{\dot{}}{0}$$
17	1 2 3	ringridm	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{1}=X$$
18	1 2 4	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
19	17 18	eqeq12d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(X\underset{\dot{}}{·}\underset{\dot{}}{1}=X\underset{\dot{}}{·}\underset{\dot{}}{0}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
20	19	biimpd	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(X\underset{\dot{}}{·}\underset{\dot{}}{1}=X\underset{\dot{}}{·}\underset{\dot{}}{0}\to X=\underset{\dot{}}{0}\right)$$
21	5 6 20	syl2anc	$$⊢\phi \to \left(X\underset{\dot{}}{·}\underset{\dot{}}{1}=X\underset{\dot{}}{·}\underset{\dot{}}{0}\to X=\underset{\dot{}}{0}\right)$$
22	21	ad2antrr	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\to \left(X\underset{\dot{}}{·}\underset{\dot{}}{1}=X\underset{\dot{}}{·}\underset{\dot{}}{0}\to X=\underset{\dot{}}{0}\right)$$
23	16 22	syl5	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\to \left(\underset{\dot{}}{1}=\underset{\dot{}}{0}\to X=\underset{\dot{}}{0}\right)$$
24	15 23	impbid	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge a\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\to \left(X=\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
25	24 7	r19.29a	$$⊢\phi \to \left(X=\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
26	25	necon3bid	$$⊢\phi \to \left(X\ne \underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)$$