Theorem crngunit

Description: Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Hypotheses	crngunit.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
	crngunit.2	$$⊢\underset{\dot{}}{1}=1_R$$
	crngunit.3	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
Assertion	crngunit	$$⊢R\in \mathrm{CRing}\to \left(X\in U\leftrightarrow X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		crngunit.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
2		crngunit.2	$$⊢\underset{\dot{}}{1}=1_R$$
3		crngunit.3	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
4		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5		eqid	$$⊢{\cdot }_R={\cdot }_R$$
6		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
7		eqid	$$⊢{\cdot }_{{opp}_r\left(R\right)}={\cdot }_{{opp}_r\left(R\right)}$$
8	4 5 6 7	crngoppr	$$⊢\left(R\in \mathrm{CRing}\wedge y\in {\mathrm{Base}}_R\wedge X\in {\mathrm{Base}}_R\right)\to y{\cdot }_{R}X=y{\cdot }_{{opp}_r\left(R\right)}X$$
9	8	3expa	$$⊢\left(\left(R\in \mathrm{CRing}\wedge y\in {\mathrm{Base}}_R\right)\wedge X\in {\mathrm{Base}}_R\right)\to y{\cdot }_{R}X=y{\cdot }_{{opp}_r\left(R\right)}X$$
10	9	eqcomd	$$⊢\left(\left(R\in \mathrm{CRing}\wedge y\in {\mathrm{Base}}_R\right)\wedge X\in {\mathrm{Base}}_R\right)\to y{\cdot }_{{opp}_r\left(R\right)}X=y{\cdot }_{R}X$$
11	10	an32s	$$⊢\left(\left(R\in \mathrm{CRing}\wedge X\in {\mathrm{Base}}_R\right)\wedge y\in {\mathrm{Base}}_R\right)\to y{\cdot }_{{opp}_r\left(R\right)}X=y{\cdot }_{R}X$$
12	11	eqeq1d	$$⊢\left(\left(R\in \mathrm{CRing}\wedge X\in {\mathrm{Base}}_R\right)\wedge y\in {\mathrm{Base}}_R\right)\to \left(y{\cdot }_{{opp}_r\left(R\right)}X=\underset{\dot{}}{1}\leftrightarrow y{\cdot }_{R}X=\underset{\dot{}}{1}\right)$$
13	12	rexbidva	$$⊢\left(R\in \mathrm{CRing}\wedge X\in {\mathrm{Base}}_R\right)\to \left(\exists y\in {\mathrm{Base}}_{R}y{\cdot }_{{opp}_r\left(R\right)}X=\underset{\dot{}}{1}\leftrightarrow \exists y\in {\mathrm{Base}}_{R}y{\cdot }_{R}X=\underset{\dot{}}{1}\right)$$
14	13	pm5.32da	$$⊢R\in \mathrm{CRing}\to \left(\left(X\in {\mathrm{Base}}_R\wedge \exists y\in {\mathrm{Base}}_{R}y{\cdot }_{{opp}_r\left(R\right)}X=\underset{\dot{}}{1}\right)\leftrightarrow \left(X\in {\mathrm{Base}}_R\wedge \exists y\in {\mathrm{Base}}_{R}y{\cdot }_{R}X=\underset{\dot{}}{1}\right)\right)$$
15	6 4	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{opp}_r\left(R\right)}$$
16		eqid	$$⊢{\parallel }_r\left({opp}_r\left(R\right)\right)={\parallel }_r\left({opp}_r\left(R\right)\right)$$
17	15 16 7	dvdsr	$$⊢X{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}\leftrightarrow \left(X\in {\mathrm{Base}}_R\wedge \exists y\in {\mathrm{Base}}_{R}y{\cdot }_{{opp}_r\left(R\right)}X=\underset{\dot{}}{1}\right)$$
18	4 3 5	dvdsr	$$⊢X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\leftrightarrow \left(X\in {\mathrm{Base}}_R\wedge \exists y\in {\mathrm{Base}}_{R}y{\cdot }_{R}X=\underset{\dot{}}{1}\right)$$
19	14 17 18	3bitr4g	$$⊢R\in \mathrm{CRing}\to \left(X{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}\leftrightarrow X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\right)$$
20	19	anbi2d	$$⊢R\in \mathrm{CRing}\to \left(\left(X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\wedge X{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}\right)\leftrightarrow \left(X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\wedge X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\right)\right)$$
21	1 2 3 6 16	isunit	$$⊢X\in U\leftrightarrow \left(X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\wedge X{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}\right)$$
22		pm4.24	$$⊢X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\leftrightarrow \left(X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\wedge X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\right)$$
23	20 21 22	3bitr4g	$$⊢R\in \mathrm{CRing}\to \left(X\in U\leftrightarrow X\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\right)$$