Theorem isunit3

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$$
	isunit3.x	$$⊢\phi \to X\in B$$
	isunit3.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	isunit3	$$⊢\phi \to \left(X\in U\leftrightarrow \exists y\in B\left(X\underset{\dot{}}{·}y=\underset{\dot{}}{1}\wedge y\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		isunit3.x	$$⊢\phi \to X\in B$$
6		isunit3.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7	1 2 3 4	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)$$
8	5	biantrurd	$$⊢\phi \to \left(\left(\exists u\in BX\underset{\dot{}}{·}u=\underset{\dot{}}{1}\wedge \exists v\in Bv\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\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)\right)$$
9	7 8	bitr4id	$$⊢\phi \to \left(X\in U\leftrightarrow \left(\exists u\in BX\underset{\dot{}}{·}u=\underset{\dot{}}{1}\wedge \exists v\in Bv\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\right)$$
10		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
11	10 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
12	10 4	ringidval	$$⊢\underset{\dot{}}{1}=0_{{\mathrm{mulGrp}}_R}$$
13	10 3	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
14	10	ringmgp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
15	6 14	syl	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
16	11 12 13 15 5	mndlrinvb	$$⊢\phi \to \left(\left(\exists u\in BX\underset{\dot{}}{·}u=\underset{\dot{}}{1}\wedge \exists v\in Bv\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\leftrightarrow \exists y\in B\left(X\underset{\dot{}}{·}y=\underset{\dot{}}{1}\wedge y\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\right)$$
17	9 16	bitrd	$$⊢\phi \to \left(X\in U\leftrightarrow \exists y\in B\left(X\underset{\dot{}}{·}y=\underset{\dot{}}{1}\wedge y\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)\right)$$