Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mndissubm | Structured version Visualization version GIF version |
Description: If the base set of a monoid is contained in the base set of another monoid, and the group operation of the monoid is the restriction of the group operation of the other monoid to its base set, and the identity element of the the other monoid is contained in the base set of the monoid, then the (base set of the) monoid is a submonoid of the other monoid. Analogous to grpissubg 18417. (Contributed by AV, 17-Feb-2024.) |
Ref | Expression |
---|---|
mndissubm.b | ⊢ 𝐵 = (Base‘𝐺) |
mndissubm.s | ⊢ 𝑆 = (Base‘𝐻) |
mndissubm.z | ⊢ 0 = (0g‘𝐺) |
Ref | Expression |
---|---|
mndissubm | ⊢ ((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) → ((𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ∈ (SubMnd‘𝐺))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr1 1195 | . . 3 ⊢ (((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → 𝑆 ⊆ 𝐵) | |
2 | simpr2 1196 | . . 3 ⊢ (((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → 0 ∈ 𝑆) | |
3 | mndmgm 18034 | . . . . . . 7 ⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Mgm) | |
4 | mndmgm 18034 | . . . . . . 7 ⊢ (𝐻 ∈ Mnd → 𝐻 ∈ Mgm) | |
5 | 3, 4 | anim12i 616 | . . . . . 6 ⊢ ((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) → (𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm)) |
6 | 5 | ad2antrr 726 | . . . . 5 ⊢ ((((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm)) |
7 | 3simpb 1150 | . . . . . 6 ⊢ ((𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) | |
8 | 7 | ad2antlr 727 | . . . . 5 ⊢ ((((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) |
9 | simpr 488 | . . . . 5 ⊢ ((((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) | |
10 | mndissubm.b | . . . . . 6 ⊢ 𝐵 = (Base‘𝐺) | |
11 | mndissubm.s | . . . . . 6 ⊢ 𝑆 = (Base‘𝐻) | |
12 | 10, 11 | mgmsscl 17973 | . . . . 5 ⊢ (((𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎(+g‘𝐺)𝑏) ∈ 𝑆) |
13 | 6, 8, 9, 12 | syl3anc 1372 | . . . 4 ⊢ ((((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎(+g‘𝐺)𝑏) ∈ 𝑆) |
14 | 13 | ralrimivva 3103 | . . 3 ⊢ (((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → ∀𝑎 ∈ 𝑆 ∀𝑏 ∈ 𝑆 (𝑎(+g‘𝐺)𝑏) ∈ 𝑆) |
15 | mndissubm.z | . . . . 5 ⊢ 0 = (0g‘𝐺) | |
16 | eqid 2738 | . . . . 5 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
17 | 10, 15, 16 | issubm 18084 | . . . 4 ⊢ (𝐺 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝑆 ∀𝑏 ∈ 𝑆 (𝑎(+g‘𝐺)𝑏) ∈ 𝑆))) |
18 | 17 | ad2antrr 726 | . . 3 ⊢ (((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → (𝑆 ∈ (SubMnd‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝑆 ∀𝑏 ∈ 𝑆 (𝑎(+g‘𝐺)𝑏) ∈ 𝑆))) |
19 | 1, 2, 14, 18 | mpbir3and 1343 | . 2 ⊢ (((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → 𝑆 ∈ (SubMnd‘𝐺)) |
20 | 19 | ex 416 | 1 ⊢ ((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) → ((𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ∈ (SubMnd‘𝐺))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ∈ wcel 2114 ∀wral 3053 ⊆ wss 3843 × cxp 5523 ↾ cres 5527 ‘cfv 6339 (class class class)co 7170 Basecbs 16586 +gcplusg 16668 0gc0g 16816 Mgmcmgm 17966 Mndcmnd 18027 SubMndcsubmnd 18071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3400 df-sbc 3681 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-op 4523 df-uni 4797 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5429 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-res 5537 df-iota 6297 df-fun 6341 df-fv 6347 df-ov 7173 df-mgm 17968 df-sgrp 18017 df-mnd 18028 df-submnd 18073 |
This theorem is referenced by: resmndismnd 18089 submefmnd 18176 |
Copyright terms: Public domain | W3C validator |