**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 ) → ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) |

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 ) → ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) |