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→UGA=A∧AGU=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∈XuGx=x∧xGu=x
4 3 eqcomd ⊢G∈Magma∩ExId→ιu∈X|∀x∈XuGx=x∧xGu=x=U
5 1 2 iorlid ⊢G∈Magma∩ExId→U∈X
6 1 exidu1 ⊢G∈Magma∩ExId→∃!u∈X∀x∈XuGx=x∧xGu=x
7 oveq1 ⊢u=U→uGx=UGx
8 7 eqeq1d ⊢u=U→uGx=x↔UGx=x
9 8 ovanraleqv ⊢u=U→∀x∈XuGx=x∧xGu=x↔∀x∈XUGx=x∧xGU=x
10 9 riota2 ⊢U∈X∧∃!u∈X∀x∈XuGx=x∧xGu=x→∀x∈XUGx=x∧xGU=x↔ιu∈X|∀x∈XuGx=x∧xGu=x=U
11 5 6 10 syl2anc ⊢G∈Magma∩ExId→∀x∈XUGx=x∧xGU=x↔ιu∈X|∀x∈XuGx=x∧xGu=x=U
12 4 11 mpbird ⊢G∈Magma∩ExId→∀x∈XUGx=x∧xGU=x
13 oveq2 ⊢x=A→UGx=UGA
14 id ⊢x=A→x=A
15 13 14 eqeq12d ⊢x=A→UGx=x↔UGA=A
16 oveq1 ⊢x=A→xGU=AGU
17 16 14 eqeq12d ⊢x=A→xGU=x↔AGU=A
18 15 17 anbi12d ⊢x=A→UGx=x∧xGU=x↔UGA=A∧AGU=A
19 18 rspccva ⊢∀x∈XUGx=x∧xGU=x∧A∈X→UGA=A∧AGU=A
20 12 19 sylan ⊢G∈Magma∩ExId∧A∈X→UGA=A∧AGU=A