Metamath Proof Explorer

Theorem idressid

Description: The restriction of a structure with an identity element to a subset containing the identity element has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013) (Revised by AV, 12-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 )
Assertion idressid 
|- ( ph -> ( 0g ` S ) = .0. )

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 5 1 ressbas2 
 |-  ( A C_ B -> A = ( Base ` S ) )
9 6 8 syl 
 |-  ( ph -> A = ( Base ` S ) )
10 7 9 eleqtrd 
 |-  ( ph -> .0. e. ( Base ` S ) )
11 1 3 2 4 0gisid 
 |-  ( ph -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
12 ssralv 
 |-  ( A C_ B -> ( A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) -> A. x e. A ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
13 6 12 syl 
 |-  ( ph -> ( A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) -> A. x e. A ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
14 1 fvexi 
 |-  B e. _V
15 14 a1i 
 |-  ( ph -> B e. _V )
16 15 6 ssexd 
 |-  ( ph -> A e. _V )
17 5 2 ressplusg 
 |-  ( A e. _V -> .+ = ( +g ` S ) )
18 16 17 syl 
 |-  ( ph -> .+ = ( +g ` S ) )
19 18 oveqd 
 |-  ( ph -> ( .0. .+ x ) = ( .0. ( +g ` S ) x ) )
20 19 eqeq1d 
 |-  ( ph -> ( ( .0. .+ x ) = x <-> ( .0. ( +g ` S ) x ) = x ) )
21 18 oveqd 
 |-  ( ph -> ( x .+ .0. ) = ( x ( +g ` S ) .0. ) )
22 21 eqeq1d 
 |-  ( ph -> ( ( x .+ .0. ) = x <-> ( x ( +g ` S ) .0. ) = x ) )
23 20 22 anbi12d 
 |-  ( ph -> ( ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) <-> ( ( .0. ( +g ` S ) x ) = x /\ ( x ( +g ` S ) .0. ) = x ) ) )
24 9 23 raleqbidv 
 |-  ( ph -> ( A. x e. A ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) <-> A. x e. ( Base ` S ) ( ( .0. ( +g ` S ) x ) = x /\ ( x ( +g ` S ) .0. ) = x ) ) )
25 13 24 sylibd 
 |-  ( ph -> ( A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) -> A. x e. ( Base ` S ) ( ( .0. ( +g ` S ) x ) = x /\ ( x ( +g ` S ) .0. ) = x ) ) )
26 25 adantld 
 |-  ( ph -> ( ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) -> A. x e. ( Base ` S ) ( ( .0. ( +g ` S ) x ) = x /\ ( x ( +g ` S ) .0. ) = x ) ) )
27 11 26 mpd 
 |-  ( ph -> A. x e. ( Base ` S ) ( ( .0. ( +g ` S ) x ) = x /\ ( x ( +g ` S ) .0. ) = x ) )
28 eqid 
 |-  ( Base ` S ) = ( Base ` S )
29 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
30 eqid 
 |-  ( +g ` S ) = ( +g ` S )
31 1 2 3 4 5 6 7 28 idressidex0 
 |-  ( ph -> E. e e. ( Base ` S ) A. x e. ( Base ` S ) ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
32 18 eqcomd 
 |-  ( ph -> ( +g ` S ) = .+ )
33 32 oveqd 
 |-  ( ph -> ( e ( +g ` S ) x ) = ( e .+ x ) )
34 33 eqeq1d 
 |-  ( ph -> ( ( e ( +g ` S ) x ) = x <-> ( e .+ x ) = x ) )
35 32 oveqd 
 |-  ( ph -> ( x ( +g ` S ) e ) = ( x .+ e ) )
36 35 eqeq1d 
 |-  ( ph -> ( ( x ( +g ` S ) e ) = x <-> ( x .+ e ) = x ) )
37 34 36 anbi12d 
 |-  ( ph -> ( ( ( e ( +g ` S ) x ) = x /\ ( x ( +g ` S ) e ) = x ) <-> ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
38 37 ralbidv 
 |-  ( ph -> ( A. x e. ( Base ` S ) ( ( e ( +g ` S ) x ) = x /\ ( x ( +g ` S ) e ) = x ) <-> A. x e. ( Base ` S ) ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
39 38 rexbidv 
 |-  ( ph -> ( E. e e. ( Base ` S ) A. x e. ( Base ` S ) ( ( e ( +g ` S ) x ) = x /\ ( x ( +g ` S ) e ) = x ) <-> E. e e. ( Base ` S ) A. x e. ( Base ` S ) ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
40 31 39 mpbird 
 |-  ( ph -> E. e e. ( Base ` S ) A. x e. ( Base ` S ) ( ( e ( +g ` S ) x ) = x /\ ( x ( +g ` S ) e ) = x ) )
41 28 29 30 40 ismgmid 
 |-  ( ph -> ( ( .0. e. ( Base ` S ) /\ A. x e. ( Base ` S ) ( ( .0. ( +g ` S ) x ) = x /\ ( x ( +g ` S ) .0. ) = x ) ) <-> ( 0g ` S ) = .0. ) )
42 10 27 41 mpbi2and 
 |-  ( ph -> ( 0g ` S ) = .0. )