Definition df-minusg

Description: Define inverse of group element. (Contributed by NM, 24-Aug-2011)

	Ref	Expression
Assertion	df-minusg	⊢ invg = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑤 ∈ ( Base ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cminusg	⊢ invg
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Base ‘ 𝑔 )
7		vw	⊢ 𝑤
8	7	cv	⊢ 𝑤
9		cplusg	⊢ +g
10	5 9	cfv	⊢ ( +g ‘ 𝑔 )
11	3	cv	⊢ 𝑥
12	8 11 10	co	⊢ ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 )
13		c0g	⊢ 0g
14	5 13	cfv	⊢ ( 0g ‘ 𝑔 )
15	12 14	wceq	⊢ ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 )
16	15 7 6	crio	⊢ ( ℩ 𝑤 ∈ ( Base ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) )
17	3 6 16	cmpt	⊢ ( 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑤 ∈ ( Base ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) ) )
18	1 2 17	cmpt	⊢ ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑤 ∈ ( Base ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) ) ) )
19	0 18	wceq	⊢ invg = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑤 ∈ ( Base ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) ) ) )