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 33036
Description: An element 𝑋 of a monoid 𝐸 is invertible iff its right-translation 𝐺 is bijective. See also mndlactf1o 33035. 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 2739 . . . . 5 (𝑣 = (𝐺0 ) → ((𝑋 + 𝑣) = 0 ↔ (𝑋 + (𝐺0 )) = 0 ))
3 f1ocnv 6860 . . . . . . . 8 (𝐺:𝐵1-1-onto𝐵𝐺:𝐵1-1-onto𝐵)
4 f1of 6848 . . . . . . . 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 18762 . . . . . . . 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 6847 . . . . . . 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 33027 . . . . . . 7 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝑋 + (𝐺0 )) ∈ 𝐵)
2120, 12jca 511 . . . . . 6 ((𝜑𝐺:𝐵1-1-onto𝐵) → ((𝑋 + (𝐺0 )) ∈ 𝐵0𝐵))
228, 16, 9mndlid 18767 . . . . . . . 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 33028 . . . . . . . . 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 2779 . . . . . . . . . 10 ((𝜑𝐺:𝐵1-1-onto𝐵) → ((𝐺0 ) + 𝑋) = 0 )
3938oveq2d 7447 . . . . . . . . 9 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝑋 + ((𝐺0 ) + 𝑋)) = (𝑋 + 0 ))
408, 16, 9mndrid 18768 . . . . . . . . . 10 ((𝐸 ∈ Mnd ∧ 𝑋𝐵) → (𝑋 + 0 ) = 𝑋)
4117, 19, 40syl2anc 584 . . . . . . . . 9 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝑋 + 0 ) = 𝑋)
4231, 39, 413eqtrd 2781 . . . . . . . 8 ((𝜑𝐺:𝐵1-1-onto𝐵) → ((𝑋 + (𝐺0 )) + 𝑋) = 𝑋)
4330, 42eqtrd 2777 . . . . . . 7 ((𝜑𝐺:𝐵1-1-onto𝐵) → (𝐺‘(𝑋 + (𝐺0 ))) = 𝑋)
4423, 27, 433eqtr4rd 2788 . . . . . 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 6855 . . . . 5 (𝐺:𝐵1-1-onto𝐵𝐺:𝐵onto𝐵)
508, 9, 16, 24, 7, 18mndractfo 33034 . . . . . 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 33033 . . . . . 6 (((𝜑𝑣𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵1-1𝐵)
5958r19.29an 3158 . . . . 5 ((𝜑 ∧ ∃𝑣𝐵 (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵1-1𝐵)
6050biimpar 477 . . . . 5 ((𝜑 ∧ ∃𝑤𝐵 (𝑤 + 𝑋) = 0 ) → 𝐺:𝐵onto𝐵)
6159, 60anim12dan 619 . . . 4 ((𝜑 ∧ (∃𝑣𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤𝐵 (𝑤 + 𝑋) = 0 )) → (𝐺:𝐵1-1𝐵𝐺:𝐵onto𝐵))
62 df-f1o 6568 . . . 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 33030 . 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 1540  wcel 2108  wrex 3070  Vcvv 3480  cmpt 5225  ccnv 5684  wf 6557  1-1wf1 6558  ontowfo 6559  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  Basecbs 17247  +gcplusg 17297  0gc0g 17484  Mndcmnd 18747
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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-0g 17486  df-mgm 18653  df-sgrp 18732  df-mnd 18748
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator