Metamath Proof Explorer

Theorem idressidex0

Description: The restriction of a structure with an identity element to a subset containing the identity element has an identity element. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013) (Revised by AV, 11-Aug-2026)

Ref Expression
Hypotheses idressidex.b 
|- B = ( Base ` G )
idressidex.p 
|- .+ = ( +g ` G )
idressidex.o 
|- .0. = ( 0g ` G )
idressidex.e 
|- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
idressidex.s 
|- S = ( G |`s A )
idressidex.a 
|- ( ph -> A C_ B )
idressidex.0 
|- ( ph -> .0. e. A )
idressidex0.c 
|- C = ( Base ` S )
Assertion idressidex0 
|- ( ph -> E. e e. C A. x e. C ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )

Proof

Step Hyp Ref Expression
1 idressidex.b 
 |-  B = ( Base ` G )
2 idressidex.p 
 |-  .+ = ( +g ` G )
3 idressidex.o 
 |-  .0. = ( 0g ` G )
4 idressidex.e 
 |-  ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
5 idressidex.s 
 |-  S = ( G |`s A )
6 idressidex.a 
 |-  ( ph -> A C_ B )
7 idressidex.0 
 |-  ( ph -> .0. e. A )
8 idressidex0.c 
 |-  C = ( Base ` S )
9 1 3 2 4 0gisid 
 |-  ( ph -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
10 5 1 ressbas2 
 |-  ( A C_ B -> A = ( Base ` S ) )
11 6 10 syl 
 |-  ( ph -> A = ( Base ` S ) )
12 8 11 eqtr4id 
 |-  ( ph -> C = A )
13 7 12 eleqtrrd 
 |-  ( ph -> .0. e. C )
14 5 1 ressbasss 
 |-  ( Base ` S ) C_ B
15 8 14 eqsstri 
 |-  C C_ B
16 ssralv 
 |-  ( C C_ B -> ( A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) -> A. x e. C ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
17 15 16 mp1i 
 |-  ( ph -> ( A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) -> A. x e. C ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
18 17 adantld 
 |-  ( ph -> ( ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) -> A. x e. C ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
19 18 adantr 
 |-  ( ( ph /\ e = .0. ) -> ( ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) -> A. x e. C ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
20 oveq1 
 |-  ( e = .0. -> ( e .+ x ) = ( .0. .+ x ) )
21 20 eqeq1d 
 |-  ( e = .0. -> ( ( e .+ x ) = x <-> ( .0. .+ x ) = x ) )
22 21 ovanraleqv 
 |-  ( e = .0. -> ( A. x e. C ( ( e .+ x ) = x /\ ( x .+ e ) = x ) <-> A. x e. C ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
23 22 adantl 
 |-  ( ( ph /\ e = .0. ) -> ( A. x e. C ( ( e .+ x ) = x /\ ( x .+ e ) = x ) <-> A. x e. C ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
24 19 23 sylibrd 
 |-  ( ( ph /\ e = .0. ) -> ( ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) -> A. x e. C ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
25 13 24 rspcimedv 
 |-  ( ph -> ( ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) -> E. e e. C A. x e. C ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
26 9 25 mpd 
 |-  ( ph -> E. e e. C A. x e. C ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )