symgsssg

Description: The symmetric group has subgroups restricting the set of non-fixed points. (Contributed by Stefan O'Rear, 24-Aug-2015)

	Ref	Expression
Hypotheses	symgsssg.g	$⊢ G = SymGrp (D)$
	symgsssg.b	$⊢ B = {Base}_{G}$
Assertion	symgsssg	$⊢ D \in V \to \{x \in B \| dom (x ∖ I) \subseteq X\} \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) \subseteq X\} = G ↾_{𝑠} \{x \in B \| dom (x ∖ I) \subseteq X\}$
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) \subseteq X\} \subseteq B$
7	6 2	sseqtri	$⊢ \{x \in B \| dom (x ∖ I) \subseteq X\} \subseteq {Base}_{G}$
8	7	a1i	$⊢ D \in V \to \{x \in B \| dom (x ∖ I) \subseteq X\} \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	sseq1d	$⊢ x = 0_{G} \to (dom (x ∖ I) \subseteq X \leftrightarrow dom (0_{G} ∖ I) \subseteq X)$
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		0ss	$⊢ \emptyset \subseteq X$
26	24 25	eqsstri	$⊢ dom (({I ↾}_{D}) ∖ I) \subseteq X$
27	18 26	eqsstrrdi	$⊢ D \in V \to dom (0_{G} ∖ I) \subseteq X$
28	11 15 27	elrabd	$⊢ D \in V \to 0_{G} \in \{x \in B \| dom (x ∖ I) \subseteq X\}$
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	sseq1d	$⊢ x = y \to (dom (x ∖ I) \subseteq X \leftrightarrow dom (y ∖ I) \subseteq X)$
33	32	elrab	$⊢ y \in \{x \in B \| dom (x ∖ I) \subseteq X\} \leftrightarrow (y \in B \land dom (y ∖ I) \subseteq X)$
34		difeq1	$⊢ x = z \to x ∖ I = z ∖ I$
35	34	dmeqd	$⊢ x = z \to dom (x ∖ I) = dom (z ∖ I)$
36	35	sseq1d	$⊢ x = z \to (dom (x ∖ I) \subseteq X \leftrightarrow dom (z ∖ I) \subseteq X)$
37	36	elrab	$⊢ z \in \{x \in B \| dom (x ∖ I) \subseteq X\} \leftrightarrow (z \in B \land dom (z ∖ I) \subseteq X)$
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	sseq1d	$⊢ x = y +_{G} z \to (dom (x ∖ I) \subseteq X \leftrightarrow dom ((y +_{G} z) ∖ I) \subseteq X)$
41	12	3ad2ant1	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \to G \in Grp$
42		simp2l	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \to y \in B$
43		simp3l	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \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) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \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) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \to y +_{G} z = y \circ z$
49	48	difeq1d	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \to (y +_{G} z) ∖ I = (y \circ z) ∖ I$
50	49	dmeqd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \to dom ((y +_{G} z) ∖ I) = dom ((y \circ z) ∖ I)$
51		mvdco	$⊢ dom ((y \circ z) ∖ I) \subseteq dom (y ∖ I) \cup dom (z ∖ I)$
52		simp2r	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \to dom (y ∖ I) \subseteq X$
53		simp3r	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \to dom (z ∖ I) \subseteq X$
54	52 53	unssd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \to dom (y ∖ I) \cup dom (z ∖ I) \subseteq X$
55	51 54	sstrid	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \to dom ((y \circ z) ∖ I) \subseteq X$
56	50 55	eqsstrd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \to dom ((y +_{G} z) ∖ I) \subseteq X$
57	40 46 56	elrabd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X) \land (z \in B \land dom (z ∖ I) \subseteq X)) \to y +_{G} z \in \{x \in B \| dom (x ∖ I) \subseteq X\}$
58	29 33 37 57	syl3anb	$⊢ (D \in V \land y \in \{x \in B \| dom (x ∖ I) \subseteq X\} \land z \in \{x \in B \| dom (x ∖ I) \subseteq X\}) \to y +_{G} z \in \{x \in B \| dom (x ∖ I) \subseteq X\}$
59		difeq1	$⊢ x = {inv}_{g} (G) (y) \to x ∖ I = {inv}_{g} (G) (y) ∖ I$
60	59	dmeqd	$⊢ x = {inv}_{g} (G) (y) \to dom (x ∖ I) = dom ({inv}_{g} (G) (y) ∖ I)$
61	60	sseq1d	$⊢ x = {inv}_{g} (G) (y) \to (dom (x ∖ I) \subseteq X \leftrightarrow dom ({inv}_{g} (G) (y) ∖ I) \subseteq X)$
62		simprl	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X)) \to y \in B$
63		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
64	2 63	grpinvcl	$⊢ (G \in Grp \land y \in B) \to {inv}_{g} (G) (y) \in B$
65	12 62 64	syl2an2r	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X)) \to {inv}_{g} (G) (y) \in B$
66	1 2 63	symginv	$⊢ y \in B \to {inv}_{g} (G) (y) = y^{-1}$
67	66	ad2antrl	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X)) \to {inv}_{g} (G) (y) = y^{-1}$
68	67	difeq1d	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X)) \to {inv}_{g} (G) (y) ∖ I = y^{-1} ∖ I$
69	68	dmeqd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X)) \to dom ({inv}_{g} (G) (y) ∖ I) = dom (y^{-1} ∖ I)$
70	1 2	symgbasf1o	$⊢ y \in B \to y : D \underset{1-1 onto}{⟶} D$
71	70	ad2antrl	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X)) \to y : D \underset{1-1 onto}{⟶} D$
72		f1omvdcnv	$⊢ y : D \underset{1-1 onto}{⟶} D \to dom (y^{-1} ∖ I) = dom (y ∖ I)$
73	71 72	syl	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X)) \to dom (y^{-1} ∖ I) = dom (y ∖ I)$
74	69 73	eqtrd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X)) \to dom ({inv}_{g} (G) (y) ∖ I) = dom (y ∖ I)$
75		simprr	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X)) \to dom (y ∖ I) \subseteq X$
76	74 75	eqsstrd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X)) \to dom ({inv}_{g} (G) (y) ∖ I) \subseteq X$
77	61 65 76	elrabd	$⊢ (D \in V \land (y \in B \land dom (y ∖ I) \subseteq X)) \to {inv}_{g} (G) (y) \in \{x \in B \| dom (x ∖ I) \subseteq X\}$
78	33 77	sylan2b	$⊢ (D \in V \land y \in \{x \in B \| dom (x ∖ I) \subseteq X\}) \to {inv}_{g} (G) (y) \in \{x \in B \| dom (x ∖ I) \subseteq X\}$
79	3 4 5 8 28 58 78 12	issubgrpd2	$⊢ D \in V \to \{x \in B \| dom (x ∖ I) \subseteq X\} \in SubGrp (G)$

Metamath Proof Explorer

Theorem symgsssg

Proof