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 No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
submefmnd.b B = Base M
submefmnd.0 0 ˙ = 0 M
submefmnd.c F = Base S
Assertion submefmnd A V S Mnd F B 0 ˙ F + S = f F , g F f g F SubMnd M

Proof

Step Hyp Ref Expression
1 submefmnd.g Could not format M = ( EndoFMnd ` A ) : No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
2 submefmnd.b B = Base M
3 submefmnd.0 0 ˙ = 0 M
4 submefmnd.c F = Base S
5 1 efmndmnd A V M Mnd
6 simpl1 S Mnd F B 0 ˙ F + S = f F , g F f g S Mnd
7 5 6 anim12i A V S Mnd F B 0 ˙ F + S = f F , g F f g M Mnd S Mnd
8 simpl2 S Mnd F B 0 ˙ F + S = f F , g F f g F B
9 simpl3 S Mnd F B 0 ˙ F + S = f F , g F f g 0 ˙ F
10 simpr S Mnd F B 0 ˙ F + S = f F , g F f g + S = f F , g F f g
11 resmpo F B F B f B , g B f g F × F = f F , g F f g
12 11 anidms F B f B , g B f g F × F = f F , g F f g
13 eqid + M = + M
14 1 2 13 efmndplusg + M = f B , g B f g
15 14 eqcomi f B , g B f g = + M
16 15 reseq1i f B , g B f g F × F = + M F × F
17 12 16 eqtr3di F B f F , g F f g = + M F × F
18 17 3ad2ant2 S Mnd F B 0 ˙ F f F , g F f g = + M F × F
19 18 adantr S Mnd F B 0 ˙ F + S = f F , g F f g f F , g F f g = + M F × F
20 10 19 eqtrd S Mnd F B 0 ˙ F + S = f F , g F f g + S = + M F × F
21 8 9 20 3jca S Mnd F B 0 ˙ F + S = f F , g F f g F B 0 ˙ F + S = + M F × F
22 21 adantl A V S Mnd F B 0 ˙ F + S = f F , g F f g F B 0 ˙ F + S = + M F × F
23 2 4 3 mndissubm M Mnd S Mnd F B 0 ˙ F + S = + M F × F F SubMnd M
24 7 22 23 sylc A V S Mnd F B 0 ˙ F + S = f F , g F f g F SubMnd M
25 24 ex A V S Mnd F B 0 ˙ F + S = f F , g F f g F SubMnd M