Metamath Proof Explorer

Theorem isunit3

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 )
isunit3.x 
|- ( ph -> X e. B )
isunit3.r 
|- ( ph -> R e. Ring )
Assertion isunit3 
|- ( ph -> ( X e. U <-> E. y e. B ( ( X .x. y ) = .1. /\ ( y .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 isunit3.x 
 |-  ( ph -> X e. B )
6 isunit3.r 
 |-  ( ph -> R e. Ring )
7 1 2 3 4 isunit2 
 |-  ( X e. U <-> ( X e. B /\ ( E. u e. B ( X .x. u ) = .1. /\ E. v e. B ( v .x. X ) = .1. ) ) )
8 5 biantrurd 
 |-  ( ph -> ( ( 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. /\ E. v e. B ( v .x. X ) = .1. ) ) ) )
9 7 8 bitr4id 
 |-  ( ph -> ( X e. U <-> ( E. u e. B ( X .x. u ) = .1. /\ E. v e. B ( v .x. X ) = .1. ) ) )
10 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
11 10 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
12 10 4 ringidval 
 |-  .1. = ( 0g ` ( mulGrp ` R ) )
13 10 3 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
14 10 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
15 6 14 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
16 11 12 13 15 5 mndlrinvb 
 |-  ( ph -> ( ( E. u e. B ( X .x. u ) = .1. /\ E. v e. B ( v .x. X ) = .1. ) <-> E. y e. B ( ( X .x. y ) = .1. /\ ( y .x. X ) = .1. ) ) )
17 9 16 bitrd 
 |-  ( ph -> ( X e. U <-> E. y e. B ( ( X .x. y ) = .1. /\ ( y .x. X ) = .1. ) ) )