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 ∃* 𝑢𝐵𝑥𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 )