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

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 
|- B = ( Base ` G )
grpinv.p 
|- .+ = ( +g ` G )
grpinv.u 
|- .0. = ( 0g ` G )
grpinv.n 
|- N = ( invg ` G )
Assertion isgrpinv 
|- ( G e. Grp -> ( ( M : B --> B /\ A. x e. B ( ( M ` x ) .+ x ) = .0. ) <-> N = M ) )

Proof

Step Hyp Ref Expression
1 grpinv.b 
 |-  B = ( Base ` G )
2 grpinv.p 
 |-  .+ = ( +g ` G )
3 grpinv.u 
 |-  .0. = ( 0g ` G )
4 grpinv.n 
 |-  N = ( invg ` G )
5 1 2 3 4 grpinvval 
 |-  ( x e. B -> ( N ` x ) = ( iota_ e e. B ( e .+ x ) = .0. ) )
6 5 ad2antlr 
 |-  ( ( ( ( G e. Grp /\ M : B --> B ) /\ x e. B ) /\ ( ( M ` x ) .+ x ) = .0. ) -> ( N ` x ) = ( iota_ e e. B ( e .+ x ) = .0. ) )
7 simpr 
 |-  ( ( ( ( G e. Grp /\ M : B --> B ) /\ x e. B ) /\ ( ( M ` x ) .+ x ) = .0. ) -> ( ( M ` x ) .+ x ) = .0. )
8 simpllr 
 |-  ( ( ( ( G e. Grp /\ M : B --> B ) /\ x e. B ) /\ ( ( M ` x ) .+ x ) = .0. ) -> M : B --> B )
9 simplr 
 |-  ( ( ( ( G e. Grp /\ M : B --> B ) /\ x e. B ) /\ ( ( M ` x ) .+ x ) = .0. ) -> x e. B )
10 8 9 ffvelcdmd 
 |-  ( ( ( ( G e. Grp /\ M : B --> B ) /\ x e. B ) /\ ( ( M ` x ) .+ x ) = .0. ) -> ( M ` x ) e. B )
11 1 2 3 grpinveu 
 |-  ( ( G e. Grp /\ x e. B ) -> E! e e. B ( e .+ x ) = .0. )
12 11 ad4ant13 
 |-  ( ( ( ( G e. Grp /\ M : B --> B ) /\ x e. B ) /\ ( ( M ` x ) .+ x ) = .0. ) -> E! e e. B ( e .+ x ) = .0. )
13 oveq1 
 |-  ( e = ( M ` x ) -> ( e .+ x ) = ( ( M ` x ) .+ x ) )
14 13 eqeq1d 
 |-  ( e = ( M ` x ) -> ( ( e .+ x ) = .0. <-> ( ( M ` x ) .+ x ) = .0. ) )
15 14 riota2 
 |-  ( ( ( M ` x ) e. B /\ E! e e. B ( e .+ x ) = .0. ) -> ( ( ( M ` x ) .+ x ) = .0. <-> ( iota_ e e. B ( e .+ x ) = .0. ) = ( M ` x ) ) )
16 10 12 15 syl2anc 
 |-  ( ( ( ( G e. Grp /\ M : B --> B ) /\ x e. B ) /\ ( ( M ` x ) .+ x ) = .0. ) -> ( ( ( M ` x ) .+ x ) = .0. <-> ( iota_ e e. B ( e .+ x ) = .0. ) = ( M ` x ) ) )
17 7 16 mpbid 
 |-  ( ( ( ( G e. Grp /\ M : B --> B ) /\ x e. B ) /\ ( ( M ` x ) .+ x ) = .0. ) -> ( iota_ e e. B ( e .+ x ) = .0. ) = ( M ` x ) )
18 6 17 eqtrd 
 |-  ( ( ( ( G e. Grp /\ M : B --> B ) /\ x e. B ) /\ ( ( M ` x ) .+ x ) = .0. ) -> ( N ` x ) = ( M ` x ) )
19 18 ex 
 |-  ( ( ( G e. Grp /\ M : B --> B ) /\ x e. B ) -> ( ( ( M ` x ) .+ x ) = .0. -> ( N ` x ) = ( M ` x ) ) )
20 19 ralimdva 
 |-  ( ( G e. Grp /\ M : B --> B ) -> ( A. x e. B ( ( M ` x ) .+ x ) = .0. -> A. x e. B ( N ` x ) = ( M ` x ) ) )
21 20 impr 
 |-  ( ( G e. Grp /\ ( M : B --> B /\ A. x e. B ( ( M ` x ) .+ x ) = .0. ) ) -> A. x e. B ( N ` x ) = ( M ` x ) )
22 1 4 grpinvfn 
 |-  N Fn B
23 ffn 
 |-  ( M : B --> B -> M Fn B )
24 23 ad2antrl 
 |-  ( ( G e. Grp /\ ( M : B --> B /\ A. x e. B ( ( M ` x ) .+ x ) = .0. ) ) -> M Fn B )
25 eqfnfv 
 |-  ( ( N Fn B /\ M Fn B ) -> ( N = M <-> A. x e. B ( N ` x ) = ( M ` x ) ) )
26 22 24 25 sylancr 
 |-  ( ( G e. Grp /\ ( M : B --> B /\ A. x e. B ( ( M ` x ) .+ x ) = .0. ) ) -> ( N = M <-> A. x e. B ( N ` x ) = ( M ` x ) ) )
27 21 26 mpbird 
 |-  ( ( G e. Grp /\ ( M : B --> B /\ A. x e. B ( ( M ` x ) .+ x ) = .0. ) ) -> N = M )
28 27 ex 
 |-  ( G e. Grp -> ( ( M : B --> B /\ A. x e. B ( ( M ` x ) .+ x ) = .0. ) -> N = M ) )
29 1 4 grpinvf 
 |-  ( G e. Grp -> N : B --> B )
30 1 2 3 4 grplinv 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( N ` x ) .+ x ) = .0. )
31 30 ralrimiva 
 |-  ( G e. Grp -> A. x e. B ( ( N ` x ) .+ x ) = .0. )
32 29 31 jca 
 |-  ( G e. Grp -> ( N : B --> B /\ A. x e. B ( ( N ` x ) .+ x ) = .0. ) )
33 feq1 
 |-  ( N = M -> ( N : B --> B <-> M : B --> B ) )
34 fveq1 
 |-  ( N = M -> ( N ` x ) = ( M ` x ) )
35 34 oveq1d 
 |-  ( N = M -> ( ( N ` x ) .+ x ) = ( ( M ` x ) .+ x ) )
36 35 eqeq1d 
 |-  ( N = M -> ( ( ( N ` x ) .+ x ) = .0. <-> ( ( M ` x ) .+ x ) = .0. ) )
37 36 ralbidv 
 |-  ( N = M -> ( A. x e. B ( ( N ` x ) .+ x ) = .0. <-> A. x e. B ( ( M ` x ) .+ x ) = .0. ) )
38 33 37 anbi12d 
 |-  ( N = M -> ( ( N : B --> B /\ A. x e. B ( ( N ` x ) .+ x ) = .0. ) <-> ( M : B --> B /\ A. x e. B ( ( M ` x ) .+ x ) = .0. ) ) )
39 32 38 syl5ibcom 
 |-  ( G e. Grp -> ( N = M -> ( M : B --> B /\ A. x e. B ( ( M ` x ) .+ x ) = .0. ) ) )
40 28 39 impbid 
 |-  ( G e. Grp -> ( ( M : B --> B /\ A. x e. B ( ( M ` x ) .+ x ) = .0. ) <-> N = M ) )