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 resmpo ( ( 𝐹𝐵𝐹𝐵 ) → ( ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( 𝑓𝐹 , 𝑔𝐹 ↦ ( 𝑓𝑔 ) ) )
12 11 anidms ( 𝐹𝐵 → ( ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( 𝑓𝐹 , 𝑔𝐹 ↦ ( 𝑓𝑔 ) ) )
13 eqid ( +g𝑀 ) = ( +g𝑀 )
14 1 2 13 efmndplusg ( +g𝑀 ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓𝑔 ) )
15 14 eqcomi ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓𝑔 ) ) = ( +g𝑀 )
16 15 reseq1i ( ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( ( +g𝑀 ) ↾ ( 𝐹 × 𝐹 ) )
17 12 16 eqtr3di ( 𝐹𝐵 → ( 𝑓𝐹 , 𝑔𝐹 ↦ ( 𝑓𝑔 ) ) = ( ( +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 ‘ 𝑀 ) ) )