This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem symgsubmefmndALT

Description: The symmetric group on a set A is a submonoid of the monoid of endofunctions on A . Alternate proof based on issubmndb and not on injsubmefmnd and sursubmefmnd . (Contributed by AV, 18-Feb-2024) (Revised by AV, 30-Mar-2024) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses symgsubmefmndALT.m ⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
symgsubmefmndALT.g ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
symgsubmefmndALT.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion symgsubmefmndALT ( 𝐴 ∈ 𝑉 → 𝐵 ∈ ( SubMnd ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 symgsubmefmndALT.m ⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
2 symgsubmefmndALT.g ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
3 symgsubmefmndALT.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 1 efmndmnd ⊢ ( 𝐴 ∈ 𝑉 → 𝑀 ∈ Mnd )
5 2 3 1 symgressbas ⊢ 𝐺 = ( 𝑀 ↾s 𝐵 )
6 2 symggrp ⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Grp )
7 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
8 6 7 syl ⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd )
9 5 8 eqeltrrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑀 ↾s 𝐵 ) ∈ Mnd )
10 2 idresperm ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) )
11 1 efmndid ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) = ( 0g ‘ 𝑀 ) )
12 3 eqcomi ⊢ ( Base ‘ 𝐺 ) = 𝐵
13 12 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ 𝐺 ) = 𝐵 )
14 10 11 13 3eltr3d ⊢ ( 𝐴 ∈ 𝑉 → ( 0g ‘ 𝑀 ) ∈ 𝐵 )
15 2 3 symgbasmap ⊢ ( 𝑓 ∈ 𝐵 → 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) )
16 15 ssriv ⊢ 𝐵 ⊆ ( 𝐴 ↑m 𝐴 )
17 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
18 1 17 efmndbas ⊢ ( Base ‘ 𝑀 ) = ( 𝐴 ↑m 𝐴 )
19 16 18 sseqtrri ⊢ 𝐵 ⊆ ( Base ‘ 𝑀 )
20 14 19 jctil ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ) )
21 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
22 17 21 issubmndb ⊢ ( 𝐵 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( ( 𝑀 ∈ Mnd ∧ ( 𝑀 ↾s 𝐵 ) ∈ Mnd ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ) ) )
23 4 9 20 22 syl21anbrc ⊢ ( 𝐴 ∈ 𝑉 → 𝐵 ∈ ( SubMnd ‘ 𝑀 ) )