![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mgmcl | Structured version Visualization version GIF version |
Description: Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.) |
Ref | Expression |
---|---|
mgmcl.b | ⊢ 𝐵 = (Base‘𝑀) |
mgmcl.o | ⊢ ⚬ = (+g‘𝑀) |
Ref | Expression |
---|---|
mgmcl | ⊢ ((𝑀 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mgmcl.b | . . . . 5 ⊢ 𝐵 = (Base‘𝑀) | |
2 | mgmcl.o | . . . . 5 ⊢ ⚬ = (+g‘𝑀) | |
3 | 1, 2 | ismgm 17596 | . . . 4 ⊢ (𝑀 ∈ Mgm → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵)) |
4 | 3 | ibi 259 | . . 3 ⊢ (𝑀 ∈ Mgm → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵) |
5 | ovrspc2v 6931 | . . . 4 ⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵) | |
6 | 5 | expcom 404 | . . 3 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵 → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵)) |
7 | 4, 6 | syl 17 | . 2 ⊢ (𝑀 ∈ Mgm → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵)) |
8 | 7 | 3impib 1150 | 1 ⊢ ((𝑀 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1113 = wceq 1658 ∈ wcel 2166 ∀wral 3117 ‘cfv 6123 (class class class)co 6905 Basecbs 16222 +gcplusg 16305 Mgmcmgm 17593 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-nul 5013 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-sbc 3663 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-iota 6086 df-fv 6131 df-ov 6908 df-mgm 17595 |
This theorem is referenced by: isnmgm 17599 mgmplusf 17604 issstrmgm 17605 gsummgmpropd 17628 mndcl 17654 dfgrp2 17801 dfgrp3e 17869 mulgnncl 17910 mulgnndir 17922 mgmhmf1o 42634 idmgmhm 42635 issubmgm2 42637 rabsubmgmd 42638 mgmhmco 42648 mgmhmeql 42650 submgmacs 42651 mgmplusgiopALT 42677 rngcl 42730 c0mgm 42756 c0snmgmhm 42761 |
Copyright terms: Public domain | W3C validator |