Theorem isunit

Description: Property of being a unit of a ring. A unit is an element that left- and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 8-Dec-2015)

	Ref	Expression
Hypotheses	unit.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
	unit.2	$$⊢\underset{\dot{}}{1}=1_R$$
	unit.3	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	unit.4	$$⊢S={opp}_r\left(R\right)$$
	unit.5	$$⊢E={\parallel }_r\left(S\right)$$
Assertion	isunit	$$⊢X\in U\leftrightarrow \left(X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\wedge XE\underset{\dot{}}{1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		unit.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
2		unit.2	$$⊢\underset{\dot{}}{1}=1_R$$
3		unit.3	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
4		unit.4	$$⊢S={opp}_r\left(R\right)$$
5		unit.5	$$⊢E={\parallel }_r\left(S\right)$$
6		elfvdm	$$⊢X\in \mathrm{Unit}\left(R\right)\to R\in \mathrm{dom}\mathrm{Unit}$$
7	6 1	eleq2s	$$⊢X\in U\to R\in \mathrm{dom}\mathrm{Unit}$$
8	7	elexd	$$⊢X\in U\to R\in \mathrm{V}$$
9		df-br	$$⊢X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\leftrightarrow ⟨X,\underset{\dot{}}{1}⟩\in \underset{\dot{}}{\parallel }$$
10		elfvdm	$$⊢⟨X,\underset{\dot{}}{1}⟩\in {\parallel }_r\left(R\right)\to R\in \mathrm{dom}{\parallel }_r$$
11	10 3	eleq2s	$$⊢⟨X,\underset{\dot{}}{1}⟩\in \underset{\dot{}}{\parallel }\to R\in \mathrm{dom}{\parallel }_r$$
12	11	elexd	$$⊢⟨X,\underset{\dot{}}{1}⟩\in \underset{\dot{}}{\parallel }\to R\in \mathrm{V}$$
13	9 12	sylbi	$$⊢X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\to R\in \mathrm{V}$$
14	13	adantr	$$⊢\left(X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\wedge XE\underset{\dot{}}{1}\right)\to R\in \mathrm{V}$$
15		fveq2	$$⊢r=R\to {\parallel }_r\left(r\right)={\parallel }_r\left(R\right)$$
16	15 3	syl6eqr	$$⊢r=R\to {\parallel }_r\left(r\right)=\underset{\dot{}}{\parallel }$$
17		fveq2	$$⊢r=R\to {opp}_r\left(r\right)={opp}_r\left(R\right)$$
18	17 4	syl6eqr	$$⊢r=R\to {opp}_r\left(r\right)=S$$
19	18	fveq2d	$$⊢r=R\to {\parallel }_r\left({opp}_r\left(r\right)\right)={\parallel }_r\left(S\right)$$
20	19 5	syl6eqr	$$⊢r=R\to {\parallel }_r\left({opp}_r\left(r\right)\right)=E$$
21	16 20	ineq12d	$$⊢r=R\to {\parallel }_r\left(r\right)\cap {\parallel }_r\left({opp}_r\left(r\right)\right)=\underset{\dot{}}{\parallel }\cap E$$
22	21	cnveqd	$$⊢r=R\to {\left({\parallel }_r\left(r\right)\cap {\parallel }_r\left({opp}_r\left(r\right)\right)\right)}^{-1}={\left(\underset{\dot{}}{\parallel }\cap E\right)}^{-1}$$
23		fveq2	$$⊢r=R\to 1_r=1_R$$
24	23 2	syl6eqr	$$⊢r=R\to 1_r=\underset{\dot{}}{1}$$
25	24	sneqd	$$⊢r=R\to \left\{1_r\right\}=\left\{\underset{\dot{}}{1}\right\}$$
26	22 25	imaeq12d	$$⊢r=R\to {\left({\parallel }_r\left(r\right)\cap {\parallel }_r\left({opp}_r\left(r\right)\right)\right)}^{-1}\left[\left\{1_r\right\}\right]={\left(\underset{\dot{}}{\parallel }\cap E\right)}^{-1}\left[\left\{\underset{\dot{}}{1}\right\}\right]$$
27		df-unit	$$⊢\mathrm{Unit}=\left(r\in \mathrm{V}⟼{\left({\parallel }_r\left(r\right)\cap {\parallel }_r\left({opp}_r\left(r\right)\right)\right)}^{-1}\left[\left\{1_r\right\}\right]\right)$$
28	3	fvexi	$$⊢\underset{\dot{}}{\parallel }\in \mathrm{V}$$
29	28	inex1	$$⊢\underset{\dot{}}{\parallel }\cap E\in \mathrm{V}$$
30	29	cnvex	$$⊢{\left(\underset{\dot{}}{\parallel }\cap E\right)}^{-1}\in \mathrm{V}$$
31	30	imaex	$$⊢{\left(\underset{\dot{}}{\parallel }\cap E\right)}^{-1}\left[\left\{\underset{\dot{}}{1}\right\}\right]\in \mathrm{V}$$
32	26 27 31	fvmpt	$$⊢R\in \mathrm{V}\to \mathrm{Unit}\left(R\right)={\left(\underset{\dot{}}{\parallel }\cap E\right)}^{-1}\left[\left\{\underset{\dot{}}{1}\right\}\right]$$
33	1 32	syl5eq	$$⊢R\in \mathrm{V}\to U={\left(\underset{\dot{}}{\parallel }\cap E\right)}^{-1}\left[\left\{\underset{\dot{}}{1}\right\}\right]$$
34	33	eleq2d	$$⊢R\in \mathrm{V}\to \left(X\in U\leftrightarrow X\in {\left(\underset{\dot{}}{\parallel }\cap E\right)}^{-1}\left[\left\{\underset{\dot{}}{1}\right\}\right]\right)$$
35		inss1	$$⊢\underset{\dot{}}{\parallel }\cap E\subseteq \underset{\dot{}}{\parallel }$$
36	3	reldvdsr	$$⊢\mathrm{Rel}\underset{\dot{}}{\parallel }$$
37		relss	$$⊢\underset{\dot{}}{\parallel }\cap E\subseteq \underset{\dot{}}{\parallel }\to \left(\mathrm{Rel}\underset{\dot{}}{\parallel }\to \mathrm{Rel}\left(\underset{\dot{}}{\parallel }\cap E\right)\right)$$
38	35 36 37	mp2	$$⊢\mathrm{Rel}\left(\underset{\dot{}}{\parallel }\cap E\right)$$
39		eliniseg2	$$⊢\mathrm{Rel}\left(\underset{\dot{}}{\parallel }\cap E\right)\to \left(X\in {\left(\underset{\dot{}}{\parallel }\cap E\right)}^{-1}\left[\left\{\underset{\dot{}}{1}\right\}\right]\leftrightarrow X\left(\underset{\dot{}}{\parallel }\cap E\right)\underset{\dot{}}{1}\right)$$
40	38 39	ax-mp	$$⊢X\in {\left(\underset{\dot{}}{\parallel }\cap E\right)}^{-1}\left[\left\{\underset{\dot{}}{1}\right\}\right]\leftrightarrow X\left(\underset{\dot{}}{\parallel }\cap E\right)\underset{\dot{}}{1}$$
41		brin	$$⊢X\left(\underset{\dot{}}{\parallel }\cap E\right)\underset{\dot{}}{1}\leftrightarrow \left(X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\wedge XE\underset{\dot{}}{1}\right)$$
42	40 41	bitri	$$⊢X\in {\left(\underset{\dot{}}{\parallel }\cap E\right)}^{-1}\left[\left\{\underset{\dot{}}{1}\right\}\right]\leftrightarrow \left(X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\wedge XE\underset{\dot{}}{1}\right)$$
43	34 42	syl6bb	$$⊢R\in \mathrm{V}\to \left(X\in U\leftrightarrow \left(X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\wedge XE\underset{\dot{}}{1}\right)\right)$$
44	8 14 43	pm5.21nii	$$⊢X\in U\leftrightarrow \left(X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\wedge XE\underset{\dot{}}{1}\right)$$