Theorem mndractf1o 33382

Description: An element 𝑋 of a monoid 𝐸 is invertible iff its right-translation 𝐺 is bijective. See also mndlactf1o 33381. 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 7431	. . . . . 6 ⊢ (𝑣 = (◡𝐺‘ 0 ) → (𝑋 + 𝑣) = (𝑋 + (◡𝐺‘ 0 )))
2	1	eqeq1d 2768	. . . . 5 ⊢ (𝑣 = (◡𝐺‘ 0 ) → ((𝑋 + 𝑣) = 0 ↔ (𝑋 + (◡𝐺‘ 0 )) = 0 ))
3		f1ocnv 6840	. . . . . . . 8 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → ◡𝐺:𝐵–1-1-onto→𝐵)
4		f1of 6827	. . . . . . . 8 ⊢ (◡𝐺:𝐵–1-1-onto→𝐵 → ◡𝐺:𝐵⟶𝐵)
5	3, 4	syl 18	. . . . . . 7 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → ◡𝐺:𝐵⟶𝐵)
6	5	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ◡𝐺:𝐵⟶𝐵)
7		mndractf1o.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Mnd)
8		mndractf1o.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐸)
9		mndractf1o.z	. . . . . . . . 9 ⊢ 0 = (0g‘𝐸)
10	8, 9	mndidcl 18836	. . . . . . . 8 ⊢ (𝐸 ∈ Mnd → 0 ∈ 𝐵)
11	7, 10	syl 18	. . . . . . 7 ⊢ (𝜑 → 0 ∈ 𝐵)
12	11	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 0 ∈ 𝐵)
13	6, 12	ffvelcdmd 7087	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (◡𝐺‘ 0 ) ∈ 𝐵)
14		f1of1 6826	. . . . . . 7 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → 𝐺:𝐵–1-1→𝐵)
15	14	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝐺:𝐵–1-1→𝐵)
16		mndractf1o.p	. . . . . . . 8 ⊢ + = (+g‘𝐸)
17	7	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝐸 ∈ Mnd)
18		mndractf1o.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
19	18	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝑋 ∈ 𝐵)
20	8, 16, 17, 19, 13	mndcld 33373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + (◡𝐺‘ 0 )) ∈ 𝐵)
21	20, 12	jca 521	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) ∈ 𝐵 ∧ 0 ∈ 𝐵))
22	8, 16, 9	mndlid 18841	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
23	17, 19, 22	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ( 0 + 𝑋) = 𝑋)
24		mndractf1o.f	. . . . . . . 8 ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋))
25		oveq1 7430	. . . . . . . 8 ⊢ (𝑎 = 0 → (𝑎 + 𝑋) = ( 0 + 𝑋))
26		ovexd 7458	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ( 0 + 𝑋) ∈ V)
27	24, 25, 12, 26	fvmptd3 7020	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘ 0 ) = ( 0 + 𝑋))
28		oveq1 7430	. . . . . . . . 9 ⊢ (𝑎 = (𝑋 + (◡𝐺‘ 0 )) → (𝑎 + 𝑋) = ((𝑋 + (◡𝐺‘ 0 )) + 𝑋))
29		ovexd 7458	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) + 𝑋) ∈ V)
30	24, 28, 20, 29	fvmptd3 7020	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = ((𝑋 + (◡𝐺‘ 0 )) + 𝑋))
31	8, 16, 17, 19, 13, 19	mndassd 33374	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) + 𝑋) = (𝑋 + ((◡𝐺‘ 0 ) + 𝑋)))
32		oveq1 7430	. . . . . . . . . . . 12 ⊢ (𝑎 = (◡𝐺‘ 0 ) → (𝑎 + 𝑋) = ((◡𝐺‘ 0 ) + 𝑋))
33		ovexd 7458	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((◡𝐺‘ 0 ) + 𝑋) ∈ V)
34	24, 32, 13, 33	fvmptd3 7020	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(◡𝐺‘ 0 )) = ((◡𝐺‘ 0 ) + 𝑋))
35		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝐺:𝐵–1-1-onto→𝐵)
36		f1ocnvfv2 7286	. . . . . . . . . . . 12 ⊢ ((𝐺:𝐵–1-1-onto→𝐵 ∧ 0 ∈ 𝐵) → (𝐺‘(◡𝐺‘ 0 )) = 0 )
37	35, 12, 36	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(◡𝐺‘ 0 )) = 0 )
38	34, 37	eqtr3d 2803	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((◡𝐺‘ 0 ) + 𝑋) = 0 )
39	38	oveq2d 7439	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + ((◡𝐺‘ 0 ) + 𝑋)) = (𝑋 + 0 ))
40	8, 16, 9	mndrid 18842	. . . . . . . . . 10 ⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)
41	17, 19, 40	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + 0 ) = 𝑋)
42	31, 39, 41	3eqtrd 2805	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) + 𝑋) = 𝑋)
43	30, 42	eqtrd 2801	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = 𝑋)
44	23, 27, 43	3eqtr4rd 2812	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = (𝐺‘ 0 ))
45		f1fveq 7267	. . . . . . 7 ⊢ ((𝐺:𝐵–1-1→𝐵 ∧ ((𝑋 + (◡𝐺‘ 0 )) ∈ 𝐵 ∧ 0 ∈ 𝐵)) → ((𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = (𝐺‘ 0 ) ↔ (𝑋 + (◡𝐺‘ 0 )) = 0 ))
46	45	biimpa 482	. . . . . 6 ⊢ (((𝐺:𝐵–1-1→𝐵 ∧ ((𝑋 + (◡𝐺‘ 0 )) ∈ 𝐵 ∧ 0 ∈ 𝐵)) ∧ (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = (𝐺‘ 0 )) → (𝑋 + (◡𝐺‘ 0 )) = 0 )
47	15, 21, 44, 46	syl21anc 851	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + (◡𝐺‘ 0 )) = 0 )
48	2, 13, 47	rspcedvdw 3587	. . . 4 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 )
49		f1ofo 6835	. . . . 5 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → 𝐺:𝐵–onto→𝐵)
50	8, 9, 16, 24, 7, 18	mndractfo 33380	. . . . . 6 ⊢ (𝜑 → (𝐺:𝐵–onto→𝐵 ↔ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ))
51	50	biimpa 482	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–onto→𝐵) → ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )
52	49, 51	sylan2 605	. . . 4 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )
53	48, 52	jca 521	. . 3 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ))
54	7	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐸 ∈ Mnd)
55	18	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝑋 ∈ 𝐵)
56		simplr 781	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝑣 ∈ 𝐵)
57		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → (𝑋 + 𝑣) = 0 )
58	8, 9, 16, 24, 54, 55, 56, 57	mndractf1 33379	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵–1-1→𝐵)
59	58	r19.29an 3172	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵–1-1→𝐵)
60	50	biimpar 483	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ) → 𝐺:𝐵–onto→𝐵)
61	59, 60	anim12dan 631	. . . 4 ⊢ ((𝜑 ∧ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )) → (𝐺:𝐵–1-1→𝐵 ∧ 𝐺:𝐵–onto→𝐵))
62		df-f1o 6550	. . . 4 ⊢ (𝐺:𝐵–1-1-onto→𝐵 ↔ (𝐺:𝐵–1-1→𝐵 ∧ 𝐺:𝐵–onto→𝐵))
63	61, 62	sylibr 237	. . 3 ⊢ ((𝜑 ∧ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )) → 𝐺:𝐵–1-1-onto→𝐵)
64	53, 63	impbida 813	. 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐵 ↔ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )))
65	8, 9, 16, 7, 18	mndlrinvb 33376	. 2 ⊢ (𝜑 → ((∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ) ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))
66	64, 65	bitrd 282	1 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∃wrex 3092  Vcvv 3458   ↦ cmpt 5197  ^◡ccnv 5665  ⟶wf 6539  –1-1→wf1 6540  –onto→wfo 6541  –1-1-onto→wf1o 6542  ‘cfv 6543  (class class class)co 7423  Basecbs 17294  +_gcplusg 17335  0_gc0g 17517  Mndcmnd 18821

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-0g 17519  df-mgm 18723  df-sgrp 18806  df-mnd 18822

This theorem is used by: (None)