This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nsgbi

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

		Ref	Expression
	Hypotheses	isnsg.1	$⊢ X = {Base}_{G}$
		isnsg.2	$⊢ \underset{˙}{+} = +_{G}$
	Assertion	nsgbi	$⊢ (S \in NrmSGrp (G) \land A \in X \land B \in X) \to (A \underset{˙}{+} B \in S \leftrightarrow B \underset{˙}{+} A \in S)$

Proof

Step	Hyp	Ref	Expression
1		isnsg.1	$⊢ X = {Base}_{G}$
2		isnsg.2	$⊢ \underset{˙}{+} = +_{G}$
3	1 2	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))$
4	3	simprbi	$⊢ S \in NrmSGrp (G) \to \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S)$
5		oveq1	$⊢ x = A \to x \underset{˙}{+} y = A \underset{˙}{+} y$
6	5	eleq1d	$⊢ x = A \to (x \underset{˙}{+} y \in S \leftrightarrow A \underset{˙}{+} y \in S)$
7		oveq2	$⊢ x = A \to y \underset{˙}{+} x = y \underset{˙}{+} A$
8	7	eleq1d	$⊢ x = A \to (y \underset{˙}{+} x \in S \leftrightarrow y \underset{˙}{+} A \in S)$
9	6 8	bibi12d	$⊢ x = A \to ((x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S) \leftrightarrow (A \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} A \in S))$
10		oveq2	$⊢ y = B \to A \underset{˙}{+} y = A \underset{˙}{+} B$
11	10	eleq1d	$⊢ y = B \to (A \underset{˙}{+} y \in S \leftrightarrow A \underset{˙}{+} B \in S)$
12		oveq1	$⊢ y = B \to y \underset{˙}{+} A = B \underset{˙}{+} A$
13	12	eleq1d	$⊢ y = B \to (y \underset{˙}{+} A \in S \leftrightarrow B \underset{˙}{+} A \in S)$
14	11 13	bibi12d	$⊢ y = B \to ((A \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} A \in S) \leftrightarrow (A \underset{˙}{+} B \in S \leftrightarrow B \underset{˙}{+} A \in S))$
15	9 14	rspc2v	$⊢ (A \in X \land B \in X) \to (\forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \leftrightarrow y \underset{˙}{+} x \in S) \to (A \underset{˙}{+} B \in S \leftrightarrow B \underset{˙}{+} A \in S))$
16	4 15	syl5com	$⊢ S \in NrmSGrp (G) \to ((A \in X \land B \in X) \to (A \underset{˙}{+} B \in S \leftrightarrow B \underset{˙}{+} A \in S))$
17	16	3impib	$⊢ (S \in NrmSGrp (G) \land A \in X \land B \in X) \to (A \underset{˙}{+} B \in S \leftrightarrow B \underset{˙}{+} A \in S)$