Metamath Proof Explorer

Theorem submefmnd

Description: If the base set of a monoid is contained in the base set of the monoid of endofunctions on a set A , contains the identity function and has the function composition as group operation, then its base set is a submonoid of the monoid of endofunctions on set A . Analogous to pgrpsubgsymg . (Contributed by AV, 17-Feb-2024)

Ref Expression
Hypotheses submefmnd.g ⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
submefmnd.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
submefmnd.0 ⊢ 0 = ( 0g ‘ 𝑀 )
submefmnd.c ⊢ 𝐹 = ( Base ‘ 𝑆 )
Assertion submefmnd ( 𝐴 ∈ 𝑉 → ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 𝐹 ∈ ( SubMnd ‘ 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 submefmnd.g ⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
2 submefmnd.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
3 submefmnd.0 ⊢ 0 = ( 0g ‘ 𝑀 )
4 submefmnd.c ⊢ 𝐹 = ( Base ‘ 𝑆 )
5 1 efmndmnd ⊢ ( 𝐴 ∈ 𝑉 → 𝑀 ∈ Mnd )
6 simpl1 ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 𝑆 ∈ Mnd )
7 5 6 anim12i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) ) → ( 𝑀 ∈ Mnd ∧ 𝑆 ∈ Mnd ) )
8 simpl2 ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 𝐹 ⊆ 𝐵 )
9 simpl3 ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 0 ∈ 𝐹 )
10 simpr ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) )
11 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
12 1 2 11 efmndplusg ⊢ ( +g ‘ 𝑀 ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) )
13 12 eqcomi ⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( +g ‘ 𝑀 )
14 13 reseq1i ⊢ ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) )
15 resmpo ⊢ ( ( 𝐹 ⊆ 𝐵 ∧ 𝐹 ⊆ 𝐵 ) → ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) )
16 15 anidms ⊢ ( 𝐹 ⊆ 𝐵 → ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) )
17 14 16 syl5reqr ⊢ ( 𝐹 ⊆ 𝐵 → ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) )
18 17 3ad2ant2 ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) → ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) )
19 18 adantr ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) )
20 10 19 eqtrd ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → ( +g ‘ 𝑆 ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) )
21 8 9 20 3jca ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → ( 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ∧ ( +g ‘ 𝑆 ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) ) )
22 21 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) ) → ( 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ∧ ( +g ‘ 𝑆 ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) ) )
23 2 4 3 mndissubm ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( ( 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ∧ ( +g ‘ 𝑆 ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) ) → 𝐹 ∈ ( SubMnd ‘ 𝑀 ) ) )
24 7 22 23 sylc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) ) → 𝐹 ∈ ( SubMnd ‘ 𝑀 ) )
25 24 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 𝐹 ∈ ( SubMnd ‘ 𝑀 ) ) )