Theorem isunit2

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

	Ref	Expression
Hypotheses	isunit2.b	|- B = ( Base ` R )
	isunit2.u	|- U = ( Unit ` R )
	isunit2.m	|- .x. = ( .r ` R )
	isunit2.1	|- .1. = ( 1r ` R )
Assertion	isunit2	|- ( X e. U <-> ( X e. B /\ ( E. u e. B ( X .x. u ) = .1. /\ E. v e. B ( v .x. X ) = .1. ) ) )

Proof

Step	Hyp	Ref	Expression
1		isunit2.b	|- B = ( Base ` R )
2		isunit2.u	|- U = ( Unit ` R )
3		isunit2.m	|- .x. = ( .r ` R )
4		isunit2.1	|- .1. = ( 1r ` R )
5		eqid	|- ( ||r ` R ) = ( ||r ` R )
6	1 5 3	dvdsr	|- ( X ( ||r ` R ) .1. <-> ( X e. B /\ E. v e. B ( v .x. X ) = .1. ) )
7		eqid	|- ( oppR ` R ) = ( oppR ` R )
8	7 1	opprbas	|- B = ( Base ` ( oppR ` R ) )
9		eqid	|- ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
10		eqid	|- ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
11	8 9 10	dvdsr	|- ( X ( ||r ` ( oppR ` R ) ) .1. <-> ( X e. B /\ E. u e. B ( u ( .r ` ( oppR ` R ) ) X ) = .1. ) )
12	1 3 7 10	opprmul	|- ( u ( .r ` ( oppR ` R ) ) X ) = ( X .x. u )
13	12	eqeq1i	|- ( ( u ( .r ` ( oppR ` R ) ) X ) = .1. <-> ( X .x. u ) = .1. )
14	13	rexbii	|- ( E. u e. B ( u ( .r ` ( oppR ` R ) ) X ) = .1. <-> E. u e. B ( X .x. u ) = .1. )
15	14	anbi2i	|- ( ( X e. B /\ E. u e. B ( u ( .r ` ( oppR ` R ) ) X ) = .1. ) <-> ( X e. B /\ E. u e. B ( X .x. u ) = .1. ) )
16	11 15	bitri	|- ( X ( ||r ` ( oppR ` R ) ) .1. <-> ( X e. B /\ E. u e. B ( X .x. u ) = .1. ) )
17	6 16	anbi12ci	|- ( ( X ( ||r ` R ) .1. /\ X ( ||r ` ( oppR ` R ) ) .1. ) <-> ( ( X e. B /\ E. u e. B ( X .x. u ) = .1. ) /\ ( X e. B /\ E. v e. B ( v .x. X ) = .1. ) ) )
18	2 4 5 7 9	isunit	|- ( X e. U <-> ( X ( ||r ` R ) .1. /\ X ( ||r ` ( oppR ` R ) ) .1. ) )
19		anandi	|- ( ( X e. B /\ ( E. u e. B ( X .x. u ) = .1. /\ E. v e. B ( v .x. X ) = .1. ) ) <-> ( ( X e. B /\ E. u e. B ( X .x. u ) = .1. ) /\ ( X e. B /\ E. v e. B ( v .x. X ) = .1. ) ) )
20	17 18 19	3bitr4i	|- ( X e. U <-> ( X e. B /\ ( E. u e. B ( X .x. u ) = .1. /\ E. v e. B ( v .x. X ) = .1. ) ) )