Metamath Proof Explorer

Theorem isgrpinv

Description: Properties showing that a function M is the inverse function of a group. (Contributed by NM, 7-Aug-2013) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses grpinv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
grpinv.p ⊢ + = ( +g ‘ 𝐺 )
grpinv.u ⊢ 0 = ( 0g ‘ 𝐺 )
grpinv.n ⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion isgrpinv ( 𝐺 ∈ Grp → ( ( 𝑀 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) ↔ 𝑁 = 𝑀 ) )

Proof

Step Hyp Ref Expression
1 grpinv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grpinv.p ⊢ + = ( +g ‘ 𝐺 )
3 grpinv.u ⊢ 0 = ( 0g ‘ 𝐺 )
4 grpinv.n ⊢ 𝑁 = ( invg ‘ 𝐺 )
5 1 2 3 4 grpinvval ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑁 ‘ 𝑥 ) = ( ℩ 𝑒 ∈ 𝐵 ( 𝑒 + 𝑥 ) = 0 ) )
6 5 ad2antlr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑀 : 𝐵 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) → ( 𝑁 ‘ 𝑥 ) = ( ℩ 𝑒 ∈ 𝐵 ( 𝑒 + 𝑥 ) = 0 ) )
7 simpr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑀 : 𝐵 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) → ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 )
8 simpllr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑀 : 𝐵 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) → 𝑀 : 𝐵 ⟶ 𝐵 )
9 simplr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑀 : 𝐵 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) → 𝑥 ∈ 𝐵 )
10 8 9 ffvelcdmd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑀 : 𝐵 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) → ( 𝑀 ‘ 𝑥 ) ∈ 𝐵 )
11 1 2 3 grpinveu ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑒 ∈ 𝐵 ( 𝑒 + 𝑥 ) = 0 )
12 11 ad4ant13 ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑀 : 𝐵 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) → ∃! 𝑒 ∈ 𝐵 ( 𝑒 + 𝑥 ) = 0 )
13 oveq1 ⊢ ( 𝑒 = ( 𝑀 ‘ 𝑥 ) → ( 𝑒 + 𝑥 ) = ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) )
14 13 eqeq1d ⊢ ( 𝑒 = ( 𝑀 ‘ 𝑥 ) → ( ( 𝑒 + 𝑥 ) = 0 ↔ ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) )
15 14 riota2 ⊢ ( ( ( 𝑀 ‘ 𝑥 ) ∈ 𝐵 ∧ ∃! 𝑒 ∈ 𝐵 ( 𝑒 + 𝑥 ) = 0 ) → ( ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ↔ ( ℩ 𝑒 ∈ 𝐵 ( 𝑒 + 𝑥 ) = 0 ) = ( 𝑀 ‘ 𝑥 ) ) )
16 10 12 15 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑀 : 𝐵 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) → ( ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ↔ ( ℩ 𝑒 ∈ 𝐵 ( 𝑒 + 𝑥 ) = 0 ) = ( 𝑀 ‘ 𝑥 ) ) )
17 7 16 mpbid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑀 : 𝐵 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) → ( ℩ 𝑒 ∈ 𝐵 ( 𝑒 + 𝑥 ) = 0 ) = ( 𝑀 ‘ 𝑥 ) )
18 6 17 eqtrd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑀 : 𝐵 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) → ( 𝑁 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) )
19 18 ex ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑀 : 𝐵 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 → ( 𝑁 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ) )
20 19 ralimdva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 : 𝐵 ⟶ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 → ∀ 𝑥 ∈ 𝐵 ( 𝑁 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ) )
21 20 impr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝑁 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) )
22 1 4 grpinvfn ⊢ 𝑁 Fn 𝐵
23 ffn ⊢ ( 𝑀 : 𝐵 ⟶ 𝐵 → 𝑀 Fn 𝐵 )
24 23 ad2antrl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) ) → 𝑀 Fn 𝐵 )
25 eqfnfv ⊢ ( ( 𝑁 Fn 𝐵 ∧ 𝑀 Fn 𝐵 ) → ( 𝑁 = 𝑀 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑁 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ) )
26 22 24 25 sylancr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) ) → ( 𝑁 = 𝑀 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑁 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ) )
27 21 26 mpbird ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) ) → 𝑁 = 𝑀 )
28 27 ex ⊢ ( 𝐺 ∈ Grp → ( ( 𝑀 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) → 𝑁 = 𝑀 ) )
29 1 4 grpinvf ⊢ ( 𝐺 ∈ Grp → 𝑁 : 𝐵 ⟶ 𝐵 )
30 1 2 3 4 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑥 ) + 𝑥 ) = 0 )
31 30 ralrimiva ⊢ ( 𝐺 ∈ Grp → ∀ 𝑥 ∈ 𝐵 ( ( 𝑁 ‘ 𝑥 ) + 𝑥 ) = 0 )
32 29 31 jca ⊢ ( 𝐺 ∈ Grp → ( 𝑁 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑁 ‘ 𝑥 ) + 𝑥 ) = 0 ) )
33 feq1 ⊢ ( 𝑁 = 𝑀 → ( 𝑁 : 𝐵 ⟶ 𝐵 ↔ 𝑀 : 𝐵 ⟶ 𝐵 ) )
34 fveq1 ⊢ ( 𝑁 = 𝑀 → ( 𝑁 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) )
35 34 oveq1d ⊢ ( 𝑁 = 𝑀 → ( ( 𝑁 ‘ 𝑥 ) + 𝑥 ) = ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) )
36 35 eqeq1d ⊢ ( 𝑁 = 𝑀 → ( ( ( 𝑁 ‘ 𝑥 ) + 𝑥 ) = 0 ↔ ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) )
37 36 ralbidv ⊢ ( 𝑁 = 𝑀 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑁 ‘ 𝑥 ) + 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) )
38 33 37 anbi12d ⊢ ( 𝑁 = 𝑀 → ( ( 𝑁 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑁 ‘ 𝑥 ) + 𝑥 ) = 0 ) ↔ ( 𝑀 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) ) )
39 32 38 syl5ibcom ⊢ ( 𝐺 ∈ Grp → ( 𝑁 = 𝑀 → ( 𝑀 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) ) )
40 28 39 impbid ⊢ ( 𝐺 ∈ Grp → ( ( 𝑀 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑀 ‘ 𝑥 ) + 𝑥 ) = 0 ) ↔ 𝑁 = 𝑀 ) )