Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mndractf1o Structured version   Visualization version   GIF version

Theorem mndractf1o 33019
Description: An element 𝑋 of a monoid 𝐸 is invertible iff its right-translation 𝐺 is bijective. See also mndlactf1o 33018. 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.
StepHypRef Expression
1 oveq2 7439 . . . . . 6 (𝑣 = (𝐺0 ) → (𝑋 + 𝑣) = (𝑋 + (𝐺0 )))
21eqeq1d 2737 . . . . 5 (𝑣 = (𝐺0 ) → ((𝑋 + 𝑣) = 0 ↔ (𝑋 + (𝐺0 )) = 0 ))
3 f1ocnv 6861 . . . . . . . 8 (𝐺:𝐵1-1-onto𝐵𝐺:𝐵1-1-onto𝐵)
4 f1of 6849 . . . . . . . 8 (𝐺:𝐵1-1-onto𝐵𝐺:𝐵𝐵)
53, 4syl 17 . . . . . . 7 (𝐺:𝐵1-1-onto𝐵𝐺:𝐵𝐵)
65adantl 481 . . . . . 6 ((𝜑𝐺:𝐵1-1-onto𝐵) → 𝐺:𝐵𝐵)
7 mndractf1o.e . . . . . . . 8 (𝜑𝐸 ∈ Mnd)
8 mndractf1o.b . . . . . . . . 9 𝐵 = (Base‘𝐸)
9 mndractf1o.z . . . . . . . . 9 0 = (0g𝐸)
108, 9mndidcl 18775 . . . . . . . 8 (𝐸 ∈ Mnd → 0𝐵)
117, 10syl 17 . . . . . . 7 (𝜑0𝐵)
1211adantr 480 . . . . . 6 ((𝜑𝐺:𝐵1-1-onto𝐵) → 0𝐵)
136, 12ffvelcdmd 7105 . . . . 5 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝐺0 ) ∈ 𝐵)
14 f1of1 6848 . . . . . . 7 (𝐺:𝐵1-1-onto𝐵𝐺:𝐵1-1𝐵)
1514adantl 481 . . . . . 6 ((𝜑𝐺:𝐵1-1-onto𝐵) → 𝐺:𝐵1-1𝐵)
16 mndractf1o.p . . . . . . . 8 + = (+g𝐸)
177adantr 480 . . . . . . . 8 ((𝜑𝐺:𝐵1-1-onto𝐵) → 𝐸 ∈ Mnd)
18 mndractf1o.x . . . . . . . . 9 (𝜑𝑋𝐵)
1918adantr 480 . . . . . . . 8 ((𝜑𝐺:𝐵1-1-onto𝐵) → 𝑋𝐵)
208, 16, 17, 19, 13mndcld 33010 . . . . . . 7 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝑋 + (𝐺0 )) ∈ 𝐵)
2120, 12jca 511 . . . . . 6 ((𝜑𝐺:𝐵1-1-onto𝐵) → ((𝑋 + (𝐺0 )) ∈ 𝐵0𝐵))
228, 16, 9mndlid 18780 . . . . . . . 8 ((𝐸 ∈ Mnd ∧ 𝑋𝐵) → ( 0 + 𝑋) = 𝑋)
2317, 19, 22syl2anc 584 . . . . . . 7 ((𝜑𝐺:𝐵1-1-onto𝐵) → ( 0 + 𝑋) = 𝑋)
24 mndractf1o.f . . . . . . . 8 𝐺 = (𝑎𝐵 ↦ (𝑎 + 𝑋))
25 oveq1 7438 . . . . . . . 8 (𝑎 = 0 → (𝑎 + 𝑋) = ( 0 + 𝑋))
26 ovexd 7466 . . . . . . . 8 ((𝜑𝐺:𝐵1-1-onto𝐵) → ( 0 + 𝑋) ∈ V)
2724, 25, 12, 26fvmptd3 7039 . . . . . . 7 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝐺0 ) = ( 0 + 𝑋))
28 oveq1 7438 . . . . . . . . 9 (𝑎 = (𝑋 + (𝐺0 )) → (𝑎 + 𝑋) = ((𝑋 + (𝐺0 )) + 𝑋))
29 ovexd 7466 . . . . . . . . 9 ((𝜑𝐺:𝐵1-1-onto𝐵) → ((𝑋 + (𝐺0 )) + 𝑋) ∈ V)
3024, 28, 20, 29fvmptd3 7039 . . . . . . . 8 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝐺‘(𝑋 + (𝐺0 ))) = ((𝑋 + (𝐺0 )) + 𝑋))
318, 16, 17, 19, 13, 19mndassd 33011 . . . . . . . . 9 ((𝜑𝐺:𝐵1-1-onto𝐵) → ((𝑋 + (𝐺0 )) + 𝑋) = (𝑋 + ((𝐺0 ) + 𝑋)))
32 oveq1 7438 . . . . . . . . . . . 12 (𝑎 = (𝐺0 ) → (𝑎 + 𝑋) = ((𝐺0 ) + 𝑋))
33 ovexd 7466 . . . . . . . . . . . 12 ((𝜑𝐺:𝐵1-1-onto𝐵) → ((𝐺0 ) + 𝑋) ∈ V)
3424, 32, 13, 33fvmptd3 7039 . . . . . . . . . . 11 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝐺‘(𝐺0 )) = ((𝐺0 ) + 𝑋))
35 simpr 484 . . . . . . . . . . . 12 ((𝜑𝐺:𝐵1-1-onto𝐵) → 𝐺:𝐵1-1-onto𝐵)
36 f1ocnvfv2 7297 . . . . . . . . . . . 12 ((𝐺:𝐵1-1-onto𝐵0𝐵) → (𝐺‘(𝐺0 )) = 0 )
3735, 12, 36syl2anc 584 . . . . . . . . . . 11 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝐺‘(𝐺0 )) = 0 )
3834, 37eqtr3d 2777 . . . . . . . . . 10 ((𝜑𝐺:𝐵1-1-onto𝐵) → ((𝐺0 ) + 𝑋) = 0 )
3938oveq2d 7447 . . . . . . . . 9 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝑋 + ((𝐺0 ) + 𝑋)) = (𝑋 + 0 ))
408, 16, 9mndrid 18781 . . . . . . . . . 10 ((𝐸 ∈ Mnd ∧ 𝑋𝐵) → (𝑋 + 0 ) = 𝑋)
4117, 19, 40syl2anc 584 . . . . . . . . 9 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝑋 + 0 ) = 𝑋)
4231, 39, 413eqtrd 2779 . . . . . . . 8 ((𝜑𝐺:𝐵1-1-onto𝐵) → ((𝑋 + (𝐺0 )) + 𝑋) = 𝑋)
4330, 42eqtrd 2775 . . . . . . 7 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝐺‘(𝑋 + (𝐺0 ))) = 𝑋)
4423, 27, 433eqtr4rd 2786 . . . . . 6 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝐺‘(𝑋 + (𝐺0 ))) = (𝐺0 ))
45 f1fveq 7282 . . . . . . 7 ((𝐺:𝐵1-1𝐵 ∧ ((𝑋 + (𝐺0 )) ∈ 𝐵0𝐵)) → ((𝐺‘(𝑋 + (𝐺0 ))) = (𝐺0 ) ↔ (𝑋 + (𝐺0 )) = 0 ))
4645biimpa 476 . . . . . 6 (((𝐺:𝐵1-1𝐵 ∧ ((𝑋 + (𝐺0 )) ∈ 𝐵0𝐵)) ∧ (𝐺‘(𝑋 + (𝐺0 ))) = (𝐺0 )) → (𝑋 + (𝐺0 )) = 0 )
4715, 21, 44, 46syl21anc 838 . . . . 5 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝑋 + (𝐺0 )) = 0 )
482, 13, 47rspcedvdw 3625 . . . 4 ((𝜑𝐺:𝐵1-1-onto𝐵) → ∃𝑣𝐵 (𝑋 + 𝑣) = 0 )
49 f1ofo 6856 . . . . 5 (𝐺:𝐵1-1-onto𝐵𝐺:𝐵onto𝐵)
508, 9, 16, 24, 7, 18mndractfo 33017 . . . . . 6 (𝜑 → (𝐺:𝐵onto𝐵 ↔ ∃𝑤𝐵 (𝑤 + 𝑋) = 0 ))
5150biimpa 476 . . . . 5 ((𝜑𝐺:𝐵onto𝐵) → ∃𝑤𝐵 (𝑤 + 𝑋) = 0 )
5249, 51sylan2 593 . . . 4 ((𝜑𝐺:𝐵1-1-onto𝐵) → ∃𝑤𝐵 (𝑤 + 𝑋) = 0 )
5348, 52jca 511 . . 3 ((𝜑𝐺:𝐵1-1-onto𝐵) → (∃𝑣𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤𝐵 (𝑤 + 𝑋) = 0 ))
547ad2antrr 726 . . . . . . 7 (((𝜑𝑣𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐸 ∈ Mnd)
5518ad2antrr 726 . . . . . . 7 (((𝜑𝑣𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝑋𝐵)
56 simplr 769 . . . . . . 7 (((𝜑𝑣𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝑣𝐵)
57 simpr 484 . . . . . . 7 (((𝜑𝑣𝐵) ∧ (𝑋 + 𝑣) = 0 ) → (𝑋 + 𝑣) = 0 )
588, 9, 16, 24, 54, 55, 56, 57mndractf1 33016 . . . . . 6 (((𝜑𝑣𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵1-1𝐵)
5958r19.29an 3156 . . . . 5 ((𝜑 ∧ ∃𝑣𝐵 (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵1-1𝐵)
6050biimpar 477 . . . . 5 ((𝜑 ∧ ∃𝑤𝐵 (𝑤 + 𝑋) = 0 ) → 𝐺:𝐵onto𝐵)
6159, 60anim12dan 619 . . . 4 ((𝜑 ∧ (∃𝑣𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤𝐵 (𝑤 + 𝑋) = 0 )) → (𝐺:𝐵1-1𝐵𝐺:𝐵onto𝐵))
62 df-f1o 6570 . . . 4 (𝐺:𝐵1-1-onto𝐵 ↔ (𝐺:𝐵1-1𝐵𝐺:𝐵onto𝐵))
6361, 62sylibr 234 . . 3 ((𝜑 ∧ (∃𝑣𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤𝐵 (𝑤 + 𝑋) = 0 )) → 𝐺:𝐵1-1-onto𝐵)
6453, 63impbida 801 . 2 (𝜑 → (𝐺:𝐵1-1-onto𝐵 ↔ (∃𝑣𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤𝐵 (𝑤 + 𝑋) = 0 )))
658, 9, 16, 7, 18mndlrinvb 33013 . 2 (𝜑 → ((∃𝑣𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤𝐵 (𝑤 + 𝑋) = 0 ) ↔ ∃𝑦𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))
6664, 65bitrd 279 1 (𝜑 → (𝐺:𝐵1-1-onto𝐵 ↔ ∃𝑦𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  wrex 3068  Vcvv 3478  cmpt 5231  ccnv 5688  wf 6559  1-1wf1 6560  ontowfo 6561  1-1-ontowf1o 6562  cfv 6563  (class class class)co 7431  Basecbs 17245  +gcplusg 17298  0gc0g 17486  Mndcmnd 18760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-0g 17488  df-mgm 18666  df-sgrp 18745  df-mnd 18761
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator