symgfisg

Description: The symmetric group has a subgroup of permutations that move finitely many points. (Contributed by Stefan O'Rear, 24-Aug-2015)

	Ref	Expression
Hypotheses	symgsssg.g	$⊢ G = SymGrp (D)$
	symgsssg.b	$⊢ B = {Base}_{G}$
Assertion	symgfisg	$⊢ D \in V \to \{x \in B \| dom (x ∖ I) \in Fin\} \in SubGrp (G)$

Proof

Step	Hyp	Ref	Expression
1		symgsssg.g	$⊢ G = SymGrp (D)$
2		symgsssg.b	$⊢ B = {Base}_{G}$
3		eqidd	$⊢ D \in V \to G ↾_{𝑠} \{x \in B \| dom (x ∖ I) \in Fin\} = G ↾_{𝑠} \{x \in B \| dom (x ∖ I) \in Fin\}$
4		eqidd	$⊢ D \in V \to 0_{G} = 0_{G}$
5		eqidd	$⊢ D \in V \to +_{G} = +_{G}$
6		ssrab2	$⊢ \{x \in B \| dom (x ∖ I) \in Fin\} \subseteq B$
7	6 2	sseqtri	$⊢ \{x \in B \| dom (x ∖ I) \in Fin\} \subseteq {Base}_{G}$
8	7	a1i	$⊢ D \in V \to \{x \in B \| dom (x ∖ I) \in Fin\} \subseteq {Base}_{G}$
9		difeq1	$⊢ x = 0_{G} \to x ∖ I = 0_{G} ∖ I$
10	9	dmeqd	$⊢ x = 0_{G} \to dom (x ∖ I) = dom (0_{G} ∖ I)$
11	10	eleq1d	$⊢ x = 0_{G} \to (dom (x ∖ I) \in Fin \leftrightarrow dom (0_{G} ∖ I) \in Fin)$
12	1	symggrp	$⊢ D \in V \to G \in Grp$
13		eqid	$⊢ 0_{G} = 0_{G}$
14	2 13	grpidcl	$⊢ G \in Grp \to 0_{G} \in B$
15	12 14	syl	$⊢ D \in V \to 0_{G} \in B$
16	1	symgid	$⊢ D \in V \to {I ↾}_{D} = 0_{G}$
17	16	difeq1d	$⊢ D \in V \to ({I ↾}_{D}) ∖ I = 0_{G} ∖ I$
18	17	dmeqd	$⊢ D \in V \to dom (({I ↾}_{D}) ∖ I) = dom (0_{G} ∖ I)$
19		resss	$⊢ {I ↾}_{D} \subseteq I$
20		ssdif0	$⊢ {I ↾}_{D} \subseteq I \leftrightarrow ({I ↾}_{D}) ∖ I = \emptyset$
21	19 20	mpbi	$⊢ ({I ↾}_{D}) ∖ I = \emptyset$
22	21	dmeqi	$⊢ dom (({I ↾}_{D}) ∖ I) = dom \emptyset$
23		dm0	$⊢ dom \emptyset = \emptyset$
24	22 23	eqtri	$⊢ dom (({I ↾}_{D}) ∖ I) = \emptyset$
25		0fi	$⊢ \emptyset \in Fin$
26	24 25	eqeltri	$⊢ dom (({I ↾}_{D}) ∖ I) \in Fin$
27	18 26	eqeltrrdi	$⊢ D \in V \to dom (0_{G} ∖ I) \in Fin$
28	11 15 27	elrabd	$⊢ D \in V \to 0_{G} \in \{x \in B \| dom (x ∖ I) \in Fin\}$
29		biid	$⊢ D \in V \leftrightarrow D \in V$
30		difeq1	$⊢ x = y \to x ∖ I = y ∖ I$
31	30	dmeqd	$⊢ x = y \to dom (x ∖ I) = dom (y ∖ I)$
32	31	eleq1d	$⊢ x = y \to (dom (x ∖ I) \in Fin \leftrightarrow dom (y ∖ I) \in Fin)$
33	32	elrab	$⊢ y \in \{x \in B \| dom (x ∖ I) \in Fin\} \leftrightarrow (y \in B \land dom (y ∖ I) \in Fin)$
34		difeq1	$⊢ x = z \to x ∖ I = z ∖ I$
35	34	dmeqd	$⊢ x = z \to dom (x ∖ I) = dom (z ∖ I)$
36	35	eleq1d	$⊢ x = z \to (dom (x ∖ I) \in Fin \leftrightarrow dom (z ∖ I) \in Fin)$
37	36	elrab	$⊢ z \in \{x \in B \| dom (x ∖ I) \in Fin\} \leftrightarrow (z \in B \land dom (z ∖ I) \in Fin)$
38		difeq1	$⊢ x = y +_{G} z \to x ∖ I = (y +_{G} z) ∖ I$
39	38	dmeqd	$⊢ x = y +_{G} z \to dom (x ∖ I) = dom ((y +_{G} z) ∖ I)$
40	39	eleq1d	$⊢ x = y +_{G} z \to (dom (x ∖ I) \in Fin \leftrightarrow dom ((y +_{G} z) ∖ I) \in Fin)$
41	12	3ad2ant1	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to G \in Grp$
42		simp2l	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to y \in B$
43		simp3l	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to z \in B$
44		eqid	$⊢ +_{G} = +_{G}$
45	2 44	grpcl	$⊢ (G \in Grp \land y \in B \land z \in B) \to y +_{G} z \in B$
46	41 42 43 45	syl3anc	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to y +_{G} z \in B$
47	1 2 44	symgov	$⊢ (y \in B \land z \in B) \to y +_{G} z = y \circ z$
48	42 43 47	syl2anc	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to y +_{G} z = y \circ z$
49	48	difeq1d	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to (y +_{G} z) ∖ I = (y \circ z) ∖ I$
50	49	dmeqd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to dom ((y +_{G} z) ∖ I) = dom ((y \circ z) ∖ I)$
51		simp2r	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to dom (y ∖ I) \in Fin$
52		simp3r	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to dom (z ∖ I) \in Fin$
53		unfi	$⊢ (dom (y ∖ I) \in Fin \land dom (z ∖ I) \in Fin) \to dom (y ∖ I) \cup dom (z ∖ I) \in Fin$
54	51 52 53	syl2anc	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to dom (y ∖ I) \cup dom (z ∖ I) \in Fin$
55		mvdco	$⊢ dom ((y \circ z) ∖ I) \subseteq dom (y ∖ I) \cup dom (z ∖ I)$
56		ssfi	$⊢ (dom (y ∖ I) \cup dom (z ∖ I) \in Fin \land dom ((y \circ z) ∖ I) \subseteq dom (y ∖ I) \cup dom (z ∖ I)) \to dom ((y \circ z) ∖ I) \in Fin$
57	54 55 56	sylancl	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to dom ((y \circ z) ∖ I) \in Fin$
58	50 57	eqeltrd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to dom ((y +_{G} z) ∖ I) \in Fin$
59	40 46 58	elrabd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin) \land (z \in B \land dom (z ∖ I) \in Fin)) \to y +_{G} z \in \{x \in B \| dom (x ∖ I) \in Fin\}$
60	29 33 37 59	syl3anb	$⊢ (D \in V \land y \in \{x \in B \| dom (x ∖ I) \in Fin\} \land z \in \{x \in B \| dom (x ∖ I) \in Fin\}) \to y +_{G} z \in \{x \in B \| dom (x ∖ I) \in Fin\}$
61		difeq1	$⊢ x = {inv}_{g} (G) (y) \to x ∖ I = {inv}_{g} (G) (y) ∖ I$
62	61	dmeqd	$⊢ x = {inv}_{g} (G) (y) \to dom (x ∖ I) = dom ({inv}_{g} (G) (y) ∖ I)$
63	62	eleq1d	$⊢ x = {inv}_{g} (G) (y) \to (dom (x ∖ I) \in Fin \leftrightarrow dom ({inv}_{g} (G) (y) ∖ I) \in Fin)$
64		simprl	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin)) \to y \in B$
65		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
66	2 65	grpinvcl	$⊢ (G \in Grp \land y \in B) \to {inv}_{g} (G) (y) \in B$
67	12 64 66	syl2an2r	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin)) \to {inv}_{g} (G) (y) \in B$
68	1 2 65	symginv	$⊢ y \in B \to {inv}_{g} (G) (y) = y^{-1}$
69	68	ad2antrl	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin)) \to {inv}_{g} (G) (y) = y^{-1}$
70	69	difeq1d	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin)) \to {inv}_{g} (G) (y) ∖ I = y^{-1} ∖ I$
71	70	dmeqd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin)) \to dom ({inv}_{g} (G) (y) ∖ I) = dom (y^{-1} ∖ I)$
72	1 2	symgbasf1o	$⊢ y \in B \to y : D \underset{1-1 onto}{⟶} D$
73	72	ad2antrl	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin)) \to y : D \underset{1-1 onto}{⟶} D$
74		f1omvdcnv	$⊢ y : D \underset{1-1 onto}{⟶} D \to dom (y^{-1} ∖ I) = dom (y ∖ I)$
75	73 74	syl	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin)) \to dom (y^{-1} ∖ I) = dom (y ∖ I)$
76	71 75	eqtrd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin)) \to dom ({inv}_{g} (G) (y) ∖ I) = dom (y ∖ I)$
77		simprr	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin)) \to dom (y ∖ I) \in Fin$
78	76 77	eqeltrd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin)) \to dom ({inv}_{g} (G) (y) ∖ I) \in Fin$
79	63 67 78	elrabd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \in Fin)) \to {inv}_{g} (G) (y) \in \{x \in B \| dom (x ∖ I) \in Fin\}$
80	33 79	sylan2b	$⊢ (D \in V \land y \in \{x \in B \| dom (x ∖ I) \in Fin\}) \to {inv}_{g} (G) (y) \in \{x \in B \| dom (x ∖ I) \in Fin\}$
81	3 4 5 8 28 60 80 12	issubgrpd2	$⊢ D \in V \to \{x \in B \| dom (x ∖ I) \in Fin\} \in SubGrp (G)$

Metamath Proof Explorer

Theorem symgfisg

Proof