Metamath Proof Explorer

Theorem cmpidelt

Description: A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cmpidelt.1 ⊢ X = ran ⁡ G
cmpidelt.2 ⊢ U = GId ⁡ G
Assertion cmpidelt ⊢ G ∈ Magma ∩ ExId ∧ A ∈ X → U G A = A ∧ A G U = A

Proof

Step Hyp Ref Expression
1 cmpidelt.1 ⊢ X = ran ⁡ G
2 cmpidelt.2 ⊢ U = GId ⁡ G
3 1 2 idrval ⊢ G ∈ Magma ∩ ExId → U = ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x
4 3 eqcomd ⊢ G ∈ Magma ∩ ExId → ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x = U
5 1 2 iorlid ⊢ G ∈ Magma ∩ ExId → U ∈ X
6 1 exidu1 ⊢ G ∈ Magma ∩ ExId → ∃! u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x
7 oveq1 ⊢ u = U → u G x = U G x
8 7 eqeq1d ⊢ u = U → u G x = x ↔ U G x = x
9 8 ovanraleqv ⊢ u = U → ∀ x ∈ X u G x = x ∧ x G u = x ↔ ∀ x ∈ X U G x = x ∧ x G U = x
10 9 riota2 ⊢ U ∈ X ∧ ∃! u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x → ∀ x ∈ X U G x = x ∧ x G U = x ↔ ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x = U
11 5 6 10 syl2anc ⊢ G ∈ Magma ∩ ExId → ∀ x ∈ X U G x = x ∧ x G U = x ↔ ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x = U
12 4 11 mpbird ⊢ G ∈ Magma ∩ ExId → ∀ x ∈ X U G x = x ∧ x G U = x
13 oveq2 ⊢ x = A → U G x = U G A
14 id ⊢ x = A → x = A
15 13 14 eqeq12d ⊢ x = A → U G x = x ↔ U G A = A
16 oveq1 ⊢ x = A → x G U = A G U
17 16 14 eqeq12d ⊢ x = A → x G U = x ↔ A G U = A
18 15 17 anbi12d ⊢ x = A → U G x = x ∧ x G U = x ↔ U G A = A ∧ A G U = A
19 18 rspccva ⊢ ∀ x ∈ X U G x = x ∧ x G U = x ∧ A ∈ X → U G A = A ∧ A G U = A
20 12 19 sylan ⊢ G ∈ Magma ∩ ExId ∧ A ∈ X → U G A = A ∧ A G U = A