Theorem 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={\mathrm{Base}}_G$$
	isnsg.2	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	isnsg2	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\leftrightarrow \left(S\in \mathrm{SubGrp}\left(G\right)\wedge \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isnsg.1	$$⊢X={\mathrm{Base}}_G$$
2		isnsg.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3	1 2	isnsg	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\leftrightarrow \left(S\in \mathrm{SubGrp}\left(G\right)\wedge \forall x\in X\forall z\in X\left(x\underset{\dot{}}{+}z\in S\leftrightarrow z\underset{\dot{}}{+}x\in S\right)\right)$$
4		dfbi2	$$⊢\left(x\underset{\dot{}}{+}z\in S\leftrightarrow z\underset{\dot{}}{+}x\in S\right)\leftrightarrow \left(\left(x\underset{\dot{}}{+}z\in S\to z\underset{\dot{}}{+}x\in S\right)\wedge \left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)\right)$$
5	4	ralbii	$$⊢\forall z\in X\left(x\underset{\dot{}}{+}z\in S\leftrightarrow z\underset{\dot{}}{+}x\in S\right)\leftrightarrow \forall z\in X\left(\left(x\underset{\dot{}}{+}z\in S\to z\underset{\dot{}}{+}x\in S\right)\wedge \left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)\right)$$
6	5	ralbii	$$⊢\forall x\in X\forall z\in X\left(x\underset{\dot{}}{+}z\in S\leftrightarrow z\underset{\dot{}}{+}x\in S\right)\leftrightarrow \forall x\in X\forall z\in X\left(\left(x\underset{\dot{}}{+}z\in S\to z\underset{\dot{}}{+}x\in S\right)\wedge \left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)\right)$$
7		r19.26-2	$$⊢\forall x\in X\forall z\in X\left(\left(x\underset{\dot{}}{+}z\in S\to z\underset{\dot{}}{+}x\in S\right)\wedge \left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)\right)\leftrightarrow \left(\forall x\in X\forall z\in X\left(x\underset{\dot{}}{+}z\in S\to z\underset{\dot{}}{+}x\in S\right)\wedge \forall x\in X\forall z\in X\left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)\right)$$
8	6 7	bitri	$$⊢\forall x\in X\forall z\in X\left(x\underset{\dot{}}{+}z\in S\leftrightarrow z\underset{\dot{}}{+}x\in S\right)\leftrightarrow \left(\forall x\in X\forall z\in X\left(x\underset{\dot{}}{+}z\in S\to z\underset{\dot{}}{+}x\in S\right)\wedge \forall x\in X\forall z\in X\left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)\right)$$
9		oveq2	$$⊢z=y\to x\underset{\dot{}}{+}z=x\underset{\dot{}}{+}y$$
10	9	eleq1d	$$⊢z=y\to \left(x\underset{\dot{}}{+}z\in S\leftrightarrow x\underset{\dot{}}{+}y\in S\right)$$
11		oveq1	$$⊢z=y\to z\underset{\dot{}}{+}x=y\underset{\dot{}}{+}x$$
12	11	eleq1d	$$⊢z=y\to \left(z\underset{\dot{}}{+}x\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)$$
13	10 12	imbi12d	$$⊢z=y\to \left(\left(x\underset{\dot{}}{+}z\in S\to z\underset{\dot{}}{+}x\in S\right)\leftrightarrow \left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)\right)$$
14	13	cbvralvw	$$⊢\forall z\in X\left(x\underset{\dot{}}{+}z\in S\to z\underset{\dot{}}{+}x\in S\right)\leftrightarrow \forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)$$
15	14	ralbii	$$⊢\forall x\in X\forall z\in X\left(x\underset{\dot{}}{+}z\in S\to z\underset{\dot{}}{+}x\in S\right)\leftrightarrow \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)$$
16		ralcom	$$⊢\forall x\in X\forall z\in X\left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)\leftrightarrow \forall z\in X\forall x\in X\left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)$$
17		oveq2	$$⊢x=y\to z\underset{\dot{}}{+}x=z\underset{\dot{}}{+}y$$
18	17	eleq1d	$$⊢x=y\to \left(z\underset{\dot{}}{+}x\in S\leftrightarrow z\underset{\dot{}}{+}y\in S\right)$$
19		oveq1	$$⊢x=y\to x\underset{\dot{}}{+}z=y\underset{\dot{}}{+}z$$
20	19	eleq1d	$$⊢x=y\to \left(x\underset{\dot{}}{+}z\in S\leftrightarrow y\underset{\dot{}}{+}z\in S\right)$$
21	18 20	imbi12d	$$⊢x=y\to \left(\left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)\leftrightarrow \left(z\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}z\in S\right)\right)$$
22	21	cbvralvw	$$⊢\forall x\in X\left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)\leftrightarrow \forall y\in X\left(z\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}z\in S\right)$$
23	22	ralbii	$$⊢\forall z\in X\forall x\in X\left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)\leftrightarrow \forall z\in X\forall y\in X\left(z\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}z\in S\right)$$
24		oveq1	$$⊢z=x\to z\underset{\dot{}}{+}y=x\underset{\dot{}}{+}y$$
25	24	eleq1d	$$⊢z=x\to \left(z\underset{\dot{}}{+}y\in S\leftrightarrow x\underset{\dot{}}{+}y\in S\right)$$
26		oveq2	$$⊢z=x\to y\underset{\dot{}}{+}z=y\underset{\dot{}}{+}x$$
27	26	eleq1d	$$⊢z=x\to \left(y\underset{\dot{}}{+}z\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)$$
28	25 27	imbi12d	$$⊢z=x\to \left(\left(z\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}z\in S\right)\leftrightarrow \left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)\right)$$
29	28	ralbidv	$$⊢z=x\to \left(\forall y\in X\left(z\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}z\in S\right)\leftrightarrow \forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)\right)$$
30	29	cbvralvw	$$⊢\forall z\in X\forall y\in X\left(z\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}z\in S\right)\leftrightarrow \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)$$
31	16 23 30	3bitri	$$⊢\forall x\in X\forall z\in X\left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)\leftrightarrow \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)$$
32	15 31	anbi12i	$$⊢\left(\forall x\in X\forall z\in X\left(x\underset{\dot{}}{+}z\in S\to z\underset{\dot{}}{+}x\in S\right)\wedge \forall x\in X\forall z\in X\left(z\underset{\dot{}}{+}x\in S\to x\underset{\dot{}}{+}z\in S\right)\right)\leftrightarrow \left(\forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)\wedge \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)\right)$$
33		anidm	$$⊢\left(\forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)\wedge \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)\right)\leftrightarrow \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)$$
34	8 32 33	3bitri	$$⊢\forall x\in X\forall z\in X\left(x\underset{\dot{}}{+}z\in S\leftrightarrow z\underset{\dot{}}{+}x\in S\right)\leftrightarrow \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)$$
35	34	anbi2i	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge \forall x\in X\forall z\in X\left(x\underset{\dot{}}{+}z\in S\leftrightarrow z\underset{\dot{}}{+}x\in S\right)\right)\leftrightarrow \left(S\in \mathrm{SubGrp}\left(G\right)\wedge \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)\right)$$
36	3 35	bitri	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\leftrightarrow \left(S\in \mathrm{SubGrp}\left(G\right)\wedge \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\to y\underset{\dot{}}{+}x\in S\right)\right)$$