Metamath Proof Explorer


Theorem idresefmnd

Description: The structure with the singleton containing only the identity function restricted to a set A as base set and the function composition as group operation, constructed by (structure) restricting the monoid of endofunctions on A to that singleton, is a monoid whose base set is a subset of the base set of the monoid of endofunctions on A . (Contributed by AV, 17-Feb-2024)

Ref Expression
Hypotheses idressubmefmnd.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
idresefmnd.e 𝐸 = ( 𝐺s { ( I ↾ 𝐴 ) } )
Assertion idresefmnd ( 𝐴𝑉 → ( 𝐸 ∈ Mnd ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 idressubmefmnd.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 idresefmnd.e 𝐸 = ( 𝐺s { ( I ↾ 𝐴 ) } )
3 1 idressubmefmnd ( 𝐴𝑉 → { ( I ↾ 𝐴 ) } ∈ ( SubMnd ‘ 𝐺 ) )
4 1 efmndmnd ( 𝐴𝑉𝐺 ∈ Mnd )
5 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 eqid ( 0g𝐺 ) = ( 0g𝐺 )
7 eqid ( 𝐺s { ( I ↾ 𝐴 ) } ) = ( 𝐺s { ( I ↾ 𝐴 ) } )
8 5 6 7 issubm2 ( 𝐺 ∈ Mnd → ( { ( I ↾ 𝐴 ) } ∈ ( SubMnd ‘ 𝐺 ) ↔ ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g𝐺 ) ∈ { ( I ↾ 𝐴 ) } ∧ ( 𝐺s { ( I ↾ 𝐴 ) } ) ∈ Mnd ) ) )
9 4 8 syl ( 𝐴𝑉 → ( { ( I ↾ 𝐴 ) } ∈ ( SubMnd ‘ 𝐺 ) ↔ ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g𝐺 ) ∈ { ( I ↾ 𝐴 ) } ∧ ( 𝐺s { ( I ↾ 𝐴 ) } ) ∈ Mnd ) ) )
10 snex { ( I ↾ 𝐴 ) } ∈ V
11 2 5 ressbas ( { ( I ↾ 𝐴 ) } ∈ V → ( { ( I ↾ 𝐴 ) } ∩ ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐸 ) )
12 10 11 mp1i ( 𝐴𝑉 → ( { ( I ↾ 𝐴 ) } ∩ ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐸 ) )
13 inss2 ( { ( I ↾ 𝐴 ) } ∩ ( Base ‘ 𝐺 ) ) ⊆ ( Base ‘ 𝐺 )
14 12 13 eqsstrrdi ( 𝐴𝑉 → ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) )
15 2 eqcomi ( 𝐺s { ( I ↾ 𝐴 ) } ) = 𝐸
16 15 eleq1i ( ( 𝐺s { ( I ↾ 𝐴 ) } ) ∈ Mnd ↔ 𝐸 ∈ Mnd )
17 16 biimpi ( ( 𝐺s { ( I ↾ 𝐴 ) } ) ∈ Mnd → 𝐸 ∈ Mnd )
18 17 3ad2ant3 ( ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g𝐺 ) ∈ { ( I ↾ 𝐴 ) } ∧ ( 𝐺s { ( I ↾ 𝐴 ) } ) ∈ Mnd ) → 𝐸 ∈ Mnd )
19 14 18 anim12ci ( ( 𝐴𝑉 ∧ ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g𝐺 ) ∈ { ( I ↾ 𝐴 ) } ∧ ( 𝐺s { ( I ↾ 𝐴 ) } ) ∈ Mnd ) ) → ( 𝐸 ∈ Mnd ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) )
20 19 ex ( 𝐴𝑉 → ( ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g𝐺 ) ∈ { ( I ↾ 𝐴 ) } ∧ ( 𝐺s { ( I ↾ 𝐴 ) } ) ∈ Mnd ) → ( 𝐸 ∈ Mnd ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) ) )
21 9 20 sylbid ( 𝐴𝑉 → ( { ( I ↾ 𝐴 ) } ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐸 ∈ Mnd ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) ) )
22 3 21 mpd ( 𝐴𝑉 → ( 𝐸 ∈ Mnd ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) )