Metamath Proof Explorer

Theorem mgmidmo

Description: A two-sided identity element is unique (if it exists) in any magma. (Contributed by Mario Carneiro, 7-Dec-2014) (Revised by NM, 17-Jun-2017)

Ref Expression
Assertion mgmidmo ∃* 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) → ( 𝑢 + 𝑥 ) = 𝑥 )
2 1 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑢 + 𝑥 ) = 𝑥 )
3 simpr ⊢ ( ( ( 𝑤 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑤 ) = 𝑥 ) → ( 𝑥 + 𝑤 ) = 𝑥 )
4 3 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑤 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑤 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑤 ) = 𝑥 )
5 oveq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 + 𝑤 ) = ( 𝑢 + 𝑤 ) )
6 id ⊢ ( 𝑥 = 𝑢 → 𝑥 = 𝑢 )
7 5 6 eqeq12d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 + 𝑤 ) = 𝑥 ↔ ( 𝑢 + 𝑤 ) = 𝑢 ) )
8 7 rspcva ⊢ ( ( 𝑢 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑤 ) = 𝑥 ) → ( 𝑢 + 𝑤 ) = 𝑢 )
9 oveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑢 + 𝑥 ) = ( 𝑢 + 𝑤 ) )
10 id ⊢ ( 𝑥 = 𝑤 → 𝑥 = 𝑤 )
11 9 10 eqeq12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑢 + 𝑥 ) = 𝑥 ↔ ( 𝑢 + 𝑤 ) = 𝑤 ) )
12 11 rspcva ⊢ ( ( 𝑤 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑢 + 𝑥 ) = 𝑥 ) → ( 𝑢 + 𝑤 ) = 𝑤 )
13 8 12 sylan9req ⊢ ( ( ( 𝑢 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑤 ) = 𝑥 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑢 + 𝑥 ) = 𝑥 ) ) → 𝑢 = 𝑤 )
14 13 an42s ⊢ ( ( ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐵 ( 𝑢 + 𝑥 ) = 𝑥 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑤 ) = 𝑥 ) ) → 𝑢 = 𝑤 )
15 14 ex ⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( ∀ 𝑥 ∈ 𝐵 ( 𝑢 + 𝑥 ) = 𝑥 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑤 ) = 𝑥 ) → 𝑢 = 𝑤 ) )
16 2 4 15 syl2ani ⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑤 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑤 ) = 𝑥 ) ) → 𝑢 = 𝑤 ) )
17 16 rgen2 ⊢ ∀ 𝑢 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑤 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑤 ) = 𝑥 ) ) → 𝑢 = 𝑤 )
18 oveq1 ⊢ ( 𝑢 = 𝑤 → ( 𝑢 + 𝑥 ) = ( 𝑤 + 𝑥 ) )
19 18 eqeq1d ⊢ ( 𝑢 = 𝑤 → ( ( 𝑢 + 𝑥 ) = 𝑥 ↔ ( 𝑤 + 𝑥 ) = 𝑥 ) )
20 19 ovanraleqv ⊢ ( 𝑢 = 𝑤 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑤 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑤 ) = 𝑥 ) ) )
21 20 rmo4 ⊢ ( ∃* 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ↔ ∀ 𝑢 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑤 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑤 ) = 𝑥 ) ) → 𝑢 = 𝑤 ) )
22 17 21 mpbir ⊢ ∃* 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 )