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

Theorem issgrp 18651
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 6899 . . 3 (𝑔 = 𝑀 → (Base‘𝑔) ∈ V)
2 fveq2 6884 . . . 4 (𝑔 = 𝑀 → (Base‘𝑔) = (Base‘𝑀))
3 issgrp.b . . . 4 𝐵 = (Base‘𝑀)
42, 3eqtr4di 2784 . . 3 (𝑔 = 𝑀 → (Base‘𝑔) = 𝐵)
5 fvexd 6899 . . . 4 ((𝑔 = 𝑀𝑏 = 𝐵) → (+g𝑔) ∈ V)
6 fveq2 6884 . . . . . 6 (𝑔 = 𝑀 → (+g𝑔) = (+g𝑀))
76adantr 480 . . . . 5 ((𝑔 = 𝑀𝑏 = 𝐵) → (+g𝑔) = (+g𝑀))
8 issgrp.o . . . . 5 = (+g𝑀)
97, 8eqtr4di 2784 . . . 4 ((𝑔 = 𝑀𝑏 = 𝐵) → (+g𝑔) = )
10 simplr 766 . . . . 5 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → 𝑏 = 𝐵)
11 id 22 . . . . . . . . . 10 (𝑜 = 𝑜 = )
12 oveq 7410 . . . . . . . . . 10 (𝑜 = → (𝑥𝑜𝑦) = (𝑥 𝑦))
13 eqidd 2727 . . . . . . . . . 10 (𝑜 = 𝑧 = 𝑧)
1411, 12, 13oveq123d 7425 . . . . . . . . 9 (𝑜 = → ((𝑥𝑜𝑦)𝑜𝑧) = ((𝑥 𝑦) 𝑧))
15 eqidd 2727 . . . . . . . . . 10 (𝑜 = 𝑥 = 𝑥)
16 oveq 7410 . . . . . . . . . 10 (𝑜 = → (𝑦𝑜𝑧) = (𝑦 𝑧))
1711, 15, 16oveq123d 7425 . . . . . . . . 9 (𝑜 = → (𝑥𝑜(𝑦𝑜𝑧)) = (𝑥 (𝑦 𝑧)))
1814, 17eqeq12d 2742 . . . . . . . 8 (𝑜 = → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
1918adantl 481 . . . . . . 7 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2010, 19raleqbidv 3336 . . . . . 6 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (∀𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2110, 20raleqbidv 3336 . . . . 5 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (∀𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2210, 21raleqbidv 3336 . . . 4 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (∀𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
235, 9, 22sbcied2 3819 . . 3 ((𝑔 = 𝑀𝑏 = 𝐵) → ([(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
241, 4, 23sbcied2 3819 . 2 (𝑔 = 𝑀 → ([(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
25 df-sgrp 18650 . 2 Smgrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
2624, 25elrab2 3681 1 (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 395   = wceq 1533  wcel 2098  wral 3055  Vcvv 3468  [wsbc 3772  cfv 6536  (class class class)co 7404  Basecbs 17151  +gcplusg 17204  Mgmcmgm 18569  Smgrpcsgrp 18649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-nul 5299
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-ral 3056  df-rab 3427  df-v 3470  df-sbc 3773  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6488  df-fv 6544  df-ov 7407  df-sgrp 18650
This theorem is referenced by:  issgrpv  18652  issgrpn0  18653  isnsgrp  18654  sgrpmgm  18655  sgrpass  18656  sgrp0  18658  sgrp0b  18659  sgrp1  18660  efmndsgrp  18809  smndex1sgrp  18831  sgrp2nmndlem4  18851  rnglidlmsgrp  21102  copissgrp  47099  nnsgrp  47108  sgrpplusgaopALT  47126  sgrp2sgrp  47159  2zrngasgrp  47177  2zrngmsgrp  47184
  Copyright terms: Public domain W3C validator