Theorem mndractf1o 33026

Description: An element 𝑋 of a monoid 𝐸 is invertible iff its right-translation 𝐺 is bijective. See also mndlactf1o 33025. 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 7413	. . . . . 6 ⊢ (𝑣 = (◡𝐺‘ 0 ) → (𝑋 + 𝑣) = (𝑋 + (◡𝐺‘ 0 )))
2	1	eqeq1d 2737	. . . . 5 ⊢ (𝑣 = (◡𝐺‘ 0 ) → ((𝑋 + 𝑣) = 0 ↔ (𝑋 + (◡𝐺‘ 0 )) = 0 ))
3		f1ocnv 6830	. . . . . . . 8 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → ◡𝐺:𝐵–1-1-onto→𝐵)
4		f1of 6818	. . . . . . . 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 18727	. . . . . . . 8 ⊢ (𝐸 ∈ Mnd → 0 ∈ 𝐵)
11	7, 10	syl 17	. . . . . . 7 ⊢ (𝜑 → 0 ∈ 𝐵)
12	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 0 ∈ 𝐵)
13	6, 12	ffvelcdmd 7075	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (◡𝐺‘ 0 ) ∈ 𝐵)
14		f1of1 6817	. . . . . . 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 33017	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + (◡𝐺‘ 0 )) ∈ 𝐵)
21	20, 12	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) ∈ 𝐵 ∧ 0 ∈ 𝐵))
22	8, 16, 9	mndlid 18732	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
23	17, 19, 22	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ( 0 + 𝑋) = 𝑋)
24		mndractf1o.f	. . . . . . . 8 ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋))
25		oveq1 7412	. . . . . . . 8 ⊢ (𝑎 = 0 → (𝑎 + 𝑋) = ( 0 + 𝑋))
26		ovexd 7440	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ( 0 + 𝑋) ∈ V)
27	24, 25, 12, 26	fvmptd3 7009	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘ 0 ) = ( 0 + 𝑋))
28		oveq1 7412	. . . . . . . . 9 ⊢ (𝑎 = (𝑋 + (◡𝐺‘ 0 )) → (𝑎 + 𝑋) = ((𝑋 + (◡𝐺‘ 0 )) + 𝑋))
29		ovexd 7440	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) + 𝑋) ∈ V)
30	24, 28, 20, 29	fvmptd3 7009	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = ((𝑋 + (◡𝐺‘ 0 )) + 𝑋))
31	8, 16, 17, 19, 13, 19	mndassd 33018	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) + 𝑋) = (𝑋 + ((◡𝐺‘ 0 ) + 𝑋)))
32		oveq1 7412	. . . . . . . . . . . 12 ⊢ (𝑎 = (◡𝐺‘ 0 ) → (𝑎 + 𝑋) = ((◡𝐺‘ 0 ) + 𝑋))
33		ovexd 7440	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((◡𝐺‘ 0 ) + 𝑋) ∈ V)
34	24, 32, 13, 33	fvmptd3 7009	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(◡𝐺‘ 0 )) = ((◡𝐺‘ 0 ) + 𝑋))
35		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝐺:𝐵–1-1-onto→𝐵)
36		f1ocnvfv2 7270	. . . . . . . . . . . 12 ⊢ ((𝐺:𝐵–1-1-onto→𝐵 ∧ 0 ∈ 𝐵) → (𝐺‘(◡𝐺‘ 0 )) = 0 )
37	35, 12, 36	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(◡𝐺‘ 0 )) = 0 )
38	34, 37	eqtr3d 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((◡𝐺‘ 0 ) + 𝑋) = 0 )
39	38	oveq2d 7421	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + ((◡𝐺‘ 0 ) + 𝑋)) = (𝑋 + 0 ))
40	8, 16, 9	mndrid 18733	. . . . . . . . . 10 ⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)
41	17, 19, 40	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + 0 ) = 𝑋)
42	31, 39, 41	3eqtrd 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) + 𝑋) = 𝑋)
43	30, 42	eqtrd 2770	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = 𝑋)
44	23, 27, 43	3eqtr4rd 2781	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = (𝐺‘ 0 ))
45		f1fveq 7255	. . . . . . 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 837	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + (◡𝐺‘ 0 )) = 0 )
48	2, 13, 47	rspcedvdw 3604	. . . 4 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 )
49		f1ofo 6825	. . . . 5 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → 𝐺:𝐵–onto→𝐵)
50	8, 9, 16, 24, 7, 18	mndractfo 33024	. . . . . 6 ⊢ (𝜑 → (𝐺:𝐵–onto→𝐵 ↔ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ))
51	50	biimpa 476	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–onto→𝐵) → ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )
52	49, 51	sylan2 593	. . . 4 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )
53	48, 52	jca 511	. . 3 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ))
54	7	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐸 ∈ Mnd)
55	18	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝑋 ∈ 𝐵)
56		simplr 768	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝑣 ∈ 𝐵)
57		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → (𝑋 + 𝑣) = 0 )
58	8, 9, 16, 24, 54, 55, 56, 57	mndractf1 33023	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵–1-1→𝐵)
59	58	r19.29an 3144	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵–1-1→𝐵)
60	50	biimpar 477	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ) → 𝐺:𝐵–onto→𝐵)
61	59, 60	anim12dan 619	. . . 4 ⊢ ((𝜑 ∧ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )) → (𝐺:𝐵–1-1→𝐵 ∧ 𝐺:𝐵–onto→𝐵))
62		df-f1o 6538	. . . 4 ⊢ (𝐺:𝐵–1-1-onto→𝐵 ↔ (𝐺:𝐵–1-1→𝐵 ∧ 𝐺:𝐵–onto→𝐵))
63	61, 62	sylibr 234	. . 3 ⊢ ((𝜑 ∧ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )) → 𝐺:𝐵–1-1-onto→𝐵)
64	53, 63	impbida 800	. 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐵 ↔ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )))
65	8, 9, 16, 7, 18	mndlrinvb 33020	. 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 1540   ∈ wcel 2108  ∃wrex 3060  Vcvv 3459   ↦ cmpt 5201  ^◡ccnv 5653  ⟶wf 6527  –1-1→wf1 6528  –onto→wfo 6529  –1-1-onto→wf1o 6530  ‘cfv 6531  (class class class)co 7405  Basecbs 17228  +_gcplusg 17271  0_gc0g 17453  Mndcmnd 18712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7362  df-ov 7408  df-0g 17455  df-mgm 18618  df-sgrp 18697  df-mnd 18713

This theorem is referenced by: (None)