Theorem isunit2

Description: Alternate definition of being a unit. (Contributed by Thierry Arnoux, 3-Aug-2025)

	Ref	Expression
Hypotheses	isunit2.b	$$⊢B={\mathrm{Base}}_R$$
	isunit2.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
	isunit2.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	isunit2.1	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	isunit2	$$⊢X\in U\leftrightarrow \left(X\in B\wedge \left(\exists u\in BX\underset{\dot{}}{·}u=\underset{\dot{}}{1}\wedge \exists v\in Bv\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isunit2.b	$$⊢B={\mathrm{Base}}_R$$
2		isunit2.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
3		isunit2.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		isunit2.1	$$⊢\underset{\dot{}}{1}=1_R$$
5		eqid	$$⊢{\parallel }_r\left(R\right)={\parallel }_r\left(R\right)$$
6	1 5 3	dvdsr	$$⊢X{\parallel }_r\left(R\right)\underset{\dot{}}{1}\leftrightarrow \left(X\in B\wedge \exists v\in Bv\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)$$
7		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
8	7 1	opprbas	$$⊢B={\mathrm{Base}}_{{opp}_r\left(R\right)}$$
9		eqid	$$⊢{\parallel }_r\left({opp}_r\left(R\right)\right)={\parallel }_r\left({opp}_r\left(R\right)\right)$$
10		eqid	$$⊢{\cdot }_{{opp}_r\left(R\right)}={\cdot }_{{opp}_r\left(R\right)}$$
11	8 9 10	dvdsr	$$⊢X{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}\leftrightarrow \left(X\in B\wedge \exists u\in Bu{\cdot }_{{opp}_r\left(R\right)}X=\underset{\dot{}}{1}\right)$$
12	1 3 7 10	opprmul	$$⊢u{\cdot }_{{opp}_r\left(R\right)}X=X\underset{\dot{}}{·}u$$
13	12	eqeq1i	$$⊢u{\cdot }_{{opp}_r\left(R\right)}X=\underset{\dot{}}{1}\leftrightarrow X\underset{\dot{}}{·}u=\underset{\dot{}}{1}$$
14	13	rexbii	$$⊢\exists u\in Bu{\cdot }_{{opp}_r\left(R\right)}X=\underset{\dot{}}{1}\leftrightarrow \exists u\in BX\underset{\dot{}}{·}u=\underset{\dot{}}{1}$$
15	14	anbi2i	$$⊢\left(X\in B\wedge \exists u\in Bu{\cdot }_{{opp}_r\left(R\right)}X=\underset{\dot{}}{1}\right)\leftrightarrow \left(X\in B\wedge \exists u\in BX\underset{\dot{}}{·}u=\underset{\dot{}}{1}\right)$$
16	11 15	bitri	$$⊢X{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}\leftrightarrow \left(X\in B\wedge \exists u\in BX\underset{\dot{}}{·}u=\underset{\dot{}}{1}\right)$$
17	6 16	anbi12ci	$$⊢\left(X{\parallel }_r\left(R\right)\underset{\dot{}}{1}\wedge X{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}\right)\leftrightarrow \left(\left(X\in B\wedge \exists u\in BX\underset{\dot{}}{·}u=\underset{\dot{}}{1}\right)\wedge \left(X\in B\wedge \exists v\in Bv\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\right)$$
18	2 4 5 7 9	isunit	$$⊢X\in U\leftrightarrow \left(X{\parallel }_r\left(R\right)\underset{\dot{}}{1}\wedge X{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}\right)$$
19		anandi	$$⊢\left(X\in B\wedge \left(\exists u\in BX\underset{\dot{}}{·}u=\underset{\dot{}}{1}\wedge \exists v\in Bv\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\right)\leftrightarrow \left(\left(X\in B\wedge \exists u\in BX\underset{\dot{}}{·}u=\underset{\dot{}}{1}\right)\wedge \left(X\in B\wedge \exists v\in Bv\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\right)$$
20	17 18 19	3bitr4i	$$⊢X\in U\leftrightarrow \left(X\in B\wedge \left(\exists u\in BX\underset{\dot{}}{·}u=\underset{\dot{}}{1}\wedge \exists v\in Bv\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\right)$$