isnsg

Description: Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypotheses	isnsg.1	$⊢ X = {Base}_{G}$
	isnsg.2	$⊢ \underset{˙}{+} = +_{G}$
Assertion	isnsg	$⊢ S \in NrmSGrp (G) \leftrightarrow (S \in SubGrp (G) \land \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S))$

Proof

Step	Hyp	Ref	Expression
1		isnsg.1	$⊢ X = {Base}_{G}$
2		isnsg.2	$⊢ \underset{˙}{+} = +_{G}$
3		df-nsg	$⊢ NrmSGrp = (g \in Grp ⟼ \{s \in SubGrp (g) \| \underset{˙}{[} {Base}_{g} / b \underset{˙}{]} \underset{˙}{[} +_{g} / p \underset{˙}{]} \forall x \in b \forall y \in b (x p y \in s \leftrightarrow y p x \in s)\})$
4	3	mptrcl	$⊢ S \in NrmSGrp (G) \to G \in Grp$
5		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
6	5	adantr	$⊢ (S \in SubGrp (G) \land \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S)) \to G \in Grp$
7		fveq2	$⊢ g = G \to SubGrp (g) = SubGrp (G)$
8		fvexd	$⊢ g = G \to {Base}_{g} \in V$
9		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
10	9 1	eqtr4di	$⊢ g = G \to {Base}_{g} = X$
11		fvexd	$⊢ (g = G \land b = X) \to +_{g} \in V$
12		simpl	$⊢ (g = G \land b = X) \to g = G$
13	12	fveq2d	$⊢ (g = G \land b = X) \to +_{g} = +_{G}$
14	13 2	eqtr4di	$⊢ (g = G \land b = X) \to +_{g} = \underset{˙}{+}$
15		simplr	$⊢ ((g = G \land b = X) \land p = \underset{˙}{+}) \to b = X$
16		simpr	$⊢ ((g = G \land b = X) \land p = \underset{˙}{+}) \to p = \underset{˙}{+}$
17	16	oveqd	$⊢ ((g = G \land b = X) \land p = \underset{˙}{+}) \to x p y = x \underset{˙}{+} y$
18	17	eleq1d	$⊢ ((g = G \land b = X) \land p = \underset{˙}{+}) \to (x p y \in s \leftrightarrow x \underset{˙}{+} y \in s)$
19	16	oveqd	$⊢ ((g = G \land b = X) \land p = \underset{˙}{+}) \to y p x = y \underset{˙}{+} x$
20	19	eleq1d	$⊢ ((g = G \land b = X) \land p = \underset{˙}{+}) \to (y p x \in s \leftrightarrow y \underset{˙}{+} x \in s)$
21	18 20	bibi12d	$⊢ ((g = G \land b = X) \land p = \underset{˙}{+}) \to ((x p y \in s \leftrightarrow y p x \in s) \leftrightarrow (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s))$
22	15 21	raleqbidv	$⊢ ((g = G \land b = X) \land p = \underset{˙}{+}) \to (\forall y \in b (x p y \in s \leftrightarrow y p x \in s) \leftrightarrow \forall y \in X (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s))$
23	15 22	raleqbidv	$⊢ ((g = G \land b = X) \land p = \underset{˙}{+}) \to (\forall x \in b \forall y \in b (x p y \in s \leftrightarrow y p x \in s) \leftrightarrow \forall x \in X \forall y \in X (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s))$
24	11 14 23	sbcied2	$⊢ (g = G \land b = X) \to (\underset{˙}{[} +_{g} / p \underset{˙}{]} \forall x \in b \forall y \in b (x p y \in s \leftrightarrow y p x \in s) \leftrightarrow \forall x \in X \forall y \in X (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s))$
25	8 10 24	sbcied2	$⊢ g = G \to (\underset{˙}{[} {Base}_{g} / b \underset{˙}{]} \underset{˙}{[} +_{g} / p \underset{˙}{]} \forall x \in b \forall y \in b (x p y \in s \leftrightarrow y p x \in s) \leftrightarrow \forall x \in X \forall y \in X (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s))$
26	7 25	rabeqbidv	$⊢ g = G \to \{s \in SubGrp (g) \| \underset{˙}{[} {Base}_{g} / b \underset{˙}{]} \underset{˙}{[} +_{g} / p \underset{˙}{]} \forall x \in b \forall y \in b (x p y \in s \leftrightarrow y p x \in s)\} = \{s \in SubGrp (G) \| \forall x \in X \forall y \in X (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s)\}$
27		fvex	$⊢ SubGrp (G) \in V$
28	27	rabex	$⊢ \{s \in SubGrp (G) \| \forall x \in X \forall y \in X (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s)\} \in V$
29	26 3 28	fvmpt	$⊢ G \in Grp \to NrmSGrp (G) = \{s \in SubGrp (G) \| \forall x \in X \forall y \in X (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s)\}$
30	29	eleq2d	$⊢ G \in Grp \to (S \in NrmSGrp (G) \leftrightarrow S \in \{s \in SubGrp (G) \| \forall x \in X \forall y \in X (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s)\})$
31		eleq2	$⊢ s = S \to (x \underset{˙}{+} y \in s \leftrightarrow x \underset{˙}{+} y \in S)$
32		eleq2	$⊢ s = S \to (y \underset{˙}{+} x \in s \leftrightarrow y \underset{˙}{+} x \in S)$
33	31 32	bibi12d	$⊢ s = S \to ((x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s) \leftrightarrow (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S))$
34	33	2ralbidv	$⊢ s = S \to (\forall x \in X \forall y \in X (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s) \leftrightarrow \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S))$
35	34	elrab	$⊢ S \in \{s \in SubGrp (G) \| \forall x \in X \forall y \in X (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s)\} \leftrightarrow (S \in SubGrp (G) \land \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S))$
36	30 35	bitrdi	$⊢ G \in Grp \to (S \in NrmSGrp (G) \leftrightarrow (S \in SubGrp (G) \land \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S)))$
37	4 6 36	pm5.21nii	$⊢ S \in NrmSGrp (G) \leftrightarrow (S \in SubGrp (G) \land \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S))$

Metamath Proof Explorer

Theorem isnsg

Proof