Metamath Proof Explorer

Theorem pgrpsubgsymg

Description: Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019) (Revised by AV, 30-Mar-2024)

Ref Expression
Hypotheses pgrpsubgsymgbi.g ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
pgrpsubgsymgbi.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
pgrpsubgsymg.c ⊢ 𝐹 = ( Base ‘ 𝑃 )
Assertion pgrpsubgsymg ( 𝐴 ∈ 𝑉 → ( ( 𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 𝐹 ∈ ( SubGrp ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 pgrpsubgsymgbi.g ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2 pgrpsubgsymgbi.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 pgrpsubgsymg.c ⊢ 𝐹 = ( Base ‘ 𝑃 )
4 1 symggrp ⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Grp )
5 simp1 ⊢ ( ( 𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 𝑃 ∈ Grp )
6 4 5 anim12i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) ) → ( 𝐺 ∈ Grp ∧ 𝑃 ∈ Grp ) )
7 simp2 ⊢ ( ( 𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 𝐹 ⊆ 𝐵 )
8 simp3 ⊢ ( ( 𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) )
9 1 2 symgbasmap ⊢ ( 𝑓 ∈ 𝐵 → 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) )
10 9 ssriv ⊢ 𝐵 ⊆ ( 𝐴 ↑m 𝐴 )
11 sstr ⊢ ( ( 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ ( 𝐴 ↑m 𝐴 ) ) → 𝐹 ⊆ ( 𝐴 ↑m 𝐴 ) )
12 10 11 mpan2 ⊢ ( 𝐹 ⊆ 𝐵 → 𝐹 ⊆ ( 𝐴 ↑m 𝐴 ) )
13 resmpo ⊢ ( ( 𝐹 ⊆ ( 𝐴 ↑m 𝐴 ) ∧ 𝐹 ⊆ ( 𝐴 ↑m 𝐴 ) ) → ( ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) )
14 13 anidms ⊢ ( 𝐹 ⊆ ( 𝐴 ↑m 𝐴 ) → ( ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) )
15 12 14 syl ⊢ ( 𝐹 ⊆ 𝐵 → ( ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) )
16 eqid ⊢ ( 𝐴 ↑m 𝐴 ) = ( 𝐴 ↑m 𝐴 )
17 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
18 1 16 17 symgplusg ⊢ ( +g ‘ 𝐺 ) = ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) )
19 18 eqcomi ⊢ ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) = ( +g ‘ 𝐺 )
20 19 reseq1i ⊢ ( ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝐹 × 𝐹 ) )
21 15 20 eqtr3di ⊢ ( 𝐹 ⊆ 𝐵 → ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝐹 × 𝐹 ) ) )
22 21 3ad2ant2 ⊢ ( ( 𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝐹 × 𝐹 ) ) )
23 8 22 eqtrd ⊢ ( ( 𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → ( +g ‘ 𝑃 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝐹 × 𝐹 ) ) )
24 7 23 jca ⊢ ( ( 𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → ( 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝐹 × 𝐹 ) ) ) )
25 24 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) ) → ( 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝐹 × 𝐹 ) ) ) )
26 2 3 grpissubg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ Grp ) → ( ( 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝐹 × 𝐹 ) ) ) → 𝐹 ∈ ( SubGrp ‘ 𝐺 ) ) )
27 6 25 26 sylc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) ) → 𝐹 ∈ ( SubGrp ‘ 𝐺 ) )
28 27 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 𝐹 ∈ ( SubGrp ‘ 𝐺 ) ) )