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 
|- M = ( EndoFMnd ` A )
submefmnd.b 
|- B = ( Base ` M )
submefmnd.0 
|- .0. = ( 0g ` M )
submefmnd.c 
|- F = ( Base ` S )
Assertion submefmnd 
|- ( A e. V -> ( ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) /\ ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> F e. ( SubMnd ` M ) ) )

Proof

Step Hyp Ref Expression
1 submefmnd.g 
 |-  M = ( EndoFMnd ` A )
2 submefmnd.b 
 |-  B = ( Base ` M )
3 submefmnd.0 
 |-  .0. = ( 0g ` M )
4 submefmnd.c 
 |-  F = ( Base ` S )
5 1 efmndmnd 
 |-  ( A e. V -> M e. Mnd )
6 simpl1 
 |-  ( ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) /\ ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> S e. Mnd )
7 5 6 anim12i 
 |-  ( ( A e. V /\ ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) /\ ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) ) ) -> ( M e. Mnd /\ S e. Mnd ) )
8 simpl2 
 |-  ( ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) /\ ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> F C_ B )
9 simpl3 
 |-  ( ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) /\ ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> .0. e. F )
10 simpr 
 |-  ( ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) /\ ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) )
11 resmpo 
 |-  ( ( F C_ B /\ F C_ B ) -> ( ( f e. B , g e. B |-> ( f o. g ) ) |` ( F X. F ) ) = ( f e. F , g e. F |-> ( f o. g ) ) )
12 11 anidms 
 |-  ( F C_ B -> ( ( f e. B , g e. B |-> ( f o. g ) ) |` ( F X. F ) ) = ( f e. F , g e. F |-> ( f o. g ) ) )
13 eqid 
 |-  ( +g ` M ) = ( +g ` M )
14 1 2 13 efmndplusg 
 |-  ( +g ` M ) = ( f e. B , g e. B |-> ( f o. g ) )
15 14 eqcomi 
 |-  ( f e. B , g e. B |-> ( f o. g ) ) = ( +g ` M )
16 15 reseq1i 
 |-  ( ( f e. B , g e. B |-> ( f o. g ) ) |` ( F X. F ) ) = ( ( +g ` M ) |` ( F X. F ) )
17 12 16 eqtr3di 
 |-  ( F C_ B -> ( f e. F , g e. F |-> ( f o. g ) ) = ( ( +g ` M ) |` ( F X. F ) ) )
18 17 3ad2ant2 
 |-  ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) -> ( f e. F , g e. F |-> ( f o. g ) ) = ( ( +g ` M ) |` ( F X. F ) ) )
19 18 adantr 
 |-  ( ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) /\ ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> ( f e. F , g e. F |-> ( f o. g ) ) = ( ( +g ` M ) |` ( F X. F ) ) )
20 10 19 eqtrd 
 |-  ( ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) /\ ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> ( +g ` S ) = ( ( +g ` M ) |` ( F X. F ) ) )
21 8 9 20 3jca 
 |-  ( ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) /\ ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> ( F C_ B /\ .0. e. F /\ ( +g ` S ) = ( ( +g ` M ) |` ( F X. F ) ) ) )
22 21 adantl 
 |-  ( ( A e. V /\ ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) /\ ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) ) ) -> ( F C_ B /\ .0. e. F /\ ( +g ` S ) = ( ( +g ` M ) |` ( F X. F ) ) ) )
23 2 4 3 mndissubm 
 |-  ( ( M e. Mnd /\ S e. Mnd ) -> ( ( F C_ B /\ .0. e. F /\ ( +g ` S ) = ( ( +g ` M ) |` ( F X. F ) ) ) -> F e. ( SubMnd ` M ) ) )
24 7 22 23 sylc 
 |-  ( ( A e. V /\ ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) /\ ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) ) ) -> F e. ( SubMnd ` M ) )
25 24 ex 
 |-  ( A e. V -> ( ( ( S e. Mnd /\ F C_ B /\ .0. e. F ) /\ ( +g ` S ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> F e. ( SubMnd ` M ) ) )