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

Metamath Proof Explorer

Theorem grpinvval

Description: The inverse of a group element. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 7-Aug-2013)

Ref Expression
Hypotheses grpinvval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
grpinvval.p ⊢ + = ( +g ‘ 𝐺 )
grpinvval.o ⊢ 0 = ( 0g ‘ 𝐺 )
grpinvval.n ⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion grpinvval ( 𝑋 ∈ 𝐵 → ( 𝑁 ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 grpinvval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grpinvval.p ⊢ + = ( +g ‘ 𝐺 )
3 grpinvval.o ⊢ 0 = ( 0g ‘ 𝐺 )
4 grpinvval.n ⊢ 𝑁 = ( invg ‘ 𝐺 )
5 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑦 + 𝑥 ) = ( 𝑦 + 𝑋 ) )
6 5 eqeq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑦 + 𝑥 ) = 0 ↔ ( 𝑦 + 𝑋 ) = 0 ) )
7 6 riotabidv ⊢ ( 𝑥 = 𝑋 → ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 ) = ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ) )
8 1 2 3 4 grpinvfval ⊢ 𝑁 = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 ) )
9 riotaex ⊢ ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ) ∈ V
10 7 8 9 fvmpt ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ) )