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

Metamath Proof Explorer

Definition df-0g

Description: Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum . The related theorems are provided later, see grpidval . (Contributed by NM, 20-Aug-2011)

Ref Expression
Assertion df-0g 0g = ( 𝑔 ∈ V ↦ ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g ‘ 𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑔 ) 𝑒 ) = 𝑥 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c0g ⊢ 0g
1 vg ⊢ 𝑔
2 cvv ⊢ V
3 ve ⊢ 𝑒
4 3 cv ⊢ 𝑒
5 cbs ⊢ Base
6 1 cv ⊢ 𝑔
7 6 5 cfv ⊢ ( Base ‘ 𝑔 )
8 4 7 wcel ⊢ 𝑒 ∈ ( Base ‘ 𝑔 )
9 vx ⊢ 𝑥
10 cplusg ⊢ +g
11 6 10 cfv ⊢ ( +g ‘ 𝑔 )
12 9 cv ⊢ 𝑥
13 4 12 11 co ⊢ ( 𝑒 ( +g ‘ 𝑔 ) 𝑥 )
14 13 12 wceq ⊢ ( 𝑒 ( +g ‘ 𝑔 ) 𝑥 ) = 𝑥
15 12 4 11 co ⊢ ( 𝑥 ( +g ‘ 𝑔 ) 𝑒 )
16 15 12 wceq ⊢ ( 𝑥 ( +g ‘ 𝑔 ) 𝑒 ) = 𝑥
17 14 16 wa ⊢ ( ( 𝑒 ( +g ‘ 𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑔 ) 𝑒 ) = 𝑥 )
18 17 9 7 wral ⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g ‘ 𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑔 ) 𝑒 ) = 𝑥 )
19 8 18 wa ⊢ ( 𝑒 ∈ ( Base ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g ‘ 𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑔 ) 𝑒 ) = 𝑥 ) )
20 19 3 cio ⊢ ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g ‘ 𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑔 ) 𝑒 ) = 𝑥 ) ) )
21 1 2 20 cmpt ⊢ ( 𝑔 ∈ V ↦ ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g ‘ 𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑔 ) 𝑒 ) = 𝑥 ) ) ) )
22 0 21 wceq ⊢ 0g = ( 𝑔 ∈ V ↦ ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g ‘ 𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑔 ) 𝑒 ) = 𝑥 ) ) ) )