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

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

Proof of Theorem issgrp
Dummy variables 𝑏 𝑔 𝑜 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 6163 . . . 4 (Base‘𝑔) ∈ V
21a1i 11 . . 3 (𝑔 = 𝑀 → (Base‘𝑔) ∈ V)
3 fveq2 6153 . . . 4 (𝑔 = 𝑀 → (Base‘𝑔) = (Base‘𝑀))
4 issgrp.b . . . 4 𝐵 = (Base‘𝑀)
53, 4syl6eqr 2673 . . 3 (𝑔 = 𝑀 → (Base‘𝑔) = 𝐵)
6 fvex 6163 . . . . 5 (+g𝑔) ∈ V
76a1i 11 . . . 4 ((𝑔 = 𝑀𝑏 = 𝐵) → (+g𝑔) ∈ V)
8 fveq2 6153 . . . . . 6 (𝑔 = 𝑀 → (+g𝑔) = (+g𝑀))
98adantr 481 . . . . 5 ((𝑔 = 𝑀𝑏 = 𝐵) → (+g𝑔) = (+g𝑀))
10 issgrp.o . . . . 5 = (+g𝑀)
119, 10syl6eqr 2673 . . . 4 ((𝑔 = 𝑀𝑏 = 𝐵) → (+g𝑔) = )
12 simplr 791 . . . . 5 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → 𝑏 = 𝐵)
13 id 22 . . . . . . . . . 10 (𝑜 = 𝑜 = )
14 oveq 6616 . . . . . . . . . 10 (𝑜 = → (𝑥𝑜𝑦) = (𝑥 𝑦))
15 eqidd 2622 . . . . . . . . . 10 (𝑜 = 𝑧 = 𝑧)
1613, 14, 15oveq123d 6631 . . . . . . . . 9 (𝑜 = → ((𝑥𝑜𝑦)𝑜𝑧) = ((𝑥 𝑦) 𝑧))
17 eqidd 2622 . . . . . . . . . 10 (𝑜 = 𝑥 = 𝑥)
18 oveq 6616 . . . . . . . . . 10 (𝑜 = → (𝑦𝑜𝑧) = (𝑦 𝑧))
1913, 17, 18oveq123d 6631 . . . . . . . . 9 (𝑜 = → (𝑥𝑜(𝑦𝑜𝑧)) = (𝑥 (𝑦 𝑧)))
2016, 19eqeq12d 2636 . . . . . . . 8 (𝑜 = → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2120adantl 482 . . . . . . 7 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2212, 21raleqbidv 3144 . . . . . 6 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (∀𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2312, 22raleqbidv 3144 . . . . 5 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (∀𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
2412, 23raleqbidv 3144 . . . 4 (((𝑔 = 𝑀𝑏 = 𝐵) ∧ 𝑜 = ) → (∀𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
257, 11, 24sbcied2 3459 . . 3 ((𝑔 = 𝑀𝑏 = 𝐵) → ([(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
262, 5, 25sbcied2 3459 . 2 (𝑔 = 𝑀 → ([(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
27 df-sgrp 17212 . 2 SGrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
2826, 27elrab2 3352 1 (𝑀 ∈ SGrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 𝑦) 𝑧) = (𝑥 (𝑦 𝑧))))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  Vcvv 3189  [wsbc 3421  cfv 5852  (class class class)co 6610  Basecbs 15788  +gcplusg 15869  Mgmcmgm 17168  SGrpcsgrp 17211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4754
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5815  df-fv 5860  df-ov 6613  df-sgrp 17212
This theorem is referenced by:  issgrpv  17214  issgrpn0  17215  isnsgrp  17216  sgrpmgm  17217  sgrpass  17218  sgrp0  17219  sgrp0b  17220  sgrp1  17221  sgrp2nmndlem4  17343  copissgrp  41117  nnsgrp  41126  sgrpplusgaopALT  41140  sgrp2sgrp  41173  lidlmsgrp  41235  2zrngasgrp  41249  2zrngmsgrp  41256
  Copyright terms: Public domain W3C validator