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

Theorem issgrp 18607
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 6903 . . 3 (𝑔 = 𝑀 → (Base‘𝑔) ∈ V)
2 fveq2 6888 . . . 4 (𝑔 = 𝑀 → (Base‘𝑔) = (Base‘𝑀))
3 issgrp.b . . . 4 𝐵 = (Base‘𝑀)
42, 3eqtr4di 2790 . . 3 (𝑔 = 𝑀 → (Base‘𝑔) = 𝐵)
5 fvexd 6903 . . . 4 ((𝑔 = 𝑀𝑏 = 𝐵) → (+g𝑔) ∈ V)
6 fveq2 6888 . . . . . 6 (𝑔 = 𝑀 → (+g𝑔) = (+g𝑀))
76adantr 481 . . . . 5 ((𝑔 = 𝑀𝑏 = 𝐵) → (+g𝑔) = (+g𝑀))
8 issgrp.o . . . . 5 = (+g𝑀)
97, 8eqtr4di 2790 . . . 4 ((𝑔 = 𝑀𝑏 = 𝐵) → (+g𝑔) = )
10 simplr 767 . . . . 5 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → 𝑏 = 𝐵)
11 id 22 . . . . . . . . . 10 (𝑜 = 𝑜 = )
12 oveq 7411 . . . . . . . . . 10 (𝑜 = → (𝑥𝑜𝑦) = (𝑥 𝑦))
13 eqidd 2733 . . . . . . . . . 10 (𝑜 = 𝑧 = 𝑧)
1411, 12, 13oveq123d 7426 . . . . . . . . 9 (𝑜 = → ((𝑥𝑜𝑦)𝑜𝑧) = ((𝑥 𝑦) 𝑧))
15 eqidd 2733 . . . . . . . . . 10 (𝑜 = 𝑥 = 𝑥)
16 oveq 7411 . . . . . . . . . 10 (𝑜 = → (𝑦𝑜𝑧) = (𝑦 𝑧))
1711, 15, 16oveq123d 7426 . . . . . . . . 9 (𝑜 = → (𝑥𝑜(𝑦𝑜𝑧)) = (𝑥 (𝑦 𝑧)))
1814, 17eqeq12d 2748 . . . . . . . 8 (𝑜 = → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
1918adantl 482 . . . . . . 7 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2010, 19raleqbidv 3342 . . . . . 6 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (∀𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2110, 20raleqbidv 3342 . . . . 5 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (∀𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2210, 21raleqbidv 3342 . . . 4 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (∀𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
235, 9, 22sbcied2 3823 . . 3 ((𝑔 = 𝑀𝑏 = 𝐵) → ([(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
241, 4, 23sbcied2 3823 . 2 (𝑔 = 𝑀 → ([(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
25 df-sgrp 18606 . 2 Smgrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
2624, 25elrab2 3685 1 (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3061  Vcvv 3474  [wsbc 3776  cfv 6540  (class class class)co 7405  Basecbs 17140  +gcplusg 17193  Mgmcmgm 18555  Smgrpcsgrp 18605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5305
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rab 3433  df-v 3476  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-sgrp 18606
This theorem is referenced by:  issgrpv  18608  issgrpn0  18609  isnsgrp  18610  sgrpmgm  18611  sgrpass  18612  sgrp0  18614  sgrp0b  18615  sgrp1  18616  efmndsgrp  18763  smndex1sgrp  18785  sgrp2nmndlem4  18805  copissgrp  46564  nnsgrp  46573  sgrpplusgaopALT  46591  sgrp2sgrp  46624  rnglidlmsgrp  46739  2zrngasgrp  46791  2zrngmsgrp  46798
  Copyright terms: Public domain W3C validator