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 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) )