# 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 𝑋 = ran 𝐺
cmpidelt.2 𝑈 = ( GId ‘ 𝐺 )
Assertion cmpidelt ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝐴𝑋 ) → ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) )

### Proof

Step Hyp Ref Expression
1 cmpidelt.1 𝑋 = ran 𝐺
2 cmpidelt.2 𝑈 = ( GId ‘ 𝐺 )
3 1 2 idrval ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝑈 = ( 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
4 3 eqcomd ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) = 𝑈 )
5 1 2 iorlid ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝑈𝑋 )
6 1 exidu1 ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃! 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )
7 oveq1 ( 𝑢 = 𝑈 → ( 𝑢 𝐺 𝑥 ) = ( 𝑈 𝐺 𝑥 ) )
8 7 eqeq1d ( 𝑢 = 𝑈 → ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐺 𝑥 ) = 𝑥 ) )
9 8 ovanraleqv ( 𝑢 = 𝑈 → ( ∀ 𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥𝑋 ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ) )
10 9 riota2 ( ( 𝑈𝑋 ∧ ∃! 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) → ( ∀ 𝑥𝑋 ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ↔ ( 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) = 𝑈 ) )
11 5 6 10 syl2anc ( 𝐺 ∈ ( Magma ∩ ExId ) → ( ∀ 𝑥𝑋 ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ↔ ( 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) = 𝑈 ) )
12 4 11 mpbird ( 𝐺 ∈ ( Magma ∩ ExId ) → ∀ 𝑥𝑋 ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) )
13 oveq2 ( 𝑥 = 𝐴 → ( 𝑈 𝐺 𝑥 ) = ( 𝑈 𝐺 𝐴 ) )
14 id ( 𝑥 = 𝐴𝑥 = 𝐴 )
15 13 14 eqeq12d ( 𝑥 = 𝐴 → ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐺 𝐴 ) = 𝐴 ) )
16 oveq1 ( 𝑥 = 𝐴 → ( 𝑥 𝐺 𝑈 ) = ( 𝐴 𝐺 𝑈 ) )
17 16 14 eqeq12d ( 𝑥 = 𝐴 → ( ( 𝑥 𝐺 𝑈 ) = 𝑥 ↔ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) )
18 15 17 anbi12d ( 𝑥 = 𝐴 → ( ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ↔ ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) ) )
19 18 rspccva ( ( ∀ 𝑥𝑋 ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ∧ 𝐴𝑋 ) → ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) )
20 12 19 sylan ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝐴𝑋 ) → ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) )