This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-gid

Description: Define a function that maps a group operation to the group's identity element. (Contributed by FL, 5-Feb-2010) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion df-gid GId = ( 𝑔 ∈ V ↦ ( ℩ 𝑢 ∈ ran 𝑔 ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgi ⊢ GId
1 vg ⊢ 𝑔
2 cvv ⊢ V
3 vu ⊢ 𝑢
4 1 cv ⊢ 𝑔
5 4 crn ⊢ ran 𝑔
6 vx ⊢ 𝑥
7 3 cv ⊢ 𝑢
8 6 cv ⊢ 𝑥
9 7 8 4 co ⊢ ( 𝑢 𝑔 𝑥 )
10 9 8 wceq ⊢ ( 𝑢 𝑔 𝑥 ) = 𝑥
11 8 7 4 co ⊢ ( 𝑥 𝑔 𝑢 )
12 11 8 wceq ⊢ ( 𝑥 𝑔 𝑢 ) = 𝑥
13 10 12 wa ⊢ ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 )
14 13 6 5 wral ⊢ ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 )
15 14 3 5 crio ⊢ ( ℩ 𝑢 ∈ ran 𝑔 ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 ) )
16 1 2 15 cmpt ⊢ ( 𝑔 ∈ V ↦ ( ℩ 𝑢 ∈ ran 𝑔 ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 ) ) )
17 0 16 wceq ⊢ GId = ( 𝑔 ∈ V ↦ ( ℩ 𝑢 ∈ ran 𝑔 ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 ) ) )