Theorem issgrp 18680

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.

Step	Hyp	Ref	Expression
1		fvexd 6912	. . 3 ⊢ (𝑔 = 𝑀 → (Base‘𝑔) ∈ V)
2		fveq2 6897	. . . 4 ⊢ (𝑔 = 𝑀 → (Base‘𝑔) = (Base‘𝑀))
3		issgrp.b	. . . 4 ⊢ 𝐵 = (Base‘𝑀)
4	2, 3	eqtr4di 2786	. . 3 ⊢ (𝑔 = 𝑀 → (Base‘𝑔) = 𝐵)
5		fvexd 6912	. . . 4 ⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑔) ∈ V)
6		fveq2 6897	. . . . . 6 ⊢ (𝑔 = 𝑀 → (+g‘𝑔) = (+g‘𝑀))
7	6	adantr 480	. . . . 5 ⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑔) = (+g‘𝑀))
8		issgrp.o	. . . . 5 ⊢ ⚬ = (+g‘𝑀)
9	7, 8	eqtr4di 2786	. . . 4 ⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑔) = ⚬ )
10		simplr 768	. . . . 5 ⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → 𝑏 = 𝐵)
11		id 22	. . . . . . . . . 10 ⊢ (𝑜 = ⚬ → 𝑜 = ⚬ )
12		oveq 7426	. . . . . . . . . 10 ⊢ (𝑜 = ⚬ → (𝑥𝑜𝑦) = (𝑥 ⚬ 𝑦))
13		eqidd 2729	. . . . . . . . . 10 ⊢ (𝑜 = ⚬ → 𝑧 = 𝑧)
14	11, 12, 13	oveq123d 7441	. . . . . . . . 9 ⊢ (𝑜 = ⚬ → ((𝑥𝑜𝑦)𝑜𝑧) = ((𝑥 ⚬ 𝑦) ⚬ 𝑧))
15		eqidd 2729	. . . . . . . . . 10 ⊢ (𝑜 = ⚬ → 𝑥 = 𝑥)
16		oveq 7426	. . . . . . . . . 10 ⊢ (𝑜 = ⚬ → (𝑦𝑜𝑧) = (𝑦 ⚬ 𝑧))
17	11, 15, 16	oveq123d 7441	. . . . . . . . 9 ⊢ (𝑜 = ⚬ → (𝑥𝑜(𝑦𝑜𝑧)) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))
18	14, 17	eqeq12d 2744	. . . . . . . 8 ⊢ (𝑜 = ⚬ → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
19	18	adantl 481	. . . . . . 7 ⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
20	10, 19	raleqbidv 3339	. . . . . 6 ⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
21	10, 20	raleqbidv 3339	. . . . 5 ⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
22	10, 21	raleqbidv 3339	. . . 4 ⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
23	5, 9, 22	sbcied2 3824	. . 3 ⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → ([(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
24	1, 4, 23	sbcied2 3824	. 2 ⊢ (𝑔 = 𝑀 → ([(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
25		df-sgrp 18679	. 2 ⊢ Smgrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
26	24, 25	elrab2 3685	1 ⊢ (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099  ∀wral 3058  Vcvv 3471  [wsbc 3776  ‘cfv 6548  (class class class)co 7420  Basecbs 17180  +_gcplusg 17233  Mgmcmgm 18598  Smgrpcsgrp 18678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-sgrp 18679

This theorem is referenced by:  issgrpv  18681  issgrpn0  18682  isnsgrp  18683  sgrpmgm  18684  sgrpass  18685  sgrp0  18687  sgrp0b  18688  sgrp1  18689  efmndsgrp  18838  smndex1sgrp  18860  sgrp2nmndlem4  18880  rnglidlmsgrp  21141  copissgrp  47230  nnsgrp  47239  sgrpplusgaopALT  47257  sgrp2sgrp  47290  2zrngasgrp  47308  2zrngmsgrp  47315