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	$⊢ G = SymGrp (A)$
	pgrpsubgsymgbi.b	$⊢ B = {Base}_{G}$
	pgrpsubgsymg.c	$⊢ F = {Base}_{P}$
Assertion	pgrpsubgsymg	$⊢ A \in V \to ((P \in Grp \land F \subseteq B \land +_{P} = (f \in F, g \in F ⟼ f \circ g)) \to F \in SubGrp (G))$

Proof

Step	Hyp	Ref	Expression
1		pgrpsubgsymgbi.g	$⊢ G = SymGrp (A)$
2		pgrpsubgsymgbi.b	$⊢ B = {Base}_{G}$
3		pgrpsubgsymg.c	$⊢ F = {Base}_{P}$
4	1	symggrp	$⊢ A \in V \to G \in Grp$
5		simp1	$⊢ (P \in Grp \land F \subseteq B \land +_{P} = (f \in F, g \in F ⟼ f \circ g)) \to P \in Grp$
6	4 5	anim12i	$⊢ (A \in V \land (P \in Grp \land F \subseteq B \land +_{P} = (f \in F, g \in F ⟼ f \circ g))) \to (G \in Grp \land P \in Grp)$
7		simp2	$⊢ (P \in Grp \land F \subseteq B \land +_{P} = (f \in F, g \in F ⟼ f \circ g)) \to F \subseteq B$
8		simp3	$⊢ (P \in Grp \land F \subseteq B \land +_{P} = (f \in F, g \in F ⟼ f \circ g)) \to +_{P} = (f \in F, g \in F ⟼ f \circ g)$
9		eqid	$⊢ A^{A} = A^{A}$
10		eqid	$⊢ +_{G} = +_{G}$
11	1 9 10	symgplusg	$⊢ +_{G} = (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g)$
12	11	eqcomi	$⊢ (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g) = +_{G}$
13	12	reseq1i	$⊢ {(f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g) ↾}_{(F \times F)} = {+_{G} ↾}_{(F \times F)}$
14	1 2	symgbasmap	$⊢ f \in B \to f \in (A^{A})$
15	14	ssriv	$⊢ B \subseteq A^{A}$
16		sstr	$⊢ (F \subseteq B \land B \subseteq A^{A}) \to F \subseteq A^{A}$
17	15 16	mpan2	$⊢ F \subseteq B \to F \subseteq A^{A}$
18		resmpo	$⊢ (F \subseteq A^{A} \land F \subseteq A^{A}) \to {(f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g) ↾}_{(F \times F)} = (f \in F, g \in F ⟼ f \circ g)$
19	18	anidms	$⊢ F \subseteq A^{A} \to {(f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g) ↾}_{(F \times F)} = (f \in F, g \in F ⟼ f \circ g)$
20	17 19	syl	$⊢ F \subseteq B \to {(f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g) ↾}_{(F \times F)} = (f \in F, g \in F ⟼ f \circ g)$
21	13 20	syl5reqr	$⊢ F \subseteq B \to (f \in F, g \in F ⟼ f \circ g) = {+_{G} ↾}_{(F \times F)}$
22	21	3ad2ant2	$⊢ (P \in Grp \land F \subseteq B \land +_{P} = (f \in F, g \in F ⟼ f \circ g)) \to (f \in F, g \in F ⟼ f \circ g) = {+_{G} ↾}_{(F \times F)}$
23	8 22	eqtrd	$⊢ (P \in Grp \land F \subseteq B \land +_{P} = (f \in F, g \in F ⟼ f \circ g)) \to +_{P} = {+_{G} ↾}_{(F \times F)}$
24	7 23	jca	$⊢ (P \in Grp \land F \subseteq B \land +_{P} = (f \in F, g \in F ⟼ f \circ g)) \to (F \subseteq B \land +_{P} = {+_{G} ↾}_{(F \times F)})$
25	24	adantl	$⊢ (A \in V \land (P \in Grp \land F \subseteq B \land +_{P} = (f \in F, g \in F ⟼ f \circ g))) \to (F \subseteq B \land +_{P} = {+_{G} ↾}_{(F \times F)})$
26	2 3	grpissubg	$⊢ (G \in Grp \land P \in Grp) \to ((F \subseteq B \land +_{P} = {+_{G} ↾}_{(F \times F)}) \to F \in SubGrp (G))$
27	6 25 26	sylc	$⊢ (A \in V \land (P \in Grp \land F \subseteq B \land +_{P} = (f \in F, g \in F ⟼ f \circ g))) \to F \in SubGrp (G)$
28	27	ex	$⊢ A \in V \to ((P \in Grp \land F \subseteq B \land +_{P} = (f \in F, g \in F ⟼ f \circ g)) \to F \in SubGrp (G))$

Metamath Proof Explorer

Theorem pgrpsubgsymg

Proof