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	5	ssrab3	$⊢ N \subseteq X$
9		simplr	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to A \in N$
10	8 9	sselid	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to A \in X$
11		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
12	1 11	grpinvcl	$⊢ (G \in Grp \land A \in X) \to {inv}_{g} (G) (A) \in X$
13	7 10 12	syl2anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to {inv}_{g} (G) (A) \in X$
14	1	subgss	$⊢ S \in SubGrp (G) \to S \subseteq X$
15	14	adantr	$⊢ (S \in SubGrp (G) \land A \in N) \to S \subseteq X$
16	15	sselda	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to w \in X$
17	1 2	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (A) \in X \land w \in X \land A \in X)) \to ({inv}_{g} (G) (A) \underset{˙}{+} w) \underset{˙}{+} A = {inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A)$
18	7 13 16 10 17	syl13anc	$⊢ ((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)$
19		eqid	$⊢ 0_{G} = 0_{G}$
20	1 2 19 11	grprinv	$⊢ (G \in Grp \land A \in X) \to A \underset{˙}{+} {inv}_{g} (G) (A) = 0_{G}$
21	7 10 20	syl2anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to A \underset{˙}{+} {inv}_{g} (G) (A) = 0_{G}$
22	21	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$
23	1 2	grpass	$⊢ (G \in Grp \land (A \in X \land {inv}_{g} (G) (A) \in X \land w \in X)) \to (A \underset{˙}{+} {inv}_{g} (G) (A)) \underset{˙}{+} w = A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} w)$
24	7 10 13 16 23	syl13anc	$⊢ ((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)$
25	1 2 19	grplid	$⊢ (G \in Grp \land w \in X) \to 0_{G} \underset{˙}{+} w = w$
26	7 16 25	syl2anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to 0_{G} \underset{˙}{+} w = w$
27	22 24 26	3eqtr3d	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} w) = w$
28		simpr	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to w \in S$
29	27 28	eqeltrd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} w) \in S$
30	1 2	grpcl	$⊢ (G \in Grp \land {inv}_{g} (G) (A) \in X \land w \in X) \to {inv}_{g} (G) (A) \underset{˙}{+} w \in X$
31	7 13 16 30	syl3anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to {inv}_{g} (G) (A) \underset{˙}{+} w \in X$
32	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)$
33	9 31 32	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)$
34	29 33	mpbid	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to ({inv}_{g} (G) (A) \underset{˙}{+} w) \underset{˙}{+} A \in S$
35	18 34	eqeltrrd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to {inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A) \in S$
36		oveq2	$⊢ x = {inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A) \to A \underset{˙}{+} x = A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A))$
37	36	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$
38		ovex	$⊢ (A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A))) \underset{˙}{-} A \in V$
39	37 4 38	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$
40	35 39	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$
41	21	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)$
42	1 2	grpcl	$⊢ (G \in Grp \land w \in X \land A \in X) \to w \underset{˙}{+} A \in X$
43	7 16 10 42	syl3anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to w \underset{˙}{+} A \in X$
44	1 2	grpass	$⊢ (G \in Grp \land (A \in X \land {inv}_{g} (G) (A) \in X \land w \underset{˙}{+} A \in X)) \to (A \underset{˙}{+} {inv}_{g} (G) (A)) \underset{˙}{+} (w \underset{˙}{+} A) = A \underset{˙}{+} ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A))$
45	7 10 13 43 44	syl13anc	$⊢ ((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))$
46	1 2 19	grplid	$⊢ (G \in Grp \land w \underset{˙}{+} A \in X) \to 0_{G} \underset{˙}{+} (w \underset{˙}{+} A) = w \underset{˙}{+} A$
47	7 43 46	syl2anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to 0_{G} \underset{˙}{+} (w \underset{˙}{+} A) = w \underset{˙}{+} A$
48	41 45 47	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$
49	48	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$
50	1 2 3	grppncan	$⊢ (G \in Grp \land w \in X \land A \in X) \to (w \underset{˙}{+} A) \underset{˙}{-} A = w$
51	7 16 10 50	syl3anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to (w \underset{˙}{+} A) \underset{˙}{-} A = w$
52	40 49 51	3eqtrd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to F ({inv}_{g} (G) (A) \underset{˙}{+} (w \underset{˙}{+} A)) = w$
53		ovex	$⊢ (A \underset{˙}{+} x) \underset{˙}{-} A \in V$
54	53 4	fnmpti	$⊢ F Fn S$
55		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$
56	54 35 55	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$
57	52 56	eqeltrrd	$⊢ ((S \in SubGrp (G) \land A \in N) \land w \in S) \to w \in ran F$
58	57	ex	$⊢ (S \in SubGrp (G) \land A \in N) \to (w \in S \to w \in ran F)$
59	58	ssrdv	$⊢ (S \in SubGrp (G) \land A \in N) \to S \subseteq ran F$
60	6	ad2antrr	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to G \in Grp$
61		simplr	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to A \in N$
62	8 61	sselid	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to A \in X$
63	15	sselda	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to x \in X$
64	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)$
65	60 62 63 62 64	syl13anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to (A \underset{˙}{+} x) \underset{˙}{-} A = A \underset{˙}{+} (x \underset{˙}{-} A)$
66	1 2 3	grpnpcan	$⊢ (G \in Grp \land x \in X \land A \in X) \to (x \underset{˙}{-} A) \underset{˙}{+} A = x$
67	60 63 62 66	syl3anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to (x \underset{˙}{-} A) \underset{˙}{+} A = x$
68		simpr	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to x \in S$
69	67 68	eqeltrd	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to (x \underset{˙}{-} A) \underset{˙}{+} A \in S$
70	1 3	grpsubcl	$⊢ (G \in Grp \land x \in X \land A \in X) \to x \underset{˙}{-} A \in X$
71	60 63 62 70	syl3anc	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to x \underset{˙}{-} A \in X$
72	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)$
73	61 71 72	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)$
74	69 73	mpbird	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to A \underset{˙}{+} (x \underset{˙}{-} A) \in S$
75	65 74	eqeltrd	$⊢ ((S \in SubGrp (G) \land A \in N) \land x \in S) \to (A \underset{˙}{+} x) \underset{˙}{-} A \in S$
76	75 4	fmptd	$⊢ (S \in SubGrp (G) \land A \in N) \to F : S ⟶ S$
77	76	frnd	$⊢ (S \in SubGrp (G) \land A \in N) \to ran F \subseteq S$
78	59 77	eqssd	$⊢ (S \in SubGrp (G) \land A \in N) \to S = ran F$

Metamath Proof Explorer

Theorem conjnmz

Proof