MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  issgrp Structured version   Visualization version   GIF version

Theorem issgrp 18611
Description: The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
Hypotheses
Ref Expression
issgrp.b 𝐵 = (Base‘𝑀)
issgrp.o = (+g𝑀)
Assertion
Ref Expression
issgrp (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
Distinct variable groups:   𝑥,𝐵,𝑦,𝑧   𝑥,𝑀,𝑦,𝑧   𝑥, ,𝑦,𝑧

Proof of Theorem issgrp
Dummy variables 𝑏 𝑔 𝑜 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvexd 6907 . . 3 (𝑔 = 𝑀 → (Base‘𝑔) ∈ V)
2 fveq2 6892 . . . 4 (𝑔 = 𝑀 → (Base‘𝑔) = (Base‘𝑀))
3 issgrp.b . . . 4 𝐵 = (Base‘𝑀)
42, 3eqtr4di 2791 . . 3 (𝑔 = 𝑀 → (Base‘𝑔) = 𝐵)
5 fvexd 6907 . . . 4 ((𝑔 = 𝑀𝑏 = 𝐵) → (+g𝑔) ∈ V)
6 fveq2 6892 . . . . . 6 (𝑔 = 𝑀 → (+g𝑔) = (+g𝑀))
76adantr 482 . . . . 5 ((𝑔 = 𝑀𝑏 = 𝐵) → (+g𝑔) = (+g𝑀))
8 issgrp.o . . . . 5 = (+g𝑀)
97, 8eqtr4di 2791 . . . 4 ((𝑔 = 𝑀𝑏 = 𝐵) → (+g𝑔) = )
10 simplr 768 . . . . 5 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → 𝑏 = 𝐵)
11 id 22 . . . . . . . . . 10 (𝑜 = 𝑜 = )
12 oveq 7415 . . . . . . . . . 10 (𝑜 = → (𝑥𝑜𝑦) = (𝑥 𝑦))
13 eqidd 2734 . . . . . . . . . 10 (𝑜 = 𝑧 = 𝑧)
1411, 12, 13oveq123d 7430 . . . . . . . . 9 (𝑜 = → ((𝑥𝑜𝑦)𝑜𝑧) = ((𝑥 𝑦) 𝑧))
15 eqidd 2734 . . . . . . . . . 10 (𝑜 = 𝑥 = 𝑥)
16 oveq 7415 . . . . . . . . . 10 (𝑜 = → (𝑦𝑜𝑧) = (𝑦 𝑧))
1711, 15, 16oveq123d 7430 . . . . . . . . 9 (𝑜 = → (𝑥𝑜(𝑦𝑜𝑧)) = (𝑥 (𝑦 𝑧)))
1814, 17eqeq12d 2749 . . . . . . . 8 (𝑜 = → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
1918adantl 483 . . . . . . 7 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2010, 19raleqbidv 3343 . . . . . 6 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (∀𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2110, 20raleqbidv 3343 . . . . 5 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (∀𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2210, 21raleqbidv 3343 . . . 4 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (∀𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
235, 9, 22sbcied2 3825 . . 3 ((𝑔 = 𝑀𝑏 = 𝐵) → ([(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
241, 4, 23sbcied2 3825 . 2 (𝑔 = 𝑀 → ([(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
25 df-sgrp 18610 . 2 Smgrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
2624, 25elrab2 3687 1 (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3062  Vcvv 3475  [wsbc 3778  cfv 6544  (class class class)co 7409  Basecbs 17144  +gcplusg 17197  Mgmcmgm 18559  Smgrpcsgrp 18609
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-sgrp 18610
This theorem is referenced by:  issgrpv  18612  issgrpn0  18613  isnsgrp  18614  sgrpmgm  18615  sgrpass  18616  sgrp0  18618  sgrp0b  18619  sgrp1  18620  efmndsgrp  18767  smndex1sgrp  18789  sgrp2nmndlem4  18809  copissgrp  46578  nnsgrp  46587  sgrpplusgaopALT  46605  sgrp2sgrp  46638  rnglidlmsgrp  46757  2zrngasgrp  46838  2zrngmsgrp  46845
  Copyright terms: Public domain W3C validator