This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. ) ) )