ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfgrp2 GIF version

Theorem dfgrp2 12779
Description: Alternate definition of a group as semigroup with a left identity and a left inverse for each element. This "definition" is weaker than df-grp 12757, based on the definition of a monoid which provides a left and a right identity. (Contributed by AV, 28-Aug-2021.)
Hypotheses
Ref Expression
dfgrp2.b 𝐵 = (Base‘𝐺)
dfgrp2.p + = (+g𝐺)
Assertion
Ref Expression
dfgrp2 (𝐺 ∈ Grp ↔ (𝐺 ∈ Smgrp ∧ ∃𝑛𝐵𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)))
Distinct variable groups:   𝐵,𝑖,𝑛,𝑥   𝑖,𝐺,𝑛,𝑥   + ,𝑖,𝑛,𝑥

Proof of Theorem dfgrp2
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grpsgrp 12778 . . 3 (𝐺 ∈ Grp → 𝐺 ∈ Smgrp)
2 grpmnd 12761 . . . . 5 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
3 dfgrp2.b . . . . . 6 𝐵 = (Base‘𝐺)
4 eqid 2177 . . . . . 6 (0g𝐺) = (0g𝐺)
53, 4mndidcl 12710 . . . . 5 (𝐺 ∈ Mnd → (0g𝐺) ∈ 𝐵)
62, 5syl 14 . . . 4 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝐵)
7 oveq1 5875 . . . . . . . 8 (𝑛 = (0g𝐺) → (𝑛 + 𝑥) = ((0g𝐺) + 𝑥))
87eqeq1d 2186 . . . . . . 7 (𝑛 = (0g𝐺) → ((𝑛 + 𝑥) = 𝑥 ↔ ((0g𝐺) + 𝑥) = 𝑥))
9 eqeq2 2187 . . . . . . . 8 (𝑛 = (0g𝐺) → ((𝑖 + 𝑥) = 𝑛 ↔ (𝑖 + 𝑥) = (0g𝐺)))
109rexbidv 2478 . . . . . . 7 (𝑛 = (0g𝐺) → (∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛 ↔ ∃𝑖𝐵 (𝑖 + 𝑥) = (0g𝐺)))
118, 10anbi12d 473 . . . . . 6 (𝑛 = (0g𝐺) → (((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛) ↔ (((0g𝐺) + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = (0g𝐺))))
1211ralbidv 2477 . . . . 5 (𝑛 = (0g𝐺) → (∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛) ↔ ∀𝑥𝐵 (((0g𝐺) + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = (0g𝐺))))
1312adantl 277 . . . 4 ((𝐺 ∈ Grp ∧ 𝑛 = (0g𝐺)) → (∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛) ↔ ∀𝑥𝐵 (((0g𝐺) + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = (0g𝐺))))
14 dfgrp2.p . . . . . . . 8 + = (+g𝐺)
153, 14, 4mndlid 12715 . . . . . . 7 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → ((0g𝐺) + 𝑥) = 𝑥)
162, 15sylan 283 . . . . . 6 ((𝐺 ∈ Grp ∧ 𝑥𝐵) → ((0g𝐺) + 𝑥) = 𝑥)
173, 14, 4grpinvex 12764 . . . . . 6 ((𝐺 ∈ Grp ∧ 𝑥𝐵) → ∃𝑖𝐵 (𝑖 + 𝑥) = (0g𝐺))
1816, 17jca 306 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑥𝐵) → (((0g𝐺) + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = (0g𝐺)))
1918ralrimiva 2550 . . . 4 (𝐺 ∈ Grp → ∀𝑥𝐵 (((0g𝐺) + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = (0g𝐺)))
206, 13, 19rspcedvd 2847 . . 3 (𝐺 ∈ Grp → ∃𝑛𝐵𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛))
211, 20jca 306 . 2 (𝐺 ∈ Grp → (𝐺 ∈ Smgrp ∧ ∃𝑛𝐵𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)))
223a1i 9 . . . . . 6 (((𝑛𝐵 ∧ ∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) ∧ 𝐺 ∈ Smgrp) → 𝐵 = (Base‘𝐺))
2314a1i 9 . . . . . 6 (((𝑛𝐵 ∧ ∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) ∧ 𝐺 ∈ Smgrp) → + = (+g𝐺))
24 sgrpmgm 12692 . . . . . . . 8 (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm)
2524adantl 277 . . . . . . 7 (((𝑛𝐵 ∧ ∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) ∧ 𝐺 ∈ Smgrp) → 𝐺 ∈ Mgm)
263, 14mgmcl 12657 . . . . . . 7 ((𝐺 ∈ Mgm ∧ 𝑎𝐵𝑏𝐵) → (𝑎 + 𝑏) ∈ 𝐵)
2725, 26syl3an1 1271 . . . . . 6 ((((𝑛𝐵 ∧ ∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) ∧ 𝐺 ∈ Smgrp) ∧ 𝑎𝐵𝑏𝐵) → (𝑎 + 𝑏) ∈ 𝐵)
283, 14sgrpass 12693 . . . . . . 7 ((𝐺 ∈ Smgrp ∧ (𝑎𝐵𝑏𝐵𝑐𝐵)) → ((𝑎 + 𝑏) + 𝑐) = (𝑎 + (𝑏 + 𝑐)))
2928adantll 476 . . . . . 6 ((((𝑛𝐵 ∧ ∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) ∧ 𝐺 ∈ Smgrp) ∧ (𝑎𝐵𝑏𝐵𝑐𝐵)) → ((𝑎 + 𝑏) + 𝑐) = (𝑎 + (𝑏 + 𝑐)))
30 simpll 527 . . . . . 6 (((𝑛𝐵 ∧ ∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) ∧ 𝐺 ∈ Smgrp) → 𝑛𝐵)
31 oveq2 5876 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑛 + 𝑥) = (𝑛 + 𝑎))
32 id 19 . . . . . . . . . . . 12 (𝑥 = 𝑎𝑥 = 𝑎)
3331, 32eqeq12d 2192 . . . . . . . . . . 11 (𝑥 = 𝑎 → ((𝑛 + 𝑥) = 𝑥 ↔ (𝑛 + 𝑎) = 𝑎))
34 oveq2 5876 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝑖 + 𝑥) = (𝑖 + 𝑎))
3534eqeq1d 2186 . . . . . . . . . . . 12 (𝑥 = 𝑎 → ((𝑖 + 𝑥) = 𝑛 ↔ (𝑖 + 𝑎) = 𝑛))
3635rexbidv 2478 . . . . . . . . . . 11 (𝑥 = 𝑎 → (∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛 ↔ ∃𝑖𝐵 (𝑖 + 𝑎) = 𝑛))
3733, 36anbi12d 473 . . . . . . . . . 10 (𝑥 = 𝑎 → (((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛) ↔ ((𝑛 + 𝑎) = 𝑎 ∧ ∃𝑖𝐵 (𝑖 + 𝑎) = 𝑛)))
3837rspcv 2837 . . . . . . . . 9 (𝑎𝐵 → (∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛) → ((𝑛 + 𝑎) = 𝑎 ∧ ∃𝑖𝐵 (𝑖 + 𝑎) = 𝑛)))
39 simpl 109 . . . . . . . . 9 (((𝑛 + 𝑎) = 𝑎 ∧ ∃𝑖𝐵 (𝑖 + 𝑎) = 𝑛) → (𝑛 + 𝑎) = 𝑎)
4038, 39syl6com 35 . . . . . . . 8 (∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛) → (𝑎𝐵 → (𝑛 + 𝑎) = 𝑎))
4140ad2antlr 489 . . . . . . 7 (((𝑛𝐵 ∧ ∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) ∧ 𝐺 ∈ Smgrp) → (𝑎𝐵 → (𝑛 + 𝑎) = 𝑎))
4241imp 124 . . . . . 6 ((((𝑛𝐵 ∧ ∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) ∧ 𝐺 ∈ Smgrp) ∧ 𝑎𝐵) → (𝑛 + 𝑎) = 𝑎)
43 oveq1 5875 . . . . . . . . . . . . 13 (𝑖 = 𝑏 → (𝑖 + 𝑎) = (𝑏 + 𝑎))
4443eqeq1d 2186 . . . . . . . . . . . 12 (𝑖 = 𝑏 → ((𝑖 + 𝑎) = 𝑛 ↔ (𝑏 + 𝑎) = 𝑛))
4544cbvrexvw 2708 . . . . . . . . . . 11 (∃𝑖𝐵 (𝑖 + 𝑎) = 𝑛 ↔ ∃𝑏𝐵 (𝑏 + 𝑎) = 𝑛)
4645biimpi 120 . . . . . . . . . 10 (∃𝑖𝐵 (𝑖 + 𝑎) = 𝑛 → ∃𝑏𝐵 (𝑏 + 𝑎) = 𝑛)
4746adantl 277 . . . . . . . . 9 (((𝑛 + 𝑎) = 𝑎 ∧ ∃𝑖𝐵 (𝑖 + 𝑎) = 𝑛) → ∃𝑏𝐵 (𝑏 + 𝑎) = 𝑛)
4838, 47syl6com 35 . . . . . . . 8 (∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛) → (𝑎𝐵 → ∃𝑏𝐵 (𝑏 + 𝑎) = 𝑛))
4948ad2antlr 489 . . . . . . 7 (((𝑛𝐵 ∧ ∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) ∧ 𝐺 ∈ Smgrp) → (𝑎𝐵 → ∃𝑏𝐵 (𝑏 + 𝑎) = 𝑛))
5049imp 124 . . . . . 6 ((((𝑛𝐵 ∧ ∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) ∧ 𝐺 ∈ Smgrp) ∧ 𝑎𝐵) → ∃𝑏𝐵 (𝑏 + 𝑎) = 𝑛)
5122, 23, 27, 29, 30, 42, 50isgrpde 12775 . . . . 5 (((𝑛𝐵 ∧ ∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) ∧ 𝐺 ∈ Smgrp) → 𝐺 ∈ Grp)
5251ex 115 . . . 4 ((𝑛𝐵 ∧ ∀𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) → (𝐺 ∈ Smgrp → 𝐺 ∈ Grp))
5352rexlimiva 2589 . . 3 (∃𝑛𝐵𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛) → (𝐺 ∈ Smgrp → 𝐺 ∈ Grp))
5453impcom 125 . 2 ((𝐺 ∈ Smgrp ∧ ∃𝑛𝐵𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)) → 𝐺 ∈ Grp)
5521, 54impbii 126 1 (𝐺 ∈ Grp ↔ (𝐺 ∈ Smgrp ∧ ∃𝑛𝐵𝑥𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖𝐵 (𝑖 + 𝑥) = 𝑛)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 978   = wceq 1353  wcel 2148  wral 2455  wrex 2456  cfv 5211  (class class class)co 5868  Basecbs 12432  +gcplusg 12505  0gc0g 12640  Mgmcmgm 12652  Smgrpcsgrp 12686  Mndcmnd 12696  Grpcgrp 12754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4205  ax-un 4429  ax-cnex 7880  ax-resscn 7881  ax-1re 7883  ax-addrcl 7886
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4289  df-xp 4628  df-rel 4629  df-cnv 4630  df-co 4631  df-dm 4632  df-rn 4633  df-res 4634  df-iota 5173  df-fun 5213  df-fn 5214  df-fv 5219  df-riota 5824  df-ov 5871  df-inn 8896  df-2 8954  df-ndx 12435  df-slot 12436  df-base 12438  df-plusg 12518  df-0g 12642  df-mgm 12654  df-sgrp 12687  df-mnd 12697  df-grp 12757
This theorem is referenced by:  dfgrp2e  12780  dfgrp3m  12845
  Copyright terms: Public domain W3C validator