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 = {Base}_{R}$
	ringinvnzdiv.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ringinvnzdiv.u	$⊢ \underset{˙}{1} = 1_{R}$
	ringinvnzdiv.z	$⊢ \underset{˙}{0} = 0_{R}$
	ringinvnzdiv.r	$⊢ φ \to R \in Ring$
	ringinvnzdiv.x	$⊢ φ \to X \in B$
	ringinvnzdiv.a	$⊢ φ \to \exists a \in B a \underset{˙}{\cdot} X = \underset{˙}{1}$
Assertion	ringinvnz1ne0	$⊢ φ \to (X \neq \underset{˙}{0} \leftrightarrow \underset{˙}{1} \neq \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		ringinvnzdiv.b	$⊢ B = {Base}_{R}$
2		ringinvnzdiv.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		ringinvnzdiv.u	$⊢ \underset{˙}{1} = 1_{R}$
4		ringinvnzdiv.z	$⊢ \underset{˙}{0} = 0_{R}$
5		ringinvnzdiv.r	$⊢ φ \to R \in Ring$
6		ringinvnzdiv.x	$⊢ φ \to X \in B$
7		ringinvnzdiv.a	$⊢ φ \to \exists a \in B a \underset{˙}{\cdot} X = \underset{˙}{1}$
8		oveq2	$⊢ X = \underset{˙}{0} \to a \underset{˙}{\cdot} X = a \underset{˙}{\cdot} \underset{˙}{0}$
9	1 2 4	ringrz	$⊢ (R \in Ring \land a \in B) \to a \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
10	5 9	sylan	$⊢ (φ \land a \in B) \to a \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
11		eqeq12	$⊢ (a \underset{˙}{\cdot} X = \underset{˙}{1} \land a \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}) \to (a \underset{˙}{\cdot} X = a \underset{˙}{\cdot} \underset{˙}{0} \leftrightarrow \underset{˙}{1} = \underset{˙}{0})$
12	11	biimpd	$⊢ (a \underset{˙}{\cdot} X = \underset{˙}{1} \land a \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}) \to (a \underset{˙}{\cdot} X = a \underset{˙}{\cdot} \underset{˙}{0} \to \underset{˙}{1} = \underset{˙}{0})$
13	12	ex	$⊢ a \underset{˙}{\cdot} X = \underset{˙}{1} \to (a \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0} \to (a \underset{˙}{\cdot} X = a \underset{˙}{\cdot} \underset{˙}{0} \to \underset{˙}{1} = \underset{˙}{0}))$
14	10 13	mpan9	$⊢ ((φ \land a \in B) \land a \underset{˙}{\cdot} X = \underset{˙}{1}) \to (a \underset{˙}{\cdot} X = a \underset{˙}{\cdot} \underset{˙}{0} \to \underset{˙}{1} = \underset{˙}{0})$
15	8 14	syl5	$⊢ ((φ \land a \in B) \land a \underset{˙}{\cdot} X = \underset{˙}{1}) \to (X = \underset{˙}{0} \to \underset{˙}{1} = \underset{˙}{0})$
16		oveq2	$⊢ \underset{˙}{1} = \underset{˙}{0} \to X \underset{˙}{\cdot} \underset{˙}{1} = X \underset{˙}{\cdot} \underset{˙}{0}$
17	1 2 3	ringridm	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{1} = X$
18	1 2 4	ringrz	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
19	17 18	eqeq12d	$⊢ (R \in Ring \land X \in B) \to (X \underset{˙}{\cdot} \underset{˙}{1} = X \underset{˙}{\cdot} \underset{˙}{0} \leftrightarrow X = \underset{˙}{0})$
20	19	biimpd	$⊢ (R \in Ring \land X \in B) \to (X \underset{˙}{\cdot} \underset{˙}{1} = X \underset{˙}{\cdot} \underset{˙}{0} \to X = \underset{˙}{0})$
21	5 6 20	syl2anc	$⊢ φ \to (X \underset{˙}{\cdot} \underset{˙}{1} = X \underset{˙}{\cdot} \underset{˙}{0} \to X = \underset{˙}{0})$
22	21	ad2antrr	$⊢ ((φ \land a \in B) \land a \underset{˙}{\cdot} X = \underset{˙}{1}) \to (X \underset{˙}{\cdot} \underset{˙}{1} = X \underset{˙}{\cdot} \underset{˙}{0} \to X = \underset{˙}{0})$
23	16 22	syl5	$⊢ ((φ \land a \in B) \land a \underset{˙}{\cdot} X = \underset{˙}{1}) \to (\underset{˙}{1} = \underset{˙}{0} \to X = \underset{˙}{0})$
24	15 23	impbid	$⊢ ((φ \land a \in B) \land a \underset{˙}{\cdot} X = \underset{˙}{1}) \to (X = \underset{˙}{0} \leftrightarrow \underset{˙}{1} = \underset{˙}{0})$
25	24 7	r19.29a	$⊢ φ \to (X = \underset{˙}{0} \leftrightarrow \underset{˙}{1} = \underset{˙}{0})$
26	25	necon3bid	$⊢ φ \to (X \neq \underset{˙}{0} \leftrightarrow \underset{˙}{1} \neq \underset{˙}{0})$

Metamath Proof Explorer

Theorem ringinvnz1ne0

Proof