isnsg2

Description: Weaken the condition of isnsg to only one side of the implication. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypotheses	isnsg.1	$⊢ X = {Base}_{G}$
	isnsg.2	$⊢ \underset{˙}{+} = +_{G}$
Assertion	isnsg2	$⊢ S \in NrmSGrp (G) \leftrightarrow (S \in SubGrp (G) \land \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \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 z \in X (x \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} x \in S))$
4		dfbi2	$⊢ (x \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} x \in S) \leftrightarrow ((x \underset{˙}{+} z \in S \to z \underset{˙}{+} x \in S) \land (z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S))$
5	4	ralbii	$⊢ \forall z \in X (x \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} x \in S) \leftrightarrow \forall z \in X ((x \underset{˙}{+} z \in S \to z \underset{˙}{+} x \in S) \land (z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S))$
6	5	ralbii	$⊢ \forall x \in X \forall z \in X (x \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} x \in S) \leftrightarrow \forall x \in X \forall z \in X ((x \underset{˙}{+} z \in S \to z \underset{˙}{+} x \in S) \land (z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S))$
7		r19.26-2	$⊢ \forall x \in X \forall z \in X ((x \underset{˙}{+} z \in S \to z \underset{˙}{+} x \in S) \land (z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S)) \leftrightarrow (\forall x \in X \forall z \in X (x \underset{˙}{+} z \in S \to z \underset{˙}{+} x \in S) \land \forall x \in X \forall z \in X (z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S))$
8	6 7	bitri	$⊢ \forall x \in X \forall z \in X (x \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} x \in S) \leftrightarrow (\forall x \in X \forall z \in X (x \underset{˙}{+} z \in S \to z \underset{˙}{+} x \in S) \land \forall x \in X \forall z \in X (z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S))$
9		oveq2	$⊢ z = y \to x \underset{˙}{+} z = x \underset{˙}{+} y$
10	9	eleq1d	$⊢ z = y \to (x \underset{˙}{+} z \in S \leftrightarrow x \underset{˙}{+} y \in S)$
11		oveq1	$⊢ z = y \to z \underset{˙}{+} x = y \underset{˙}{+} x$
12	11	eleq1d	$⊢ z = y \to (z \underset{˙}{+} x \in S \leftrightarrow y \underset{˙}{+} x \in S)$
13	10 12	imbi12d	$⊢ z = y \to ((x \underset{˙}{+} z \in S \to z \underset{˙}{+} x \in S) \leftrightarrow (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S))$
14	13	cbvralvw	$⊢ \forall z \in X (x \underset{˙}{+} z \in S \to z \underset{˙}{+} x \in S) \leftrightarrow \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S)$
15	14	ralbii	$⊢ \forall x \in X \forall z \in X (x \underset{˙}{+} z \in S \to z \underset{˙}{+} x \in S) \leftrightarrow \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S)$
16		ralcom	$⊢ \forall x \in X \forall z \in X (z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S) \leftrightarrow \forall z \in X \forall x \in X (z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S)$
17		oveq2	$⊢ x = y \to z \underset{˙}{+} x = z \underset{˙}{+} y$
18	17	eleq1d	$⊢ x = y \to (z \underset{˙}{+} x \in S \leftrightarrow z \underset{˙}{+} y \in S)$
19		oveq1	$⊢ x = y \to x \underset{˙}{+} z = y \underset{˙}{+} z$
20	19	eleq1d	$⊢ x = y \to (x \underset{˙}{+} z \in S \leftrightarrow y \underset{˙}{+} z \in S)$
21	18 20	imbi12d	$⊢ x = y \to ((z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S) \leftrightarrow (z \underset{˙}{+} y \in S \to y \underset{˙}{+} z \in S))$
22	21	cbvralvw	$⊢ \forall x \in X (z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S) \leftrightarrow \forall y \in X (z \underset{˙}{+} y \in S \to y \underset{˙}{+} z \in S)$
23	22	ralbii	$⊢ \forall z \in X \forall x \in X (z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S) \leftrightarrow \forall z \in X \forall y \in X (z \underset{˙}{+} y \in S \to y \underset{˙}{+} z \in S)$
24		oveq1	$⊢ z = x \to z \underset{˙}{+} y = x \underset{˙}{+} y$
25	24	eleq1d	$⊢ z = x \to (z \underset{˙}{+} y \in S \leftrightarrow x \underset{˙}{+} y \in S)$
26		oveq2	$⊢ z = x \to y \underset{˙}{+} z = y \underset{˙}{+} x$
27	26	eleq1d	$⊢ z = x \to (y \underset{˙}{+} z \in S \leftrightarrow y \underset{˙}{+} x \in S)$
28	25 27	imbi12d	$⊢ z = x \to ((z \underset{˙}{+} y \in S \to y \underset{˙}{+} z \in S) \leftrightarrow (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S))$
29	28	ralbidv	$⊢ z = x \to (\forall y \in X (z \underset{˙}{+} y \in S \to y \underset{˙}{+} z \in S) \leftrightarrow \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S))$
30	29	cbvralvw	$⊢ \forall z \in X \forall y \in X (z \underset{˙}{+} y \in S \to y \underset{˙}{+} z \in S) \leftrightarrow \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S)$
31	16 23 30	3bitri	$⊢ \forall x \in X \forall z \in X (z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S) \leftrightarrow \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S)$
32	15 31	anbi12i	$⊢ (\forall x \in X \forall z \in X (x \underset{˙}{+} z \in S \to z \underset{˙}{+} x \in S) \land \forall x \in X \forall z \in X (z \underset{˙}{+} x \in S \to x \underset{˙}{+} z \in S)) \leftrightarrow (\forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S) \land \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S))$
33		anidm	$⊢ (\forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S) \land \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S)) \leftrightarrow \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S)$
34	8 32 33	3bitri	$⊢ \forall x \in X \forall z \in X (x \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} x \in S) \leftrightarrow \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S)$
35	34	anbi2i	$⊢ (S \in SubGrp (G) \land \forall x \in X \forall z \in X (x \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} x \in S)) \leftrightarrow (S \in SubGrp (G) \land \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S))$
36	3 35	bitri	$⊢ S \in NrmSGrp (G) \leftrightarrow (S \in SubGrp (G) \land \forall x \in X \forall y \in X (x \underset{˙}{+} y \in S \to y \underset{˙}{+} x \in S))$

Metamath Proof Explorer

Theorem isnsg2

Proof