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	1 2	symgbasmap	$⊢ f \in B \to f \in (A^{A})$
10	9	ssriv	$⊢ B \subseteq A^{A}$
11		sstr	$⊢ (F \subseteq B \land B \subseteq A^{A}) \to F \subseteq A^{A}$
12	10 11	mpan2	$⊢ F \subseteq B \to F \subseteq A^{A}$
13		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)$
14	13	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)$
15	12 14	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)$
16		eqid	$⊢ A^{A} = A^{A}$
17		eqid	$⊢ +_{G} = +_{G}$
18	1 16 17	symgplusg	$⊢ +_{G} = (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g)$
19	18	eqcomi	$⊢ (f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g) = +_{G}$
20	19	reseq1i	$⊢ {(f \in (A^{A}), g \in (A^{A}) ⟼ f \circ g) ↾}_{(F \times F)} = {+_{G} ↾}_{(F \times F)}$
21	15 20	eqtr3di	$⊢ 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