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 ⊢ 𝐵 = ( Base ‘ 𝐸 )
mndractf1o.z ⊢ 0 = ( 0g ‘ 𝐸 )
mndractf1o.p ⊢ + = ( +g ‘ 𝐸 )
mndractf1o.f ⊢ 𝐺 = ( 𝑎 ∈ 𝐵 ↦ ( 𝑎 + 𝑋 ) )
mndractf1o.e ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
mndractf1o.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion mndractf1o ( 𝜑 → ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 mndractf1o.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
2 mndractf1o.z ⊢ 0 = ( 0g ‘ 𝐸 )
3 mndractf1o.p ⊢ + = ( +g ‘ 𝐸 )
4 mndractf1o.f ⊢ 𝐺 = ( 𝑎 ∈ 𝐵 ↦ ( 𝑎 + 𝑋 ) )
5 mndractf1o.e ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
6 mndractf1o.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 oveq2 ⊢ ( 𝑣 = ( ◡ 𝐺 ‘ 0 ) → ( 𝑋 + 𝑣 ) = ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) )
8 7 eqeq1d ⊢ ( 𝑣 = ( ◡ 𝐺 ‘ 0 ) → ( ( 𝑋 + 𝑣 ) = 0 ↔ ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) = 0 ) )
9 f1ocnv ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐵 –1-1-onto→ 𝐵 )
10 f1of ⊢ ( ◡ 𝐺 : 𝐵 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐵 ⟶ 𝐵 )
11 9 10 syl ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐵 ⟶ 𝐵 )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ◡ 𝐺 : 𝐵 ⟶ 𝐵 )
13 1 2 mndidcl ⊢ ( 𝐸 ∈ Mnd → 0 ∈ 𝐵 )
14 5 13 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → 0 ∈ 𝐵 )
16 12 15 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( ◡ 𝐺 ‘ 0 ) ∈ 𝐵 )
17 f1of1 ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 → 𝐺 : 𝐵 –1-1→ 𝐵 )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → 𝐺 : 𝐵 –1-1→ 𝐵 )
19 5 adantr ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → 𝐸 ∈ Mnd )
20 6 adantr ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → 𝑋 ∈ 𝐵 )
21 1 3 19 20 16 mndcld ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) ∈ 𝐵 )
22 21 15 jca ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) ∈ 𝐵 ∧ 0 ∈ 𝐵 ) )
23 1 3 2 mndlid ⊢ ( ( 𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( 0 + 𝑋 ) = 𝑋 )
24 19 20 23 syl2anc ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( 0 + 𝑋 ) = 𝑋 )
25 oveq1 ⊢ ( 𝑎 = 0 → ( 𝑎 + 𝑋 ) = ( 0 + 𝑋 ) )
26 ovexd ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( 0 + 𝑋 ) ∈ V )
27 4 25 15 26 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝐺 ‘ 0 ) = ( 0 + 𝑋 ) )
28 oveq1 ⊢ ( 𝑎 = ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) → ( 𝑎 + 𝑋 ) = ( ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) + 𝑋 ) )
29 ovexd ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) + 𝑋 ) ∈ V )
30 4 28 21 29 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝐺 ‘ ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) ) = ( ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) + 𝑋 ) )
31 1 3 19 20 16 20 mndassd ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) + 𝑋 ) = ( 𝑋 + ( ( ◡ 𝐺 ‘ 0 ) + 𝑋 ) ) )
32 oveq1 ⊢ ( 𝑎 = ( ◡ 𝐺 ‘ 0 ) → ( 𝑎 + 𝑋 ) = ( ( ◡ 𝐺 ‘ 0 ) + 𝑋 ) )
33 ovexd ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( ( ◡ 𝐺 ‘ 0 ) + 𝑋 ) ∈ V )
34 4 32 16 33 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 0 ) ) = ( ( ◡ 𝐺 ‘ 0 ) + 𝑋 ) )
35 simpr ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → 𝐺 : 𝐵 –1-1-onto→ 𝐵 )
36 f1ocnvfv2 ⊢ ( ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 ∧ 0 ∈ 𝐵 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 0 ) ) = 0 )
37 35 15 36 syl2anc ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 0 ) ) = 0 )
38 34 37 eqtr3d ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( ( ◡ 𝐺 ‘ 0 ) + 𝑋 ) = 0 )
39 38 oveq2d ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝑋 + ( ( ◡ 𝐺 ‘ 0 ) + 𝑋 ) ) = ( 𝑋 + 0 ) )
40 1 3 2 mndrid ⊢ ( ( 𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + 0 ) = 𝑋 )
41 19 20 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝑋 + 0 ) = 𝑋 )
42 31 39 41 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) + 𝑋 ) = 𝑋 )
43 30 42 eqtrd ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝐺 ‘ ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) ) = 𝑋 )
44 24 27 43 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝐺 ‘ ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) ) = ( 𝐺 ‘ 0 ) )
45 f1fveq ⊢ ( ( 𝐺 : 𝐵 –1-1→ 𝐵 ∧ ( ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) ∈ 𝐵 ∧ 0 ∈ 𝐵 ) ) → ( ( 𝐺 ‘ ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) ) = ( 𝐺 ‘ 0 ) ↔ ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) = 0 ) )
46 45 biimpa ⊢ ( ( ( 𝐺 : 𝐵 –1-1→ 𝐵 ∧ ( ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) ∈ 𝐵 ∧ 0 ∈ 𝐵 ) ) ∧ ( 𝐺 ‘ ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) ) = ( 𝐺 ‘ 0 ) ) → ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) = 0 )
47 18 22 44 46 syl21anc ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( 𝑋 + ( ◡ 𝐺 ‘ 0 ) ) = 0 )
48 8 16 47 rspcedvdw ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ∃ 𝑣 ∈ 𝐵 ( 𝑋 + 𝑣 ) = 0 )
49 f1ofo ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 → 𝐺 : 𝐵 –onto→ 𝐵 )
50 1 2 3 4 5 6 mndractfo ⊢ ( 𝜑 → ( 𝐺 : 𝐵 –onto→ 𝐵 ↔ ∃ 𝑤 ∈ 𝐵 ( 𝑤 + 𝑋 ) = 0 ) )
51 50 biimpa ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) → ∃ 𝑤 ∈ 𝐵 ( 𝑤 + 𝑋 ) = 0 )
52 49 51 sylan2 ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ∃ 𝑤 ∈ 𝐵 ( 𝑤 + 𝑋 ) = 0 )
53 48 52 jca ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) → ( ∃ 𝑣 ∈ 𝐵 ( 𝑋 + 𝑣 ) = 0 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑤 + 𝑋 ) = 0 ) )
54 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑣 ) = 0 ) → 𝐸 ∈ Mnd )
55 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑣 ) = 0 ) → 𝑋 ∈ 𝐵 )
56 simplr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑣 ) = 0 ) → 𝑣 ∈ 𝐵 )
57 simpr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑣 ) = 0 ) → ( 𝑋 + 𝑣 ) = 0 )
58 1 2 3 4 54 55 56 57 mndractf1 ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑣 ) = 0 ) → 𝐺 : 𝐵 –1-1→ 𝐵 )
59 58 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑋 + 𝑣 ) = 0 ) → 𝐺 : 𝐵 –1-1→ 𝐵 )
60 50 biimpar ⊢ ( ( 𝜑 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑤 + 𝑋 ) = 0 ) → 𝐺 : 𝐵 –onto→ 𝐵 )
61 59 60 anim12dan ⊢ ( ( 𝜑 ∧ ( ∃ 𝑣 ∈ 𝐵 ( 𝑋 + 𝑣 ) = 0 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑤 + 𝑋 ) = 0 ) ) → ( 𝐺 : 𝐵 –1-1→ 𝐵 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) )
62 df-f1o ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 ↔ ( 𝐺 : 𝐵 –1-1→ 𝐵 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) )
63 61 62 sylibr ⊢ ( ( 𝜑 ∧ ( ∃ 𝑣 ∈ 𝐵 ( 𝑋 + 𝑣 ) = 0 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑤 + 𝑋 ) = 0 ) ) → 𝐺 : 𝐵 –1-1-onto→ 𝐵 )
64 53 63 impbida ⊢ ( 𝜑 → ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 ↔ ( ∃ 𝑣 ∈ 𝐵 ( 𝑋 + 𝑣 ) = 0 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑤 + 𝑋 ) = 0 ) ) )
65 1 2 3 5 6 mndlrinvb ⊢ ( 𝜑 → ( ( ∃ 𝑣 ∈ 𝐵 ( 𝑋 + 𝑣 ) = 0 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑤 + 𝑋 ) = 0 ) ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) )
66 64 65 bitrd ⊢ ( 𝜑 → ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) )