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