Theorem ismnddef 17504

Description: The predicate "is a monoid", corresponding 1-to-1 to the definition. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 1-Feb-2020.)

Hypotheses

Ref	Expression
ismnddef.b	⊢ 𝐵 = (Base‘𝐺)
ismnddef.p	⊢ + = (+g‘𝐺)

Assertion

Ref	Expression
ismnddef	⊢ (𝐺 ∈ Mnd ↔ (𝐺 ∈ SGrp ∧ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎)))

Distinct variable groups:   𝐵,𝑎,𝑒   + ,𝑎,𝑒

Allowed substitution hints:   𝐺(𝑒,𝑎)

Proof of Theorem ismnddef

Dummy variables 𝑏 𝑔 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvex 6342	. . 3 ⊢ (Base‘𝑔) ∈ V
2		fvex 6342	. . 3 ⊢ (+g‘𝑔) ∈ V
3		fveq2 6332	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺))
4		ismnddef.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
5	3, 4	syl6eqr 2823	. . . . . 6 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝐵)
6	5	eqeq2d 2781	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑏 = (Base‘𝑔) ↔ 𝑏 = 𝐵))
7		fveq2 6332	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (+g‘𝑔) = (+g‘𝐺))
8		ismnddef.p	. . . . . . 7 ⊢ + = (+g‘𝐺)
9	7, 8	syl6eqr 2823	. . . . . 6 ⊢ (𝑔 = 𝐺 → (+g‘𝑔) = + )
10	9	eqeq2d 2781	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑝 = (+g‘𝑔) ↔ 𝑝 = + ))
11	6, 10	anbi12d 616	. . . 4 ⊢ (𝑔 = 𝐺 → ((𝑏 = (Base‘𝑔) ∧ 𝑝 = (+g‘𝑔)) ↔ (𝑏 = 𝐵 ∧ 𝑝 = + )))
12		simpl 468	. . . . 5 ⊢ ((𝑏 = 𝐵 ∧ 𝑝 = + ) → 𝑏 = 𝐵)
13		oveq 6799	. . . . . . . . 9 ⊢ (𝑝 = + → (𝑒𝑝𝑎) = (𝑒 + 𝑎))
14	13	eqeq1d 2773	. . . . . . . 8 ⊢ (𝑝 = + → ((𝑒𝑝𝑎) = 𝑎 ↔ (𝑒 + 𝑎) = 𝑎))
15		oveq 6799	. . . . . . . . 9 ⊢ (𝑝 = + → (𝑎𝑝𝑒) = (𝑎 + 𝑒))
16	15	eqeq1d 2773	. . . . . . . 8 ⊢ (𝑝 = + → ((𝑎𝑝𝑒) = 𝑎 ↔ (𝑎 + 𝑒) = 𝑎))
17	14, 16	anbi12d 616	. . . . . . 7 ⊢ (𝑝 = + → (((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎) ↔ ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎)))
18	17	adantl 467	. . . . . 6 ⊢ ((𝑏 = 𝐵 ∧ 𝑝 = + ) → (((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎) ↔ ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎)))
19	12, 18	raleqbidv 3301	. . . . 5 ⊢ ((𝑏 = 𝐵 ∧ 𝑝 = + ) → (∀𝑎 ∈ 𝑏 ((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎) ↔ ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎)))
20	12, 19	rexeqbidv 3302	. . . 4 ⊢ ((𝑏 = 𝐵 ∧ 𝑝 = + ) → (∃𝑒 ∈ 𝑏 ∀𝑎 ∈ 𝑏 ((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎) ↔ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎)))
21	11, 20	syl6bi 243	. . 3 ⊢ (𝑔 = 𝐺 → ((𝑏 = (Base‘𝑔) ∧ 𝑝 = (+g‘𝑔)) → (∃𝑒 ∈ 𝑏 ∀𝑎 ∈ 𝑏 ((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎) ↔ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎))))
22	1, 2, 21	sbc2iedv 3656	. 2 ⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑎 ∈ 𝑏 ((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎) ↔ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎)))
23		df-mnd 17503	. 2 ⊢ Mnd = {𝑔 ∈ SGrp ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑎 ∈ 𝑏 ((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎)}
24	22, 23	elrab2 3518	1 ⊢ (𝐺 ∈ Mnd ↔ (𝐺 ∈ SGrp ∧ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎)))

Syntax hints:   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145  ∀wral 3061  ∃wrex 3062  [wsbc 3587  ‘cfv 6031  (class class class)co 6793  Basecbs 16064  +_gcplusg 16149  SGrpcsgrp 17491  Mndcmnd 17502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4923

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039  df-ov 6796  df-mnd 17503

This theorem is referenced by:  ismnd  17505  isnmnd  17506  mndsgrp  17507  mnd1  17539  isringrng  42409  2zrngamnd  42469