Metamath Proof Explorer

Theorem isexid2

Description: If G e. ( Magma i^i ExId ) , then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis isexid2.1 ⊢ 𝑋 = ran 𝐺
Assertion isexid2 ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )

Proof

Step Hyp Ref Expression
1 isexid2.1 ⊢ 𝑋 = ran 𝐺
2 rngopidOLD ⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ran 𝐺 = dom dom 𝐺 )
3 elin ⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) ↔ ( 𝐺 ∈ Magma ∧ 𝐺 ∈ ExId ) )
4 eqid ⊢ dom dom 𝐺 = dom dom 𝐺
5 4 isexid ⊢ ( 𝐺 ∈ ExId → ( 𝐺 ∈ ExId ↔ ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
6 5 ibi ⊢ ( 𝐺 ∈ ExId → ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )
7 6 a1d ⊢ ( 𝐺 ∈ ExId → ( 𝑋 = dom dom 𝐺 → ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
8 7 adantl ⊢ ( ( 𝐺 ∈ Magma ∧ 𝐺 ∈ ExId ) → ( 𝑋 = dom dom 𝐺 → ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
9 3 8 sylbi ⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝑋 = dom dom 𝐺 → ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
10 eqeq2 ⊢ ( ran 𝐺 = dom dom 𝐺 → ( 𝑋 = ran 𝐺 ↔ 𝑋 = dom dom 𝐺 ) )
11 raleq ⊢ ( ran 𝐺 = dom dom 𝐺 → ( ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
12 11 rexeqbi1dv ⊢ ( ran 𝐺 = dom dom 𝐺 → ( ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
13 10 12 imbi12d ⊢ ( ran 𝐺 = dom dom 𝐺 → ( ( 𝑋 = ran 𝐺 → ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ↔ ( 𝑋 = dom dom 𝐺 → ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) )
14 9 13 syl5ibr ⊢ ( ran 𝐺 = dom dom 𝐺 → ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝑋 = ran 𝐺 → ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) )
15 2 14 mpcom ⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝑋 = ran 𝐺 → ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
16 15 com12 ⊢ ( 𝑋 = ran 𝐺 → ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
17 raleq ⊢ ( 𝑋 = ran 𝐺 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
18 17 rexeqbi1dv ⊢ ( 𝑋 = ran 𝐺 → ( ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
19 16 18 sylibrd ⊢ ( 𝑋 = ran 𝐺 → ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
20 1 19 ax-mp ⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )