conjnmzb

Description: Alternative condition for elementhood in the 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	conjnmzb	$⊢ S \in SubGrp (G) \to (A \in N \leftrightarrow (A \in X \land 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	5	ssrab3	$⊢ N \subseteq X$
7		simpr	$⊢ (S \in SubGrp (G) \land A \in N) \to A \in N$
8	6 7	sseldi	$⊢ (S \in SubGrp (G) \land A \in N) \to A \in X$
9	1 2 3 4 5	conjnmz	$⊢ (S \in SubGrp (G) \land A \in N) \to S = ran F$
10	8 9	jca	$⊢ (S \in SubGrp (G) \land A \in N) \to (A \in X \land S = ran F)$
11		simprl	$⊢ (S \in SubGrp (G) \land (A \in X \land S = ran F)) \to A \in X$
12		simplrr	$⊢ ((S \in SubGrp (G) \land (A \in X \land S = ran F)) \land w \in X) \to S = ran F$
13	12	eleq2d	$⊢ ((S \in SubGrp (G) \land (A \in X \land S = ran F)) \land w \in X) \to (A \underset{˙}{+} w \in S \leftrightarrow A \underset{˙}{+} w \in ran F)$
14		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
15	14	ad3antrrr	$⊢ (((S \in SubGrp (G) \land A \in X) \land w \in X) \land x \in S) \to G \in Grp$
16		simpllr	$⊢ (((S \in SubGrp (G) \land A \in X) \land w \in X) \land x \in S) \to A \in X$
17	1	subgss	$⊢ S \in SubGrp (G) \to S \subseteq X$
18	17	ad2antrr	$⊢ ((S \in SubGrp (G) \land A \in X) \land w \in X) \to S \subseteq X$
19	18	sselda	$⊢ (((S \in SubGrp (G) \land A \in X) \land w \in X) \land x \in S) \to x \in X$
20	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)$
21	15 16 19 16 20	syl13anc	$⊢ (((S \in SubGrp (G) \land A \in X) \land w \in X) \land x \in S) \to (A \underset{˙}{+} x) \underset{˙}{-} A = A \underset{˙}{+} (x \underset{˙}{-} A)$
22	21	eqeq1d	$⊢ (((S \in SubGrp (G) \land A \in X) \land w \in X) \land x \in S) \to ((A \underset{˙}{+} x) \underset{˙}{-} A = A \underset{˙}{+} w \leftrightarrow A \underset{˙}{+} (x \underset{˙}{-} A) = A \underset{˙}{+} w)$
23	1 3	grpsubcl	$⊢ (G \in Grp \land x \in X \land A \in X) \to x \underset{˙}{-} A \in X$
24	15 19 16 23	syl3anc	$⊢ (((S \in SubGrp (G) \land A \in X) \land w \in X) \land x \in S) \to x \underset{˙}{-} A \in X$
25		simplr	$⊢ (((S \in SubGrp (G) \land A \in X) \land w \in X) \land x \in S) \to w \in X$
26	1 2	grplcan	$⊢ (G \in Grp \land (x \underset{˙}{-} A \in X \land w \in X \land A \in X)) \to (A \underset{˙}{+} (x \underset{˙}{-} A) = A \underset{˙}{+} w \leftrightarrow x \underset{˙}{-} A = w)$
27	15 24 25 16 26	syl13anc	$⊢ (((S \in SubGrp (G) \land A \in X) \land w \in X) \land x \in S) \to (A \underset{˙}{+} (x \underset{˙}{-} A) = A \underset{˙}{+} w \leftrightarrow x \underset{˙}{-} A = w)$
28	1 2 3	grpsubadd	$⊢ (G \in Grp \land (x \in X \land A \in X \land w \in X)) \to (x \underset{˙}{-} A = w \leftrightarrow w \underset{˙}{+} A = x)$
29	15 19 16 25 28	syl13anc	$⊢ (((S \in SubGrp (G) \land A \in X) \land w \in X) \land x \in S) \to (x \underset{˙}{-} A = w \leftrightarrow w \underset{˙}{+} A = x)$
30	22 27 29	3bitrd	$⊢ (((S \in SubGrp (G) \land A \in X) \land w \in X) \land x \in S) \to ((A \underset{˙}{+} x) \underset{˙}{-} A = A \underset{˙}{+} w \leftrightarrow w \underset{˙}{+} A = x)$
31		eqcom	$⊢ A \underset{˙}{+} w = (A \underset{˙}{+} x) \underset{˙}{-} A \leftrightarrow (A \underset{˙}{+} x) \underset{˙}{-} A = A \underset{˙}{+} w$
32		eqcom	$⊢ x = w \underset{˙}{+} A \leftrightarrow w \underset{˙}{+} A = x$
33	30 31 32	3bitr4g	$⊢ (((S \in SubGrp (G) \land A \in X) \land w \in X) \land x \in S) \to (A \underset{˙}{+} w = (A \underset{˙}{+} x) \underset{˙}{-} A \leftrightarrow x = w \underset{˙}{+} A)$
34	33	rexbidva	$⊢ ((S \in SubGrp (G) \land A \in X) \land w \in X) \to (\exists x \in S A \underset{˙}{+} w = (A \underset{˙}{+} x) \underset{˙}{-} A \leftrightarrow \exists x \in S x = w \underset{˙}{+} A)$
35	34	adantlrr	$⊢ ((S \in SubGrp (G) \land (A \in X \land S = ran F)) \land w \in X) \to (\exists x \in S A \underset{˙}{+} w = (A \underset{˙}{+} x) \underset{˙}{-} A \leftrightarrow \exists x \in S x = w \underset{˙}{+} A)$
36		ovex	$⊢ A \underset{˙}{+} w \in V$
37		eqeq1	$⊢ y = A \underset{˙}{+} w \to (y = (A \underset{˙}{+} x) \underset{˙}{-} A \leftrightarrow A \underset{˙}{+} w = (A \underset{˙}{+} x) \underset{˙}{-} A)$
38	37	rexbidv	$⊢ y = A \underset{˙}{+} w \to (\exists x \in S y = (A \underset{˙}{+} x) \underset{˙}{-} A \leftrightarrow \exists x \in S A \underset{˙}{+} w = (A \underset{˙}{+} x) \underset{˙}{-} A)$
39	4	rnmpt	$⊢ ran F = \{y \| \exists x \in S y = (A \underset{˙}{+} x) \underset{˙}{-} A\}$
40	36 38 39	elab2	$⊢ A \underset{˙}{+} w \in ran F \leftrightarrow \exists x \in S A \underset{˙}{+} w = (A \underset{˙}{+} x) \underset{˙}{-} A$
41		risset	$⊢ w \underset{˙}{+} A \in S \leftrightarrow \exists x \in S x = w \underset{˙}{+} A$
42	35 40 41	3bitr4g	$⊢ ((S \in SubGrp (G) \land (A \in X \land S = ran F)) \land w \in X) \to (A \underset{˙}{+} w \in ran F \leftrightarrow w \underset{˙}{+} A \in S)$
43	13 42	bitrd	$⊢ ((S \in SubGrp (G) \land (A \in X \land S = ran F)) \land w \in X) \to (A \underset{˙}{+} w \in S \leftrightarrow w \underset{˙}{+} A \in S)$
44	43	ralrimiva	$⊢ (S \in SubGrp (G) \land (A \in X \land S = ran F)) \to \forall w \in X (A \underset{˙}{+} w \in S \leftrightarrow w \underset{˙}{+} A \in S)$
45	5	elnmz	$⊢ A \in N \leftrightarrow (A \in X \land \forall w \in X (A \underset{˙}{+} w \in S \leftrightarrow w \underset{˙}{+} A \in S))$
46	11 44 45	sylanbrc	$⊢ (S \in SubGrp (G) \land (A \in X \land S = ran F)) \to A \in N$
47	10 46	impbida	$⊢ S \in SubGrp (G) \to (A \in N \leftrightarrow (A \in X \land S = ran F))$

Metamath Proof Explorer

Theorem conjnmzb

Proof