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 ‘ 𝐺 ) ) )