Theorem mndractf1o 33017

Description: An element 𝑋 of a monoid 𝐸 is invertible iff its right-translation 𝐺 is bijective. See also mndlactf1o 33016. 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 7456	. . . . . 6 ⊢ (𝑣 = (◡𝐺‘ 0 ) → (𝑋 + 𝑣) = (𝑋 + (◡𝐺‘ 0 )))
2	1	eqeq1d 2742	. . . . 5 ⊢ (𝑣 = (◡𝐺‘ 0 ) → ((𝑋 + 𝑣) = 0 ↔ (𝑋 + (◡𝐺‘ 0 )) = 0 ))
3		f1ocnv 6874	. . . . . . . 8 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → ◡𝐺:𝐵–1-1-onto→𝐵)
4		f1of 6862	. . . . . . . 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 18787	. . . . . . . 8 ⊢ (𝐸 ∈ Mnd → 0 ∈ 𝐵)
11	7, 10	syl 17	. . . . . . 7 ⊢ (𝜑 → 0 ∈ 𝐵)
12	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 0 ∈ 𝐵)
13	6, 12	ffvelcdmd 7119	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (◡𝐺‘ 0 ) ∈ 𝐵)
14		f1of1 6861	. . . . . . 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 33008	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + (◡𝐺‘ 0 )) ∈ 𝐵)
21	20, 12	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) ∈ 𝐵 ∧ 0 ∈ 𝐵))
22	8, 16, 9	mndlid 18792	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
23	17, 19, 22	syl2anc 583	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ( 0 + 𝑋) = 𝑋)
24		mndractf1o.f	. . . . . . . 8 ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋))
25		oveq1 7455	. . . . . . . 8 ⊢ (𝑎 = 0 → (𝑎 + 𝑋) = ( 0 + 𝑋))
26		ovexd 7483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ( 0 + 𝑋) ∈ V)
27	24, 25, 12, 26	fvmptd3 7052	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘ 0 ) = ( 0 + 𝑋))
28		oveq1 7455	. . . . . . . . 9 ⊢ (𝑎 = (𝑋 + (◡𝐺‘ 0 )) → (𝑎 + 𝑋) = ((𝑋 + (◡𝐺‘ 0 )) + 𝑋))
29		ovexd 7483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) + 𝑋) ∈ V)
30	24, 28, 20, 29	fvmptd3 7052	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = ((𝑋 + (◡𝐺‘ 0 )) + 𝑋))
31	8, 16, 17, 19, 13, 19	mndassd 33009	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) + 𝑋) = (𝑋 + ((◡𝐺‘ 0 ) + 𝑋)))
32		oveq1 7455	. . . . . . . . . . . 12 ⊢ (𝑎 = (◡𝐺‘ 0 ) → (𝑎 + 𝑋) = ((◡𝐺‘ 0 ) + 𝑋))
33		ovexd 7483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((◡𝐺‘ 0 ) + 𝑋) ∈ V)
34	24, 32, 13, 33	fvmptd3 7052	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(◡𝐺‘ 0 )) = ((◡𝐺‘ 0 ) + 𝑋))
35		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝐺:𝐵–1-1-onto→𝐵)
36		f1ocnvfv2 7313	. . . . . . . . . . . 12 ⊢ ((𝐺:𝐵–1-1-onto→𝐵 ∧ 0 ∈ 𝐵) → (𝐺‘(◡𝐺‘ 0 )) = 0 )
37	35, 12, 36	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(◡𝐺‘ 0 )) = 0 )
38	34, 37	eqtr3d 2782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((◡𝐺‘ 0 ) + 𝑋) = 0 )
39	38	oveq2d 7464	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + ((◡𝐺‘ 0 ) + 𝑋)) = (𝑋 + 0 ))
40	8, 16, 9	mndrid 18793	. . . . . . . . . 10 ⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)
41	17, 19, 40	syl2anc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + 0 ) = 𝑋)
42	31, 39, 41	3eqtrd 2784	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (◡𝐺‘ 0 )) + 𝑋) = 𝑋)
43	30, 42	eqtrd 2780	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = 𝑋)
44	23, 27, 43	3eqtr4rd 2791	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (◡𝐺‘ 0 ))) = (𝐺‘ 0 ))
45		f1fveq 7299	. . . . . . 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 3638	. . . 4 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 )
49		f1ofo 6869	. . . . 5 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → 𝐺:𝐵–onto→𝐵)
50	8, 9, 16, 24, 7, 18	mndractfo 33015	. . . . . 6 ⊢ (𝜑 → (𝐺:𝐵–onto→𝐵 ↔ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ))
51	50	biimpa 476	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–onto→𝐵) → ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )
52	49, 51	sylan2 592	. . . 4 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )
53	48, 52	jca 511	. . 3 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ))
54	7	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐸 ∈ Mnd)
55	18	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝑋 ∈ 𝐵)
56		simplr 768	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝑣 ∈ 𝐵)
57		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → (𝑋 + 𝑣) = 0 )
58	8, 9, 16, 24, 54, 55, 56, 57	mndractf1 33014	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵–1-1→𝐵)
59	58	r19.29an 3164	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵–1-1→𝐵)
60	50	biimpar 477	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ) → 𝐺:𝐵–onto→𝐵)
61	59, 60	anim12dan 618	. . . 4 ⊢ ((𝜑 ∧ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )) → (𝐺:𝐵–1-1→𝐵 ∧ 𝐺:𝐵–onto→𝐵))
62		df-f1o 6580	. . . 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 33011	. 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 1537   ∈ wcel 2108  ∃wrex 3076  Vcvv 3488   ↦ cmpt 5249  ^◡ccnv 5699  ⟶wf 6569  –1-1→wf1 6570  –onto→wfo 6571  –1-1-onto→wf1o 6572  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  +_gcplusg 17311  0_gc0g 17499  Mndcmnd 18772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-0g 17501  df-mgm 18678  df-sgrp 18757  df-mnd 18773

This theorem is referenced by: (None)