Theorem idressidex

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 )
Assertion	idressidex	|- ( ph -> E. e e. A A. x e. A ( ( 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		eqid	|- ( Base ` S ) = ( Base ` S )
9	1 2 3 4 5 6 7 8	idressidex0	|- ( ph -> E. e e. ( Base ` S ) A. x e. ( Base ` S ) ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
10	5 1	ressbas2	|- ( A C_ B -> A = ( Base ` S ) )
11		id	|- ( A = ( Base ` S ) -> A = ( Base ` S ) )
12		raleq	|- ( A = ( Base ` S ) -> ( A. x e. A ( ( e .+ x ) = x /\ ( x .+ e ) = x ) <-> A. x e. ( Base ` S ) ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
13	11 12	rexeqbidv	|- ( A = ( Base ` S ) -> ( E. e e. A A. x e. A ( ( e .+ x ) = x /\ ( x .+ e ) = x ) <-> E. e e. ( Base ` S ) A. x e. ( Base ` S ) ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
14	6 10 13	3syl	|- ( ph -> ( E. e e. A A. x e. A ( ( e .+ x ) = x /\ ( x .+ e ) = x ) <-> E. e e. ( Base ` S ) A. x e. ( Base ` S ) ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
15	9 14	mpbird	|- ( ph -> E. e e. A A. x e. A ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )