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

Metamath Proof Explorer

Theorem grpoinvfval

Description: The inverse function of a group. (Contributed by NM, 26-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpinvfval.1 ⊢ 𝑋 = ran 𝐺
grpinvfval.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
grpinvfval.3 ⊢ 𝑁 = ( inv ‘ 𝐺 )
Assertion grpoinvfval ( 𝐺 ∈ GrpOp → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 grpinvfval.1 ⊢ 𝑋 = ran 𝐺
2 grpinvfval.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
3 grpinvfval.3 ⊢ 𝑁 = ( inv ‘ 𝐺 )
4 rnexg ⊢ ( 𝐺 ∈ GrpOp → ran 𝐺 ∈ V )
5 1 4 eqeltrid ⊢ ( 𝐺 ∈ GrpOp → 𝑋 ∈ V )
6 mptexg ⊢ ( 𝑋 ∈ V → ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) ∈ V )
7 5 6 syl ⊢ ( 𝐺 ∈ GrpOp → ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) ∈ V )
8 rneq ⊢ ( 𝑔 = 𝐺 → ran 𝑔 = ran 𝐺 )
9 8 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ran 𝑔 = 𝑋 )
10 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑦 𝑔 𝑥 ) = ( 𝑦 𝐺 𝑥 ) )
11 fveq2 ⊢ ( 𝑔 = 𝐺 → ( GId ‘ 𝑔 ) = ( GId ‘ 𝐺 ) )
12 11 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( GId ‘ 𝑔 ) = 𝑈 )
13 10 12 eqeq12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑦 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ↔ ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
14 9 13 riotaeqbidv ⊢ ( 𝑔 = 𝐺 → ( ℩ 𝑦 ∈ ran 𝑔 ( 𝑦 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) = ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
15 9 14 mpteq12dv ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ ran 𝑔 ↦ ( ℩ 𝑦 ∈ ran 𝑔 ( 𝑦 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )
16 df-ginv ⊢ inv = ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 ↦ ( ℩ 𝑦 ∈ ran 𝑔 ( 𝑦 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) ) )
17 15 16 fvmptg ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) ∈ V ) → ( inv ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )
18 7 17 mpdan ⊢ ( 𝐺 ∈ GrpOp → ( inv ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )
19 3 18 eqtrid ⊢ ( 𝐺 ∈ GrpOp → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )