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

Metamath Proof Explorer

Theorem grpoinvval

Description: The inverse of a group element. (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 grpoinvval ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )

Proof

Step Hyp Ref Expression
1 grpinvfval.1 ⊢ 𝑋 = ran 𝐺
2 grpinvfval.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
3 grpinvfval.3 ⊢ 𝑁 = ( inv ‘ 𝐺 )
4 1 2 3 grpoinvfval ⊢ ( 𝐺 ∈ GrpOp → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )
5 4 fveq1d ⊢ ( 𝐺 ∈ GrpOp → ( 𝑁 ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) ‘ 𝐴 ) )
6 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑦 𝐺 𝑥 ) = ( 𝑦 𝐺 𝐴 ) )
7 6 eqeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ↔ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
8 7 riotabidv ⊢ ( 𝑥 = 𝐴 → ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) = ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
9 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
10 riotaex ⊢ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) ∈ V
11 8 9 10 fvmpt ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) ‘ 𝐴 ) = ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
12 5 11 sylan9eq ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )