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

Proof

Step	Hyp	Ref	Expression
1		idressidex.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		idressidex.p	⊢ + = ( +_g ‘ 𝐺 )
3		idressidex.o	⊢ 0 = ( 0_g ‘ 𝐺 )
4		idressidex.e	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
5		idressidex.s	⊢ 𝑆 = ( 𝐺 ↾_s 𝐴 )
6		idressidex.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
7		idressidex.0	⊢ ( 𝜑 → 0 ∈ 𝐴 )
8		idressidex0.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
9	1 3 2 4	0gisid	⊢ ( 𝜑 → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
10	5 1	ressbas2	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( Base ‘ 𝑆 ) )
11	6 10	syl	⊢ ( 𝜑 → 𝐴 = ( Base ‘ 𝑆 ) )
12	8 11	eqtr4id	⊢ ( 𝜑 → 𝐶 = 𝐴 )
13	7 12	eleqtrrd	⊢ ( 𝜑 → 0 ∈ 𝐶 )
14	5 1	ressbasss	⊢ ( Base ‘ 𝑆 ) ⊆ 𝐵
15	8 14	eqsstri	⊢ 𝐶 ⊆ 𝐵
16		ssralv	⊢ ( 𝐶 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝐶 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
17	15 16	mp1i	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝐶 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
18	17	adantld	⊢ ( 𝜑 → ( ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) → ∀ 𝑥 ∈ 𝐶 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑒 = 0 ) → ( ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) → ∀ 𝑥 ∈ 𝐶 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
20		oveq1	⊢ ( 𝑒 = 0 → ( 𝑒 + 𝑥 ) = ( 0 + 𝑥 ) )
21	20	eqeq1d	⊢ ( 𝑒 = 0 → ( ( 𝑒 + 𝑥 ) = 𝑥 ↔ ( 0 + 𝑥 ) = 𝑥 ) )
22	21	ovanraleqv	⊢ ( 𝑒 = 0 → ( ∀ 𝑥 ∈ 𝐶 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐶 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝑒 = 0 ) → ( ∀ 𝑥 ∈ 𝐶 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐶 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
24	19 23	sylibrd	⊢ ( ( 𝜑 ∧ 𝑒 = 0 ) → ( ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) → ∀ 𝑥 ∈ 𝐶 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
25	13 24	rspcimedv	⊢ ( 𝜑 → ( ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) → ∃ 𝑒 ∈ 𝐶 ∀ 𝑥 ∈ 𝐶 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
26	9 25	mpd	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐶 ∀ 𝑥 ∈ 𝐶 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )

Metamath Proof Explorer

Theorem idressidex0

Proof