Metamath Proof Explorer


Theorem mndissubm

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 . (Contributed by AV, 17-Feb-2024)

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

Proof

Step Hyp Ref Expression
1 mndissubm.b 𝐵 = ( Base ‘ 𝐺 )
2 mndissubm.s 𝑆 = ( Base ‘ 𝐻 )
3 mndissubm.z 0 = ( 0g𝐺 )
4 simpr1 ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆𝐵 )
5 simpr2 ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 0𝑆 )
6 mndmgm ( 𝐺 ∈ Mnd → 𝐺 ∈ Mgm )
7 mndmgm ( 𝐻 ∈ Mnd → 𝐻 ∈ Mgm )
8 6 7 anim12i ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) → ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) )
9 8 ad2antrr ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑎𝑆𝑏𝑆 ) ) → ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) )
10 3simpb ( ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) )
11 10 ad2antlr ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑎𝑆𝑏𝑆 ) ) → ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) )
12 simpr ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑎𝑆𝑏𝑆 ) ) → ( 𝑎𝑆𝑏𝑆 ) )
13 1 2 mgmsscl ( ( ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ ( 𝑎𝑆𝑏𝑆 ) ) → ( 𝑎 ( +g𝐺 ) 𝑏 ) ∈ 𝑆 )
14 9 11 12 13 syl3anc ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑎𝑆𝑏𝑆 ) ) → ( 𝑎 ( +g𝐺 ) 𝑏 ) ∈ 𝑆 )
15 14 ralrimivva ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ∀ 𝑎𝑆𝑏𝑆 ( 𝑎 ( +g𝐺 ) 𝑏 ) ∈ 𝑆 )
16 eqid ( +g𝐺 ) = ( +g𝐺 )
17 1 3 16 issubm ( 𝐺 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝑆𝐵0𝑆 ∧ ∀ 𝑎𝑆𝑏𝑆 ( 𝑎 ( +g𝐺 ) 𝑏 ) ∈ 𝑆 ) ) )
18 17 ad2antrr ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝑆𝐵0𝑆 ∧ ∀ 𝑎𝑆𝑏𝑆 ( 𝑎 ( +g𝐺 ) 𝑏 ) ∈ 𝑆 ) ) )
19 4 5 15 18 mpbir3and ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
20 19 ex ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) → ( ( 𝑆𝐵0𝑆 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) )