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

Metamath Proof Explorer

Theorem mndractf1o

Description: An element X of a monoid E is invertible iff its right-translation G is bijective. See also mndlactf1o . Remark in chapter I. of BourbakiAlg1 p. 17 . (Contributed by Thierry Arnoux, 3-Aug-2025)

Ref Expression
Hypotheses mndractf1o.b 
|- B = ( Base ` E )
mndractf1o.z 
|- .0. = ( 0g ` E )
mndractf1o.p 
|- .+ = ( +g ` E )
mndractf1o.f 
|- G = ( a e. B |-> ( a .+ X ) )
mndractf1o.e 
|- ( ph -> E e. Mnd )
mndractf1o.x 
|- ( ph -> X e. B )
Assertion mndractf1o 
|- ( ph -> ( G : B -1-1-onto-> B <-> E. y e. B ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) )

Proof

Step Hyp Ref Expression
1 mndractf1o.b 
 |-  B = ( Base ` E )
2 mndractf1o.z 
 |-  .0. = ( 0g ` E )
3 mndractf1o.p 
 |-  .+ = ( +g ` E )
4 mndractf1o.f 
 |-  G = ( a e. B |-> ( a .+ X ) )
5 mndractf1o.e 
 |-  ( ph -> E e. Mnd )
6 mndractf1o.x 
 |-  ( ph -> X e. B )
7 oveq2 
 |-  ( v = ( `' G ` .0. ) -> ( X .+ v ) = ( X .+ ( `' G ` .0. ) ) )
8 7 eqeq1d 
 |-  ( v = ( `' G ` .0. ) -> ( ( X .+ v ) = .0. <-> ( X .+ ( `' G ` .0. ) ) = .0. ) )
9 f1ocnv 
 |-  ( G : B -1-1-onto-> B -> `' G : B -1-1-onto-> B )
10 f1of 
 |-  ( `' G : B -1-1-onto-> B -> `' G : B --> B )
11 9 10 syl 
 |-  ( G : B -1-1-onto-> B -> `' G : B --> B )
12 11 adantl 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> `' G : B --> B )
13 1 2 mndidcl 
 |-  ( E e. Mnd -> .0. e. B )
14 5 13 syl 
 |-  ( ph -> .0. e. B )
15 14 adantr 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> .0. e. B )
16 12 15 ffvelcdmd 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( `' G ` .0. ) e. B )
17 f1of1 
 |-  ( G : B -1-1-onto-> B -> G : B -1-1-> B )
18 17 adantl 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> G : B -1-1-> B )
19 5 adantr 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> E e. Mnd )
20 6 adantr 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> X e. B )
21 1 3 19 20 16 mndcld 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( X .+ ( `' G ` .0. ) ) e. B )
22 21 15 jca 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( ( X .+ ( `' G ` .0. ) ) e. B /\ .0. e. B ) )
23 1 3 2 mndlid 
 |-  ( ( E e. Mnd /\ X e. B ) -> ( .0. .+ X ) = X )
24 19 20 23 syl2anc 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( .0. .+ X ) = X )
25 oveq1 
 |-  ( a = .0. -> ( a .+ X ) = ( .0. .+ X ) )
26 ovexd 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( .0. .+ X ) e. _V )
27 4 25 15 26 fvmptd3 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( G ` .0. ) = ( .0. .+ X ) )
28 oveq1 
 |-  ( a = ( X .+ ( `' G ` .0. ) ) -> ( a .+ X ) = ( ( X .+ ( `' G ` .0. ) ) .+ X ) )
29 ovexd 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( ( X .+ ( `' G ` .0. ) ) .+ X ) e. _V )
30 4 28 21 29 fvmptd3 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( G ` ( X .+ ( `' G ` .0. ) ) ) = ( ( X .+ ( `' G ` .0. ) ) .+ X ) )
31 1 3 19 20 16 20 mndassd 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( ( X .+ ( `' G ` .0. ) ) .+ X ) = ( X .+ ( ( `' G ` .0. ) .+ X ) ) )
32 oveq1 
 |-  ( a = ( `' G ` .0. ) -> ( a .+ X ) = ( ( `' G ` .0. ) .+ X ) )
33 ovexd 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( ( `' G ` .0. ) .+ X ) e. _V )
34 4 32 16 33 fvmptd3 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( G ` ( `' G ` .0. ) ) = ( ( `' G ` .0. ) .+ X ) )
35 simpr 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> G : B -1-1-onto-> B )
36 f1ocnvfv2 
 |-  ( ( G : B -1-1-onto-> B /\ .0. e. B ) -> ( G ` ( `' G ` .0. ) ) = .0. )
37 35 15 36 syl2anc 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( G ` ( `' G ` .0. ) ) = .0. )
38 34 37 eqtr3d 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( ( `' G ` .0. ) .+ X ) = .0. )
39 38 oveq2d 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( X .+ ( ( `' G ` .0. ) .+ X ) ) = ( X .+ .0. ) )
40 1 3 2 mndrid 
 |-  ( ( E e. Mnd /\ X e. B ) -> ( X .+ .0. ) = X )
41 19 20 40 syl2anc 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( X .+ .0. ) = X )
42 31 39 41 3eqtrd 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( ( X .+ ( `' G ` .0. ) ) .+ X ) = X )
43 30 42 eqtrd 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( G ` ( X .+ ( `' G ` .0. ) ) ) = X )
44 24 27 43 3eqtr4rd 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( G ` ( X .+ ( `' G ` .0. ) ) ) = ( G ` .0. ) )
45 f1fveq 
 |-  ( ( G : B -1-1-> B /\ ( ( X .+ ( `' G ` .0. ) ) e. B /\ .0. e. B ) ) -> ( ( G ` ( X .+ ( `' G ` .0. ) ) ) = ( G ` .0. ) <-> ( X .+ ( `' G ` .0. ) ) = .0. ) )
46 45 biimpa 
 |-  ( ( ( G : B -1-1-> B /\ ( ( X .+ ( `' G ` .0. ) ) e. B /\ .0. e. B ) ) /\ ( G ` ( X .+ ( `' G ` .0. ) ) ) = ( G ` .0. ) ) -> ( X .+ ( `' G ` .0. ) ) = .0. )
47 18 22 44 46 syl21anc 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( X .+ ( `' G ` .0. ) ) = .0. )
48 8 16 47 rspcedvdw 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> E. v e. B ( X .+ v ) = .0. )
49 f1ofo 
 |-  ( G : B -1-1-onto-> B -> G : B -onto-> B )
50 1 2 3 4 5 6 mndractfo 
 |-  ( ph -> ( G : B -onto-> B <-> E. w e. B ( w .+ X ) = .0. ) )
51 50 biimpa 
 |-  ( ( ph /\ G : B -onto-> B ) -> E. w e. B ( w .+ X ) = .0. )
52 49 51 sylan2 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> E. w e. B ( w .+ X ) = .0. )
53 48 52 jca 
 |-  ( ( ph /\ G : B -1-1-onto-> B ) -> ( E. v e. B ( X .+ v ) = .0. /\ E. w e. B ( w .+ X ) = .0. ) )
54 5 ad2antrr 
 |-  ( ( ( ph /\ v e. B ) /\ ( X .+ v ) = .0. ) -> E e. Mnd )
55 6 ad2antrr 
 |-  ( ( ( ph /\ v e. B ) /\ ( X .+ v ) = .0. ) -> X e. B )
56 simplr 
 |-  ( ( ( ph /\ v e. B ) /\ ( X .+ v ) = .0. ) -> v e. B )
57 simpr 
 |-  ( ( ( ph /\ v e. B ) /\ ( X .+ v ) = .0. ) -> ( X .+ v ) = .0. )
58 1 2 3 4 54 55 56 57 mndractf1 
 |-  ( ( ( ph /\ v e. B ) /\ ( X .+ v ) = .0. ) -> G : B -1-1-> B )
59 58 r19.29an 
 |-  ( ( ph /\ E. v e. B ( X .+ v ) = .0. ) -> G : B -1-1-> B )
60 50 biimpar 
 |-  ( ( ph /\ E. w e. B ( w .+ X ) = .0. ) -> G : B -onto-> B )
61 59 60 anim12dan 
 |-  ( ( ph /\ ( E. v e. B ( X .+ v ) = .0. /\ E. w e. B ( w .+ X ) = .0. ) ) -> ( G : B -1-1-> B /\ G : B -onto-> B ) )
62 df-f1o 
 |-  ( G : B -1-1-onto-> B <-> ( G : B -1-1-> B /\ G : B -onto-> B ) )
63 61 62 sylibr 
 |-  ( ( ph /\ ( E. v e. B ( X .+ v ) = .0. /\ E. w e. B ( w .+ X ) = .0. ) ) -> G : B -1-1-onto-> B )
64 53 63 impbida 
 |-  ( ph -> ( G : B -1-1-onto-> B <-> ( E. v e. B ( X .+ v ) = .0. /\ E. w e. B ( w .+ X ) = .0. ) ) )
65 1 2 3 5 6 mndlrinvb 
 |-  ( ph -> ( ( E. v e. B ( X .+ v ) = .0. /\ E. w e. B ( w .+ X ) = .0. ) <-> E. y e. B ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) )
66 64 65 bitrd 
 |-  ( ph -> ( G : B -1-1-onto-> B <-> E. y e. B ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) )