Metamath Proof Explorer

Theorem cmpidelt

Description: A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cmpidelt.1 
|- X = ran G
cmpidelt.2 
|- U = ( GId ` G )
Assertion cmpidelt 
|- ( ( G e. ( Magma i^i ExId ) /\ A e. X ) -> ( ( U G A ) = A /\ ( A G U ) = A ) )

Proof

Step Hyp Ref Expression
1 cmpidelt.1 
 |-  X = ran G
2 cmpidelt.2 
 |-  U = ( GId ` G )
3 1 2 idrval 
 |-  ( G e. ( Magma i^i ExId ) -> U = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
4 3 eqcomd 
 |-  ( G e. ( Magma i^i ExId ) -> ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) = U )
5 1 2 iorlid 
 |-  ( G e. ( Magma i^i ExId ) -> U e. X )
6 1 exidu1 
 |-  ( G e. ( Magma i^i ExId ) -> E! u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )
7 oveq1 
 |-  ( u = U -> ( u G x ) = ( U G x ) )
8 7 eqeq1d 
 |-  ( u = U -> ( ( u G x ) = x <-> ( U G x ) = x ) )
9 8 ovanraleqv 
 |-  ( u = U -> ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) <-> A. x e. X ( ( U G x ) = x /\ ( x G U ) = x ) ) )
10 9 riota2 
 |-  ( ( U e. X /\ E! u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) -> ( A. x e. X ( ( U G x ) = x /\ ( x G U ) = x ) <-> ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) = U ) )
11 5 6 10 syl2anc 
 |-  ( G e. ( Magma i^i ExId ) -> ( A. x e. X ( ( U G x ) = x /\ ( x G U ) = x ) <-> ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) = U ) )
12 4 11 mpbird 
 |-  ( G e. ( Magma i^i ExId ) -> A. x e. X ( ( U G x ) = x /\ ( x G U ) = x ) )
13 oveq2 
 |-  ( x = A -> ( U G x ) = ( U G A ) )
14 id 
 |-  ( x = A -> x = A )
15 13 14 eqeq12d 
 |-  ( x = A -> ( ( U G x ) = x <-> ( U G A ) = A ) )
16 oveq1 
 |-  ( x = A -> ( x G U ) = ( A G U ) )
17 16 14 eqeq12d 
 |-  ( x = A -> ( ( x G U ) = x <-> ( A G U ) = A ) )
18 15 17 anbi12d 
 |-  ( x = A -> ( ( ( U G x ) = x /\ ( x G U ) = x ) <-> ( ( U G A ) = A /\ ( A G U ) = A ) ) )
19 18 rspccva 
 |-  ( ( A. x e. X ( ( U G x ) = x /\ ( x G U ) = x ) /\ A e. X ) -> ( ( U G A ) = A /\ ( A G U ) = A ) )
20 12 19 sylan 
 |-  ( ( G e. ( Magma i^i ExId ) /\ A e. X ) -> ( ( U G A ) = A /\ ( A G U ) = A ) )