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

Metamath Proof Explorer

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 ‘ 𝑔 ) ) ) )