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