![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ismgm | Structured version Visualization version GIF version |
Description: The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
Ref | Expression |
---|---|
ismgm.b | ⊢ 𝐵 = (Base‘𝑀) |
ismgm.o | ⊢ ⚬ = (+g‘𝑀) |
Ref | Expression |
---|---|
ismgm | ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvexd 6854 | . . 3 ⊢ (𝑚 = 𝑀 → (Base‘𝑚) ∈ V) | |
2 | fveq2 6839 | . . . 4 ⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀)) | |
3 | ismgm.b | . . . 4 ⊢ 𝐵 = (Base‘𝑀) | |
4 | 2, 3 | eqtr4di 2795 | . . 3 ⊢ (𝑚 = 𝑀 → (Base‘𝑚) = 𝐵) |
5 | fvexd 6854 | . . . 4 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑚) ∈ V) | |
6 | fveq2 6839 | . . . . . 6 ⊢ (𝑚 = 𝑀 → (+g‘𝑚) = (+g‘𝑀)) | |
7 | 6 | adantr 481 | . . . . 5 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑚) = (+g‘𝑀)) |
8 | ismgm.o | . . . . 5 ⊢ ⚬ = (+g‘𝑀) | |
9 | 7, 8 | eqtr4di 2795 | . . . 4 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑚) = ⚬ ) |
10 | simplr 767 | . . . . 5 ⊢ (((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → 𝑏 = 𝐵) | |
11 | oveq 7357 | . . . . . . . 8 ⊢ (𝑜 = ⚬ → (𝑥𝑜𝑦) = (𝑥 ⚬ 𝑦)) | |
12 | 11 | adantl 482 | . . . . . . 7 ⊢ (((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (𝑥𝑜𝑦) = (𝑥 ⚬ 𝑦)) |
13 | 12, 10 | eleq12d 2832 | . . . . . 6 ⊢ (((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → ((𝑥𝑜𝑦) ∈ 𝑏 ↔ (𝑥 ⚬ 𝑦) ∈ 𝐵)) |
14 | 10, 13 | raleqbidv 3317 | . . . . 5 ⊢ (((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏 ↔ ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵)) |
15 | 10, 14 | raleqbidv 3317 | . . . 4 ⊢ (((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵)) |
16 | 5, 9, 15 | sbcied2 3784 | . . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ([(+g‘𝑚) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵)) |
17 | 1, 4, 16 | sbcied2 3784 | . 2 ⊢ (𝑚 = 𝑀 → ([(Base‘𝑚) / 𝑏][(+g‘𝑚) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵)) |
18 | df-mgm 18457 | . 2 ⊢ Mgm = {𝑚 ∣ [(Base‘𝑚) / 𝑏][(+g‘𝑚) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏} | |
19 | 17, 18 | elab2g 3630 | 1 ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3062 Vcvv 3443 [wsbc 3737 ‘cfv 6493 (class class class)co 7351 Basecbs 17043 +gcplusg 17093 Mgmcmgm 18455 |
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 2708 ax-nul 5261 |
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 2715 df-cleq 2729 df-clel 2815 df-ne 2942 df-ral 3063 df-rab 3406 df-v 3445 df-sbc 3738 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-iota 6445 df-fv 6501 df-ov 7354 df-mgm 18457 |
This theorem is referenced by: ismgmn0 18459 mgmcl 18460 issstrmgm 18468 mgm0 18471 issgrpv 18508 efmndmgm 18655 smndex1mgm 18677 0mgm 45969 ismgmd 45971 mgm2mgm 46062 lidlmmgm 46124 |
Copyright terms: Public domain | W3C validator |