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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	idressidex.p	⊢ + = ( +g ‘ 𝐺 )
	idressidex.o	⊢ 0 = ( 0g ‘ 𝐺 )
	idressidex.e	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
	idressidex.s	⊢ 𝑆 = ( 𝐺 ↾s 𝐴 )
	idressidex.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	idressidex.0	⊢ ( 𝜑 → 0 ∈ 𝐴 )
Assertion	idressidex	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		idressidex.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		idressidex.p	⊢ + = ( +g ‘ 𝐺 )
3		idressidex.o	⊢ 0 = ( 0g ‘ 𝐺 )
4		idressidex.e	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
5		idressidex.s	⊢ 𝑆 = ( 𝐺 ↾s 𝐴 )
6		idressidex.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
7		idressidex.0	⊢ ( 𝜑 → 0 ∈ 𝐴 )
8		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
9	1 2 3 4 5 6 7 8	idressidex0	⊢ ( 𝜑 → ∃ 𝑒 ∈ ( Base ‘ 𝑆 ) ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
10	5 1	ressbas2	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( Base ‘ 𝑆 ) )
11		id	⊢ ( 𝐴 = ( Base ‘ 𝑆 ) → 𝐴 = ( Base ‘ 𝑆 ) )
12		raleq	⊢ ( 𝐴 = ( Base ‘ 𝑆 ) → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
13	11 12	rexeqbidv	⊢ ( 𝐴 = ( Base ‘ 𝑆 ) → ( ∃ 𝑒 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∃ 𝑒 ∈ ( Base ‘ 𝑆 ) ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
14	6 10 13	3syl	⊢ ( 𝜑 → ( ∃ 𝑒 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∃ 𝑒 ∈ ( Base ‘ 𝑆 ) ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
15	9 14	mpbird	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )