conjnmz

Description: A subgroup is unchanged under conjugation by an element of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypotheses	conjghm.x	$⊢ X = {Base}_{G}$
	conjghm.p	$⊢ \underset{˙}{+} = +_{G}$
	conjghm.m	$⊢ \underset{˙}{-} = -_{G}$
	conjsubg.f	$⊢ F = (x \in S ⟼ (A \underset{˙}{+} x) \underset{˙}{-} A)$
	conjnmz.1	$⊢ N = \{y \in X \| \forall z \in X (y \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} y \in S)\}$
Assertion	conjnmz	$⊢ (S \in SubGrp (G) \land A \in N) \to S = ran F$

Proof

Step	Hyp	Ref	Expression
1		conjghm.x	$⊢ X = {Base}_{G}$
2		conjghm.p	$⊢ \underset{˙}{+} = +_{G}$
3		conjghm.m	$⊢ \underset{˙}{-} = -_{G}$
4		conjsubg.f	$⊢ F = (x \in S ⟼ (A \underset{˙}{+} x) \underset{˙}{-} A)$
5		conjnmz.1	$⊢ N = \{y \in X \| \forall z \in X (y \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} y \in S)\}$
6		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
7	6	ad2antrr	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to G \in Grp$
8		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
9	5	ssrab3	$⊢ N \subseteq X$
10		simplr	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to A \in N$
11	9 10	sselid	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to A \in X$
12	1 8 7 11	grpinvcld	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to {inv}_{g} (G) (A) \in X$
13	1	subgss	$⊢ S \in SubGrp (G) \to S \subseteq X$
14	13	adantr	$⊢ (S \in SubGrp (G) \land A \in N) \to S \subseteq X$
15	14	sselda	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to w \in X$
16	1 2 7 12 15 11	grpassd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to ({inv}_{g} (G) (A) \underset{˙}{+} w) \underset{˙}{+} A = {inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A)$
17		eqid	$⊢ 0_{G} = 0_{G}$
18	1 2 17 8 7 11	grprinvd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to A \underset{˙}{+} {inv}_{g} (G) (A) = 0_{G}$
19	18	oveq1d	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to (A \underset{˙}{+} {inv}_{g} (G) (A)) \underset{˙}{+} w = 0_{G} \underset{˙}{+} w$
20	1 2 7 11 12 15	grpassd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to (A \underset{˙}{+} {inv}_{g} (G) (A)) \underset{˙}{+} w = A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} w)$
21	1 2 17 7 15	grplidd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to 0_{G} \underset{˙}{+} w = w$
22	19 20 21	3eqtr3d	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} w) = w$
23		simpr	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to w \in S$
24	22 23	eqeltrd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} w) \in S$
25	1 2 7 12 15	grpcld	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to {inv}_{g} (G) (A) \underset{˙}{+} w \in X$
26	5	nmzbi	$⊢ (A \in N \land {inv}_{g} (G) (A) \underset{˙}{+} w \in X) \to (A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} w) \in S \leftrightarrow ({inv}_{g} (G) (A) \underset{˙}{+} w) \underset{˙}{+} A \in S)$
27	10 25 26	syl2anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to (A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} w) \in S \leftrightarrow ({inv}_{g} (G) (A) \underset{˙}{+} w) \underset{˙}{+} A \in S)$
28	24 27	mpbid	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to ({inv}_{g} (G) (A) \underset{˙}{+} w) \underset{˙}{+} A \in S$
29	16 28	eqeltrrd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to {inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A) \in S$
30		oveq2	$⊢ x = {inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A) \to A \underset{˙}{+} x = A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A))$
31	30	oveq1d	$⊢ x = {inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A) \to (A \underset{˙}{+} x) \underset{˙}{-} A = (A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A))) \underset{˙}{-} A$
32		ovex	$⊢ (A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A))) \underset{˙}{-} A \in V$
33	31 4 32	fvmpt	$⊢ {inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A) \in S \to F ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A)) = (A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A))) \underset{˙}{-} A$
34	29 33	syl	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to F ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A)) = (A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A))) \underset{˙}{-} A$
35	18	oveq1d	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to (A \underset{˙}{+} {inv}_{g} (G) (A)) \underset{˙}{+} (w \underset{˙}{+} A) = 0_{G} \underset{˙}{+} (w \underset{˙}{+} A)$
36	1 2 7 15 11	grpcld	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to w \underset{˙}{+} A \in X$
37	1 2 7 11 12 36	grpassd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to (A \underset{˙}{+} {inv}_{g} (G) (A)) \underset{˙}{+} (w \underset{˙}{+} A) = A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A))$
38	1 2 17 7 36	grplidd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to 0_{G} \underset{˙}{+} (w \underset{˙}{+} A) = w \underset{˙}{+} A$
39	35 37 38	3eqtr3d	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A)) = w \underset{˙}{+} A$
40	39	oveq1d	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to (A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A))) \underset{˙}{-} A = (w \underset{˙}{+} A) \underset{˙}{-} A$
41	1 2 3	grppncan	$⊢ (G \in Grp \land w \in X \land A \in X) \to (w \underset{˙}{+} A) \underset{˙}{-} A = w$
42	7 15 11 41	syl3anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to (w \underset{˙}{+} A) \underset{˙}{-} A = w$
43	34 40 42	3eqtrd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to F ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A)) = w$
44		ovex	$⊢ (A \underset{˙}{+} x) \underset{˙}{-} A \in V$
45	44 4	fnmpti	$⊢ F Fn S$
46		fnfvelrn	$⊢ (F Fn S \land {inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A) \in S) \to F ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A)) \in ran F$
47	45 29 46	sylancr	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to F ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A)) \in ran F$
48	43 47	eqeltrrd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to w \in ran F$
49	48	ex	$⊢ (S \in SubGrp (G) \land A \in N) \to (w \in S \to w \in ran F)$
50	49	ssrdv	$⊢ (S \in SubGrp (G) \land A \in N) \to S \subseteq ran F$
51	6	ad2antrr	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to G \in Grp$
52		simplr	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to A \in N$
53	9 52	sselid	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to A \in X$
54	14	sselda	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to x \in X$
55	1 2 3	grpaddsubass	$⊢ (G \in Grp \land (A \in X \land x \in X \land A \in X)) \to (A \underset{˙}{+} x) \underset{˙}{-} A = A \underset{˙}{+} (x \underset{˙}{-} A)$
56	51 53 54 53 55	syl13anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to (A \underset{˙}{+} x) \underset{˙}{-} A = A \underset{˙}{+} (x \underset{˙}{-} A)$
57	1 2 3	grpnpcan	$⊢ (G \in Grp \land x \in X \land A \in X) \to (x \underset{˙}{-} A) \underset{˙}{+} A = x$
58	51 54 53 57	syl3anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to (x \underset{˙}{-} A) \underset{˙}{+} A = x$
59		simpr	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to x \in S$
60	58 59	eqeltrd	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to (x \underset{˙}{-} A) \underset{˙}{+} A \in S$
61	1 3	grpsubcl	$⊢ (G \in Grp \land x \in X \land A \in X) \to x \underset{˙}{-} A \in X$
62	51 54 53 61	syl3anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to x \underset{˙}{-} A \in X$
63	5	nmzbi	$⊢ (A \in N \land x \underset{˙}{-} A \in X) \to (A \underset{˙}{+} (x \underset{˙}{-} A) \in S \leftrightarrow (x \underset{˙}{-} A) \underset{˙}{+} A \in S)$
64	52 62 63	syl2anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to (A \underset{˙}{+} (x \underset{˙}{-} A) \in S \leftrightarrow (x \underset{˙}{-} A) \underset{˙}{+} A \in S)$
65	60 64	mpbird	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to A \underset{˙}{+} (x \underset{˙}{-} A) \in S$
66	56 65	eqeltrd	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to (A \underset{˙}{+} x) \underset{˙}{-} A \in S$
67	66 4	fmptd	$⊢ (S \in SubGrp (G) \land A \in N) \to F : S ⟶ S$
68	67	frnd	$⊢ (S \in SubGrp (G) \land A \in N) \to ran F \subseteq S$
69	50 68	eqssd	$⊢ (S \in SubGrp (G) \land A \in N) \to S = ran F$

Metamath Proof Explorer

Theorem conjnmz

Proof