Metamath Proof Explorer

Theorem 0gisid

Description: In a structure with an identity element, the group identity element is an identity element of the structure. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013) (Revised by AV, 11-Aug-2026)

Ref Expression
Hypotheses ismgmid.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ismgmid.o ⊢ 0 = ( 0g ‘ 𝐺 )
ismgmid.p ⊢ + = ( +g ‘ 𝐺 )
mgmidcl.e ⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
Assertion 0gisid ( 𝜑 → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 ismgmid.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ismgmid.o ⊢ 0 = ( 0g ‘ 𝐺 )
3 ismgmid.p ⊢ + = ( +g ‘ 𝐺 )
4 mgmidcl.e ⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
5 oveq1 ⊢ ( 𝑒 = 𝑖 → ( 𝑒 + 𝑥 ) = ( 𝑖 + 𝑥 ) )
6 5 eqeq1d ⊢ ( 𝑒 = 𝑖 → ( ( 𝑒 + 𝑥 ) = 𝑥 ↔ ( 𝑖 + 𝑥 ) = 𝑥 ) )
7 6 ovanraleqv ⊢ ( 𝑒 = 𝑖 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑖 ) = 𝑥 ) ) )
8 7 cbvrexvw ⊢ ( ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∃ 𝑖 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑖 ) = 𝑥 ) )
9 1 2 3 4 ismgmid ⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑖 ) = 𝑥 ) ) ↔ 0 = 𝑖 ) )
10 9 biimpa ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑖 ) = 𝑥 ) ) ) → 0 = 𝑖 )
11 eleq1 ⊢ ( 𝑖 = 0 → ( 𝑖 ∈ 𝐵 ↔ 0 ∈ 𝐵 ) )
12 oveq1 ⊢ ( 𝑖 = 0 → ( 𝑖 + 𝑥 ) = ( 0 + 𝑥 ) )
13 12 eqeq1d ⊢ ( 𝑖 = 0 → ( ( 𝑖 + 𝑥 ) = 𝑥 ↔ ( 0 + 𝑥 ) = 𝑥 ) )
14 13 ovanraleqv ⊢ ( 𝑖 = 0 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑖 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
15 11 14 anbi12d ⊢ ( 𝑖 = 0 → ( ( 𝑖 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑖 ) = 𝑥 ) ) ↔ ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) ) )
16 15 eqcoms ⊢ ( 0 = 𝑖 → ( ( 𝑖 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑖 ) = 𝑥 ) ) ↔ ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ 0 = 𝑖 ) → ( ( 𝑖 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑖 ) = 𝑥 ) ) ↔ ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) ) )
18 17 biimpd ⊢ ( ( 𝜑 ∧ 0 = 𝑖 ) → ( ( 𝑖 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑖 ) = 𝑥 ) ) → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) ) )
19 18 impancom ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑖 ) = 𝑥 ) ) ) → ( 0 = 𝑖 → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) ) )
20 10 19 mpd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑖 ) = 𝑥 ) ) ) → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
21 20 rexlimdvaa ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑖 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑖 ) = 𝑥 ) → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) ) )
22 8 21 biimtrid ⊢ ( 𝜑 → ( ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) ) )
23 4 22 mpd ⊢ ( 𝜑 → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )