Metamath Proof Explorer

Theorem exidu1

Description: Uniqueness of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis exidu1.1 ⊢ 𝑋 = ran 𝐺
Assertion exidu1 ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )

Proof

Step Hyp Ref Expression
1 exidu1.1 ⊢ 𝑋 = ran 𝐺
2 1 isexid2 ⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )
3 simpl ⊢ ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ( 𝑢 𝐺 𝑥 ) = 𝑥 )
4 3 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
5 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑢 𝐺 𝑥 ) = ( 𝑢 𝐺 𝑦 ) )
6 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
7 5 6 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑢 𝐺 𝑦 ) = 𝑦 ) )
8 7 rspcv ⊢ ( 𝑦 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 → ( 𝑢 𝐺 𝑦 ) = 𝑦 ) )
9 4 8 syl5 ⊢ ( 𝑦 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ( 𝑢 𝐺 𝑦 ) = 𝑦 ) )
10 simpr ⊢ ( ( ( 𝑦 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑥 ) → ( 𝑥 𝐺 𝑦 ) = 𝑥 )
11 10 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) = 𝑥 )
12 oveq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 𝐺 𝑦 ) = ( 𝑢 𝐺 𝑦 ) )
13 id ⊢ ( 𝑥 = 𝑢 → 𝑥 = 𝑢 )
14 12 13 eqeq12d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 𝐺 𝑦 ) = 𝑥 ↔ ( 𝑢 𝐺 𝑦 ) = 𝑢 ) )
15 14 rspcv ⊢ ( 𝑢 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) = 𝑥 → ( 𝑢 𝐺 𝑦 ) = 𝑢 ) )
16 11 15 syl5 ⊢ ( 𝑢 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑥 ) → ( 𝑢 𝐺 𝑦 ) = 𝑢 ) )
17 9 16 im2anan9r ⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑥 ) ) → ( ( 𝑢 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑢 𝐺 𝑦 ) = 𝑢 ) ) )
18 eqtr2 ⊢ ( ( ( 𝑢 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑢 𝐺 𝑦 ) = 𝑢 ) → 𝑦 = 𝑢 )
19 18 equcomd ⊢ ( ( ( 𝑢 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑢 𝐺 𝑦 ) = 𝑢 ) → 𝑢 = 𝑦 )
20 17 19 syl6 ⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑥 ) ) → 𝑢 = 𝑦 ) )
21 20 rgen2 ⊢ ∀ 𝑢 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑥 ) ) → 𝑢 = 𝑦 )
22 oveq1 ⊢ ( 𝑢 = 𝑦 → ( 𝑢 𝐺 𝑥 ) = ( 𝑦 𝐺 𝑥 ) )
23 22 eqeq1d ⊢ ( 𝑢 = 𝑦 → ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑦 𝐺 𝑥 ) = 𝑥 ) )
24 23 ovanraleqv ⊢ ( 𝑢 = 𝑦 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑥 ) ) )
25 24 reu4 ⊢ ( ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ( ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑥 ) ) → 𝑢 = 𝑦 ) ) )
26 2 21 25 sylanblrc ⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )