Metamath Proof Explorer


Theorem exidresid

Description: The restriction of a binary operation with identity to a subset containing the identity has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013)

Ref Expression
Hypotheses exidres.1 𝑋 = ran 𝐺
exidres.2 𝑈 = ( GId ‘ 𝐺 )
exidres.3 𝐻 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) )
Assertion exidresid ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) ∧ 𝐻 ∈ Magma ) → ( GId ‘ 𝐻 ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 exidres.1 𝑋 = ran 𝐺
2 exidres.2 𝑈 = ( GId ‘ 𝐺 )
3 exidres.3 𝐻 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) )
4 resexg ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ∈ V )
5 3 4 eqeltrid ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐻 ∈ V )
6 eqid ran 𝐻 = ran 𝐻
7 6 gidval ( 𝐻 ∈ V → ( GId ‘ 𝐻 ) = ( 𝑢 ∈ ran 𝐻𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) )
8 5 7 syl ( 𝐺 ∈ ( Magma ∩ ExId ) → ( GId ‘ 𝐻 ) = ( 𝑢 ∈ ran 𝐻𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) )
9 8 3ad2ant1 ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → ( GId ‘ 𝐻 ) = ( 𝑢 ∈ ran 𝐻𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) )
10 9 adantr ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) ∧ 𝐻 ∈ Magma ) → ( GId ‘ 𝐻 ) = ( 𝑢 ∈ ran 𝐻𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) )
11 1 2 3 exidreslem ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → ( 𝑈 ∈ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) )
12 11 simprd ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) )
13 12 adantr ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) ∧ 𝐻 ∈ Magma ) → ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) )
14 1 2 3 exidres ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → 𝐻 ∈ ExId )
15 elin ( 𝐻 ∈ ( Magma ∩ ExId ) ↔ ( 𝐻 ∈ Magma ∧ 𝐻 ∈ ExId ) )
16 rngopidOLD ( 𝐻 ∈ ( Magma ∩ ExId ) → ran 𝐻 = dom dom 𝐻 )
17 15 16 sylbir ( ( 𝐻 ∈ Magma ∧ 𝐻 ∈ ExId ) → ran 𝐻 = dom dom 𝐻 )
18 17 ancoms ( ( 𝐻 ∈ ExId ∧ 𝐻 ∈ Magma ) → ran 𝐻 = dom dom 𝐻 )
19 14 18 sylan ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) ∧ 𝐻 ∈ Magma ) → ran 𝐻 = dom dom 𝐻 )
20 19 raleqdv ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) ∧ 𝐻 ∈ Magma ) → ( ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) )
21 13 20 mpbird ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) ∧ 𝐻 ∈ Magma ) → ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) )
22 11 simpld ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → 𝑈 ∈ dom dom 𝐻 )
23 22 adantr ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) ∧ 𝐻 ∈ Magma ) → 𝑈 ∈ dom dom 𝐻 )
24 23 19 eleqtrrd ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) ∧ 𝐻 ∈ Magma ) → 𝑈 ∈ ran 𝐻 )
25 6 exidu1 ( 𝐻 ∈ ( Magma ∩ ExId ) → ∃! 𝑢 ∈ ran 𝐻𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
26 15 25 sylbir ( ( 𝐻 ∈ Magma ∧ 𝐻 ∈ ExId ) → ∃! 𝑢 ∈ ran 𝐻𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
27 26 ancoms ( ( 𝐻 ∈ ExId ∧ 𝐻 ∈ Magma ) → ∃! 𝑢 ∈ ran 𝐻𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
28 14 27 sylan ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) ∧ 𝐻 ∈ Magma ) → ∃! 𝑢 ∈ ran 𝐻𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
29 oveq1 ( 𝑢 = 𝑈 → ( 𝑢 𝐻 𝑥 ) = ( 𝑈 𝐻 𝑥 ) )
30 29 eqeq1d ( 𝑢 = 𝑈 → ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐻 𝑥 ) = 𝑥 ) )
31 30 ovanraleqv ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) )
32 31 riota2 ( ( 𝑈 ∈ ran 𝐻 ∧ ∃! 𝑢 ∈ ran 𝐻𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) → ( ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ↔ ( 𝑢 ∈ ran 𝐻𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) = 𝑈 ) )
33 24 28 32 syl2anc ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) ∧ 𝐻 ∈ Magma ) → ( ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ↔ ( 𝑢 ∈ ran 𝐻𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) = 𝑈 ) )
34 21 33 mpbid ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) ∧ 𝐻 ∈ Magma ) → ( 𝑢 ∈ ran 𝐻𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) = 𝑈 )
35 10 34 eqtrd ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) ∧ 𝐻 ∈ Magma ) → ( GId ‘ 𝐻 ) = 𝑈 )