Metamath Proof Explorer

Theorem rngoidmlem

Description: The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Feb-2010) (New usage is discouraged.)

Ref Expression
Hypotheses uridm.1 
|- H = ( 2nd ` R )
uridm.2 
|- X = ran ( 1st ` R )
uridm.3 
|- U = ( GId ` H )
Assertion rngoidmlem 
|- ( ( R e. RingOps /\ A e. X ) -> ( ( U H A ) = A /\ ( A H U ) = A ) )

Proof

Step Hyp Ref Expression
1 uridm.1 
 |-  H = ( 2nd ` R )
2 uridm.2 
 |-  X = ran ( 1st ` R )
3 uridm.3 
 |-  U = ( GId ` H )
4 1 rngomndo 
 |-  ( R e. RingOps -> H e. MndOp )
5 mndomgmid 
 |-  ( H e. MndOp -> H e. ( Magma i^i ExId ) )
6 eqid 
 |-  ran H = ran H
7 6 3 cmpidelt 
 |-  ( ( H e. ( Magma i^i ExId ) /\ A e. ran H ) -> ( ( U H A ) = A /\ ( A H U ) = A ) )
8 7 ex 
 |-  ( H e. ( Magma i^i ExId ) -> ( A e. ran H -> ( ( U H A ) = A /\ ( A H U ) = A ) ) )
9 4 5 8 3syl 
 |-  ( R e. RingOps -> ( A e. ran H -> ( ( U H A ) = A /\ ( A H U ) = A ) ) )
10 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
11 1 10 rngorn1eq 
 |-  ( R e. RingOps -> ran ( 1st ` R ) = ran H )
12 eqtr 
 |-  ( ( X = ran ( 1st ` R ) /\ ran ( 1st ` R ) = ran H ) -> X = ran H )
13 simpl 
 |-  ( ( X = ran H /\ R e. RingOps ) -> X = ran H )
14 13 eleq2d 
 |-  ( ( X = ran H /\ R e. RingOps ) -> ( A e. X <-> A e. ran H ) )
15 14 imbi1d 
 |-  ( ( X = ran H /\ R e. RingOps ) -> ( ( A e. X -> ( ( U H A ) = A /\ ( A H U ) = A ) ) <-> ( A e. ran H -> ( ( U H A ) = A /\ ( A H U ) = A ) ) ) )
16 15 ex 
 |-  ( X = ran H -> ( R e. RingOps -> ( ( A e. X -> ( ( U H A ) = A /\ ( A H U ) = A ) ) <-> ( A e. ran H -> ( ( U H A ) = A /\ ( A H U ) = A ) ) ) ) )
17 12 16 syl 
 |-  ( ( X = ran ( 1st ` R ) /\ ran ( 1st ` R ) = ran H ) -> ( R e. RingOps -> ( ( A e. X -> ( ( U H A ) = A /\ ( A H U ) = A ) ) <-> ( A e. ran H -> ( ( U H A ) = A /\ ( A H U ) = A ) ) ) ) )
18 2 17 mpan 
 |-  ( ran ( 1st ` R ) = ran H -> ( R e. RingOps -> ( ( A e. X -> ( ( U H A ) = A /\ ( A H U ) = A ) ) <-> ( A e. ran H -> ( ( U H A ) = A /\ ( A H U ) = A ) ) ) ) )
19 11 18 mpcom 
 |-  ( R e. RingOps -> ( ( A e. X -> ( ( U H A ) = A /\ ( A H U ) = A ) ) <-> ( A e. ran H -> ( ( U H A ) = A /\ ( A H U ) = A ) ) ) )
20 9 19 mpbird 
 |-  ( R e. RingOps -> ( A e. X -> ( ( U H A ) = A /\ ( A H U ) = A ) ) )
21 20 imp 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( U H A ) = A /\ ( A H U ) = A ) )