Metamath Proof Explorer

Theorem exidresid

Description: The restriction of a binary operation with identity to a subset containing the identity has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013)

Ref Expression
Hypotheses exidres.1 
|- X = ran G
exidres.2 
|- U = ( GId ` G )
exidres.3 
|- H = ( G |` ( Y X. Y ) )
Assertion exidresid 
|- ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> ( GId ` H ) = U )

Proof

Step Hyp Ref Expression
1 exidres.1 
 |-  X = ran G
2 exidres.2 
 |-  U = ( GId ` G )
3 exidres.3 
 |-  H = ( G |` ( Y X. Y ) )
4 resexg 
 |-  ( G e. ( Magma i^i ExId ) -> ( G |` ( Y X. Y ) ) e. _V )
5 3 4 eqeltrid 
 |-  ( G e. ( Magma i^i ExId ) -> H e. _V )
6 eqid 
 |-  ran H = ran H
7 6 gidval 
 |-  ( H e. _V -> ( GId ` H ) = ( iota_ u e. ran H A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) ) )
8 5 7 syl 
 |-  ( G e. ( Magma i^i ExId ) -> ( GId ` H ) = ( iota_ u e. ran H A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) ) )
9 8 3ad2ant1 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> ( GId ` H ) = ( iota_ u e. ran H A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) ) )
10 9 adantr 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> ( GId ` H ) = ( iota_ u e. ran H A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) ) )
11 1 2 3 exidreslem 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> ( U e. dom dom H /\ A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) ) )
12 11 simprd 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) )
13 12 adantr 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) )
14 1 2 3 exidres 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> H e. ExId )
15 elin 
 |-  ( H e. ( Magma i^i ExId ) <-> ( H e. Magma /\ H e. ExId ) )
16 rngopidOLD 
 |-  ( H e. ( Magma i^i ExId ) -> ran H = dom dom H )
17 15 16 sylbir 
 |-  ( ( H e. Magma /\ H e. ExId ) -> ran H = dom dom H )
18 17 ancoms 
 |-  ( ( H e. ExId /\ H e. Magma ) -> ran H = dom dom H )
19 14 18 sylan 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> ran H = dom dom H )
20 19 raleqdv 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> ( A. x e. ran H ( ( U H x ) = x /\ ( x H U ) = x ) <-> A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) ) )
21 13 20 mpbird 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> A. x e. ran H ( ( U H x ) = x /\ ( x H U ) = x ) )
22 11 simpld 
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> U e. dom dom H )
23 22 adantr 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> U e. dom dom H )
24 23 19 eleqtrrd 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> U e. ran H )
25 6 exidu1 
 |-  ( H e. ( Magma i^i ExId ) -> E! u e. ran H A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) )
26 15 25 sylbir 
 |-  ( ( H e. Magma /\ H e. ExId ) -> E! u e. ran H A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) )
27 26 ancoms 
 |-  ( ( H e. ExId /\ H e. Magma ) -> E! u e. ran H A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) )
28 14 27 sylan 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> E! u e. ran H A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) )
29 oveq1 
 |-  ( u = U -> ( u H x ) = ( U H x ) )
30 29 eqeq1d 
 |-  ( u = U -> ( ( u H x ) = x <-> ( U H x ) = x ) )
31 30 ovanraleqv 
 |-  ( u = U -> ( A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) <-> A. x e. ran H ( ( U H x ) = x /\ ( x H U ) = x ) ) )
32 31 riota2 
 |-  ( ( U e. ran H /\ E! u e. ran H A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) ) -> ( A. x e. ran H ( ( U H x ) = x /\ ( x H U ) = x ) <-> ( iota_ u e. ran H A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) ) = U ) )
33 24 28 32 syl2anc 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> ( A. x e. ran H ( ( U H x ) = x /\ ( x H U ) = x ) <-> ( iota_ u e. ran H A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) ) = U ) )
34 21 33 mpbid 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> ( iota_ u e. ran H A. x e. ran H ( ( u H x ) = x /\ ( x H u ) = x ) ) = U )
35 10 34 eqtrd 
 |-  ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> ( GId ` H ) = U )