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𝑔 ) 𝑒 ) = 𝑥 ) ) ) )