Metamath Proof Explorer


Theorem resmndismnd

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 other monoid restricted to the base set of the monoid is a monoid. Analogous to resgrpisgrp . (Contributed by AV, 17-Feb-2024)

Ref Expression
Hypotheses mndissubm.b 𝐵 = ( Base ‘ 𝐺 )
mndissubm.s 𝑆 = ( Base ‘ 𝐻 )
mndissubm.z 0 = ( 0g𝐺 )
Assertion resmndismnd ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) → ( ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( 𝐺s 𝑆 ) ∈ Mnd ) )

Proof

Step Hyp Ref Expression
1 mndissubm.b 𝐵 = ( Base ‘ 𝐺 )
2 mndissubm.s 𝑆 = ( Base ‘ 𝐻 )
3 mndissubm.z 0 = ( 0g𝐺 )
4 1 2 3 mndissubm ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) → ( ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) )
5 4 imp ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
6 simpl ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) → 𝐺 ∈ Mnd )
7 3simpa ( ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( 𝑆𝐵0𝑆 ) )
8 6 7 anim12i ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝐺 ∈ Mnd ∧ ( 𝑆𝐵0𝑆 ) ) )
9 8 biantrud ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( ( 𝐺s 𝑆 ) ∈ Mnd ↔ ( ( 𝐺s 𝑆 ) ∈ Mnd ∧ ( 𝐺 ∈ Mnd ∧ ( 𝑆𝐵0𝑆 ) ) ) ) )
10 an21 ( ( ( 𝐺 ∈ Mnd ∧ ( 𝐺s 𝑆 ) ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ) ) ↔ ( ( 𝐺s 𝑆 ) ∈ Mnd ∧ ( 𝐺 ∈ Mnd ∧ ( 𝑆𝐵0𝑆 ) ) ) )
11 9 10 bitr4di ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( ( 𝐺s 𝑆 ) ∈ Mnd ↔ ( ( 𝐺 ∈ Mnd ∧ ( 𝐺s 𝑆 ) ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ) ) ) )
12 1 3 issubmndb ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( ( 𝐺 ∈ Mnd ∧ ( 𝐺s 𝑆 ) ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ) ) )
13 11 12 bitr4di ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( ( 𝐺s 𝑆 ) ∈ Mnd ↔ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) )
14 5 13 mpbird ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝐺s 𝑆 ) ∈ Mnd )
15 14 ex ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) → ( ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( 𝐺s 𝑆 ) ∈ Mnd ) )