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

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 5 1 ressbas2 ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( Base ‘ 𝑆 ) )
9 6 8 syl ⊢ ( 𝜑 → 𝐴 = ( Base ‘ 𝑆 ) )
10 7 9 eleqtrd ⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑆 ) )
11 1 3 2 4 0gisid ⊢ ( 𝜑 → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
12 ssralv ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
13 6 12 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
14 1 fvexi ⊢ 𝐵 ∈ V
15 14 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
16 15 6 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
17 5 2 ressplusg ⊢ ( 𝐴 ∈ V → + = ( +g ‘ 𝑆 ) )
18 16 17 syl ⊢ ( 𝜑 → + = ( +g ‘ 𝑆 ) )
19 18 oveqd ⊢ ( 𝜑 → ( 0 + 𝑥 ) = ( 0 ( +g ‘ 𝑆 ) 𝑥 ) )
20 19 eqeq1d ⊢ ( 𝜑 → ( ( 0 + 𝑥 ) = 𝑥 ↔ ( 0 ( +g ‘ 𝑆 ) 𝑥 ) = 𝑥 ) )
21 18 oveqd ⊢ ( 𝜑 → ( 𝑥 + 0 ) = ( 𝑥 ( +g ‘ 𝑆 ) 0 ) )
22 21 eqeq1d ⊢ ( 𝜑 → ( ( 𝑥 + 0 ) = 𝑥 ↔ ( 𝑥 ( +g ‘ 𝑆 ) 0 ) = 𝑥 ) )
23 20 22 anbi12d ⊢ ( 𝜑 → ( ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ↔ ( ( 0 ( +g ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑆 ) 0 ) = 𝑥 ) ) )
24 9 23 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 0 ( +g ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑆 ) 0 ) = 𝑥 ) ) )
25 13 24 sylibd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 0 ( +g ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑆 ) 0 ) = 𝑥 ) ) )
26 25 adantld ⊢ ( 𝜑 → ( ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 0 ( +g ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑆 ) 0 ) = 𝑥 ) ) )
27 11 26 mpd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 0 ( +g ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑆 ) 0 ) = 𝑥 ) )
28 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
29 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
30 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
31 1 2 3 4 5 6 7 28 idressidex0 ⊢ ( 𝜑 → ∃ 𝑒 ∈ ( Base ‘ 𝑆 ) ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
32 18 eqcomd ⊢ ( 𝜑 → ( +g ‘ 𝑆 ) = + )
33 32 oveqd ⊢ ( 𝜑 → ( 𝑒 ( +g ‘ 𝑆 ) 𝑥 ) = ( 𝑒 + 𝑥 ) )
34 33 eqeq1d ⊢ ( 𝜑 → ( ( 𝑒 ( +g ‘ 𝑆 ) 𝑥 ) = 𝑥 ↔ ( 𝑒 + 𝑥 ) = 𝑥 ) )
35 32 oveqd ⊢ ( 𝜑 → ( 𝑥 ( +g ‘ 𝑆 ) 𝑒 ) = ( 𝑥 + 𝑒 ) )
36 35 eqeq1d ⊢ ( 𝜑 → ( ( 𝑥 ( +g ‘ 𝑆 ) 𝑒 ) = 𝑥 ↔ ( 𝑥 + 𝑒 ) = 𝑥 ) )
37 34 36 anbi12d ⊢ ( 𝜑 → ( ( ( 𝑒 ( +g ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑆 ) 𝑒 ) = 𝑥 ) ↔ ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
38 37 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑒 ( +g ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑆 ) 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
39 38 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑒 ∈ ( Base ‘ 𝑆 ) ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑒 ( +g ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑆 ) 𝑒 ) = 𝑥 ) ↔ ∃ 𝑒 ∈ ( Base ‘ 𝑆 ) ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
40 31 39 mpbird ⊢ ( 𝜑 → ∃ 𝑒 ∈ ( Base ‘ 𝑆 ) ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑒 ( +g ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑆 ) 𝑒 ) = 𝑥 ) )
41 28 29 30 40 ismgmid ⊢ ( 𝜑 → ( ( 0 ∈ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 0 ( +g ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑆 ) 0 ) = 𝑥 ) ) ↔ ( 0g ‘ 𝑆 ) = 0 ) )
42 10 27 41 mpbi2and ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = 0 )