Theorem ismgm 18817

Description: The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)

Hypotheses

Ref	Expression
ismgm.b	⊢ 𝐵 = (Base‘𝑀)
ismgm.o	⊢ ⚬ = (+g‘𝑀)

Assertion

Ref	Expression
ismgm	⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))

Distinct variable groups:   𝑥,𝐵,𝑦   𝑥,𝑀,𝑦   𝑥, ⚬ ,𝑦

Allowed substitution hints:   𝑉(𝑥, 𝑦)

Proof of Theorem ismgm

Dummy variables 𝑏 𝑚 𝑜 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvexd 6900	. . 3 ⊢ (𝑚 = 𝑀 → (Base‘𝑚) ∈ V)
2		fveq2 6885	. . . 4 ⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀))
3		ismgm.b	. . . 4 ⊢ 𝐵 = (Base‘𝑀)
4	2, 3	eqtr4di 2813	. . 3 ⊢ (𝑚 = 𝑀 → (Base‘𝑚) = 𝐵)
5		fvexd 6900	. . . 4 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑚) ∈ V)
6		fveq2 6885	. . . . . 6 ⊢ (𝑚 = 𝑀 → (+g‘𝑚) = (+g‘𝑀))
7	6	adantr 486	. . . . 5 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑚) = (+g‘𝑀))
8		ismgm.o	. . . . 5 ⊢ ⚬ = (+g‘𝑀)
9	7, 8	eqtr4di 2813	. . . 4 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑚) = ⚬ )
10		simplr 781	. . . . 5 ⊢ (((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → 𝑏 = 𝐵)
11		oveq 7426	. . . . . . . 8 ⊢ (𝑜 = ⚬ → (𝑥𝑜𝑦) = (𝑥 ⚬ 𝑦))
12	11	adantl 487	. . . . . . 7 ⊢ (((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (𝑥𝑜𝑦) = (𝑥 ⚬ 𝑦))
13	12, 10	eleq12d 2854	. . . . . 6 ⊢ (((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → ((𝑥𝑜𝑦) ∈ 𝑏 ↔ (𝑥 ⚬ 𝑦) ∈ 𝐵))
14	10, 13	raleqbidv 3334	. . . . 5 ⊢ (((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏 ↔ ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
15	10, 14	raleqbidv 3334	. . . 4 ⊢ (((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
16	5, 9, 15	sbcied2 3782	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ([(+g‘𝑚) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
17	1, 4, 16	sbcied2 3782	. 2 ⊢ (𝑚 = 𝑀 → ([(Base‘𝑚) / 𝑏][(+g‘𝑚) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
18		df-mgm 18816	. 2 ⊢ Mgm = {𝑚 ∣ [(Base‘𝑚) / 𝑏][(+g‘𝑚) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏}
19	17, 18	elab2g 3633	1 ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076  Vcvv 3450  [wsbc 3738  ‘cfv 6538  (class class class)co 7420  Basecbs 17387  +_gcplusg 17428  Mgmcmgm 18814

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-mgm 18816

This theorem is used by:  ismgmn0  18818  mgmcl  18819  ismgmd  18830  issstrmgm  18831  mgm0  18834  issgrpv  18910  efmndmgm  19081  smndex1mgm  19106  rnglidlmmgm  21533  0mgm  49263  mgm2mgm  49324