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

Metamath Proof Explorer

Definition df-ginv

Description: Define a function that maps a group operation to the group's inverse function. (Contributed by NM, 26-Oct-2006) (New usage is discouraged.)

Ref Expression
Assertion df-ginv inv = ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 ↦ ( ℩ 𝑧 ∈ ran 𝑔 ( 𝑧 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgn ⊢ inv
1 vg ⊢ 𝑔
2 cgr ⊢ GrpOp
3 vx ⊢ 𝑥
4 1 cv ⊢ 𝑔
5 4 crn ⊢ ran 𝑔
6 vz ⊢ 𝑧
7 6 cv ⊢ 𝑧
8 3 cv ⊢ 𝑥
9 7 8 4 co ⊢ ( 𝑧 𝑔 𝑥 )
10 cgi ⊢ GId
11 4 10 cfv ⊢ ( GId ‘ 𝑔 )
12 9 11 wceq ⊢ ( 𝑧 𝑔 𝑥 ) = ( GId ‘ 𝑔 )
13 12 6 5 crio ⊢ ( ℩ 𝑧 ∈ ran 𝑔 ( 𝑧 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) )
14 3 5 13 cmpt ⊢ ( 𝑥 ∈ ran 𝑔 ↦ ( ℩ 𝑧 ∈ ran 𝑔 ( 𝑧 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) )
15 1 2 14 cmpt ⊢ ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 ↦ ( ℩ 𝑧 ∈ ran 𝑔 ( 𝑧 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) ) )
16 0 15 wceq ⊢ inv = ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 ↦ ( ℩ 𝑧 ∈ ran 𝑔 ( 𝑧 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) ) )