Theorem mndractf1o 33123

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

Hypotheses

Ref	Expression
mndractf1o.b	⊢ 𝐵 = (Base‘𝐸)
mndractf1o.z	⊢ 0 = (0g‘𝐸)
mndractf1o.p	⊢ + = (+g‘𝐸)
mndractf1o.f	⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋))
mndractf1o.e	⊢ (𝜑 → 𝐸 ∈ Mnd)
mndractf1o.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)

Assertion

Ref	Expression
mndractf1o	⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))

Distinct variable groups:   + ,𝑎,𝑦   0 ,𝑎,𝑦   𝐵,𝑎,𝑦   𝐺,𝑎,𝑦   𝑋,𝑎,𝑦   𝜑,𝑎,𝑦

Allowed substitution hints:   𝐸(𝑦,𝑎)

Proof of Theorem mndractf1o

Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7376	. . . . . 6 ⊢ (𝑣 = (◡𝐺‘ 0 ) → (𝑋 + 𝑣) = (𝑋 + (◡𝐺‘ 0 )))
2	1	eqeq1d 2739	. . . . 5 ⊢ (𝑣 = (◡𝐺‘ 0 ) → ((𝑋 + 𝑣) = 0 ↔ (𝑋 + (◡𝐺‘ 0 )) = 0 ))
3		f1ocnv 6794	. . . . . . . 8 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → ◡𝐺:𝐵–1-1-onto→𝐵)
4		f1of 6782	. . . . . . . 8 ⊢ (◡𝐺:𝐵–1-1-onto→𝐵 → ◡𝐺:𝐵⟶𝐵)
5	3, 4	syl 17	. . . . . . 7 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → ◡𝐺:𝐵⟶𝐵)
6	5	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ◡𝐺:𝐵⟶𝐵)
7		mndractf1o.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Mnd)
8		mndractf1o.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐸)
9		mndractf1o.z	. . . . . . . . 9 ⊢ 0 = (0g‘𝐸)
10	8, 9	mndidcl 18686	. . . . . . . 8 ⊢ (𝐸 ∈ Mnd → 0 ∈ 𝐵)
11	7, 10	syl 17	. . . . . . 7 ⊢ (𝜑 → 0 ∈ 𝐵)
12	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 0 ∈ 𝐵)
13	6, 12	ffvelcdmd 7039	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (◡𝐺‘ 0 ) ∈ 𝐵)
14		f1of1 6781	. . . . . . 7 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → 𝐺:𝐵–1-1→𝐵)
15	14	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝐺:𝐵–1-1→𝐵)
16		mndractf1o.p	. . . . . . . 8 ⊢ + = (+g‘𝐸)
17	7	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝐸 ∈ Mnd)
18		mndractf1o.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
19	18	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝑋 ∈ 𝐵)
20	8, 16, 17, 19, 13	mndcld 33114	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + (◡𝐺‘ 0 )) ∈ 𝐵)
21	20, 12	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) ∈ 𝐵 ∧ 0 ∈ 𝐵))
22	8, 16, 9	mndlid 18691	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
23	17, 19, 22	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ( 0 + 𝑋) = 𝑋)
24		mndractf1o.f	. . . . . . . 8 ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋))
25		oveq1 7375	. . . . . . . 8 ⊢ (𝑎 = 0 → (𝑎 + 𝑋) = ( 0 + 𝑋))
26		ovexd 7403	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ( 0 + 𝑋) ∈ V)
27	24, 25, 12, 26	fvmptd3 6973	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘ 0 ) = ( 0 + 𝑋))
28		oveq1 7375	. . . . . . . . 9 ⊢ (𝑎 = (𝑋 + (◡𝐺‘ 0 )) → (𝑎 + 𝑋) = ((𝑋 + (◡𝐺‘ 0 )) + 𝑋))
29		ovexd 7403	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) + 𝑋) ∈ V)
30	24, 28, 20, 29	fvmptd3 6973	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = ((𝑋 + (◡𝐺‘ 0 )) + 𝑋))
31	8, 16, 17, 19, 13, 19	mndassd 33115	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) + 𝑋) = (𝑋 + ((◡𝐺‘ 0 ) + 𝑋)))
32		oveq1 7375	. . . . . . . . . . . 12 ⊢ (𝑎 = (◡𝐺‘ 0 ) → (𝑎 + 𝑋) = ((◡𝐺‘ 0 ) + 𝑋))
33		ovexd 7403	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((◡𝐺‘ 0 ) + 𝑋) ∈ V)
34	24, 32, 13, 33	fvmptd3 6973	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(◡𝐺‘ 0 )) = ((◡𝐺‘ 0 ) + 𝑋))
35		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝐺:𝐵–1-1-onto→𝐵)
36		f1ocnvfv2 7233	. . . . . . . . . . . 12 ⊢ ((𝐺:𝐵–1-1-onto→𝐵 ∧ 0 ∈ 𝐵) → (𝐺‘(◡𝐺‘ 0 )) = 0 )
37	35, 12, 36	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(◡𝐺‘ 0 )) = 0 )
38	34, 37	eqtr3d 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((◡𝐺‘ 0 ) + 𝑋) = 0 )
39	38	oveq2d 7384	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + ((◡𝐺‘ 0 ) + 𝑋)) = (𝑋 + 0 ))
40	8, 16, 9	mndrid 18692	. . . . . . . . . 10 ⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)
41	17, 19, 40	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + 0 ) = 𝑋)
42	31, 39, 41	3eqtrd 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) + 𝑋) = 𝑋)
43	30, 42	eqtrd 2772	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = 𝑋)
44	23, 27, 43	3eqtr4rd 2783	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = (𝐺‘ 0 ))
45		f1fveq 7218	. . . . . . 7 ⊢ ((𝐺:𝐵–1-1→𝐵 ∧ ((𝑋 + (◡𝐺‘ 0 )) ∈ 𝐵 ∧ 0 ∈ 𝐵)) → ((𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = (𝐺‘ 0 ) ↔ (𝑋 + (◡𝐺‘ 0 )) = 0 ))
46	45	biimpa 476	. . . . . 6 ⊢ (((𝐺:𝐵–1-1→𝐵 ∧ ((𝑋 + (◡𝐺‘ 0 )) ∈ 𝐵 ∧ 0 ∈ 𝐵)) ∧ (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = (𝐺‘ 0 )) → (𝑋 + (◡𝐺‘ 0 )) = 0 )
47	15, 21, 44, 46	syl21anc 838	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + (◡𝐺‘ 0 )) = 0 )
48	2, 13, 47	rspcedvdw 3581	. . . 4 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 )
49		f1ofo 6789	. . . . 5 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → 𝐺:𝐵–onto→𝐵)
50	8, 9, 16, 24, 7, 18	mndractfo 33121	. . . . . 6 ⊢ (𝜑 → (𝐺:𝐵–onto→𝐵 ↔ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ))
51	50	biimpa 476	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–onto→𝐵) → ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )
52	49, 51	sylan2 594	. . . 4 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )
53	48, 52	jca 511	. . 3 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ))
54	7	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐸 ∈ Mnd)
55	18	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝑋 ∈ 𝐵)
56		simplr 769	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝑣 ∈ 𝐵)
57		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → (𝑋 + 𝑣) = 0 )
58	8, 9, 16, 24, 54, 55, 56, 57	mndractf1 33120	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵–1-1→𝐵)
59	58	r19.29an 3142	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵–1-1→𝐵)
60	50	biimpar 477	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ) → 𝐺:𝐵–onto→𝐵)
61	59, 60	anim12dan 620	. . . 4 ⊢ ((𝜑 ∧ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )) → (𝐺:𝐵–1-1→𝐵 ∧ 𝐺:𝐵–onto→𝐵))
62		df-f1o 6507	. . . 4 ⊢ (𝐺:𝐵–1-1-onto→𝐵 ↔ (𝐺:𝐵–1-1→𝐵 ∧ 𝐺:𝐵–onto→𝐵))
63	61, 62	sylibr 234	. . 3 ⊢ ((𝜑 ∧ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )) → 𝐺:𝐵–1-1-onto→𝐵)
64	53, 63	impbida 801	. 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐵 ↔ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )))
65	8, 9, 16, 7, 18	mndlrinvb 33117	. 2 ⊢ (𝜑 → ((∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ) ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))
66	64, 65	bitrd 279	1 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  Vcvv 3442   ↦ cmpt 5181  ^◡ccnv 5631  ⟶wf 6496  –1-1→wf1 6497  –onto→wfo 6498  –1-1-onto→wf1o 6499  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  0_gc0g 17371  Mndcmnd 18671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-0g 17373  df-mgm 18577  df-sgrp 18656  df-mnd 18672

This theorem is referenced by: (None)