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 ‘ 𝐻 ) = 𝑈 )