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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	isnsg.2	⊢ + = ( +g ‘ 𝐺 )
Assertion	isnsg2	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isnsg.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		isnsg.2	⊢ + = ( +g ‘ 𝐺 )
3	1 2	isnsg	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ) )
4		dfbi2	⊢ ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) )
5	4	ralbii	⊢ ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) )
6	5	ralbii	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) )
7		r19.26-2	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) ↔ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) )
8	6 7	bitri	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) )
9		oveq2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 + 𝑧 ) = ( 𝑥 + 𝑦 ) )
10	9	eleq1d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑥 + 𝑦 ) ∈ 𝑆 ) )
11		oveq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 + 𝑥 ) = ( 𝑦 + 𝑥 ) )
12	11	eleq1d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 + 𝑥 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
13	10 12	imbi12d	⊢ ( 𝑧 = 𝑦 → ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
14	13	cbvralvw	⊢ ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
15	14	ralbii	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
16		ralcom	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) )
17		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝑧 + 𝑥 ) = ( 𝑧 + 𝑦 ) )
18	17	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑧 + 𝑥 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) )
19		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 + 𝑧 ) = ( 𝑦 + 𝑧 ) )
20	19	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑧 ) ∈ 𝑆 ) )
21	18 20	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ↔ ( ( 𝑧 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑧 ) ∈ 𝑆 ) ) )
22	21	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑧 ) ∈ 𝑆 ) )
23	22	ralbii	⊢ ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑧 ) ∈ 𝑆 ) )
24		oveq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 + 𝑦 ) = ( 𝑥 + 𝑦 ) )
25	24	eleq1d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑥 + 𝑦 ) ∈ 𝑆 ) )
26		oveq2	⊢ ( 𝑧 = 𝑥 → ( 𝑦 + 𝑧 ) = ( 𝑦 + 𝑥 ) )
27	26	eleq1d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
28	25 27	imbi12d	⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑧 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑧 ) ∈ 𝑆 ) ↔ ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
29	28	ralbidv	⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
30	29	cbvralvw	⊢ ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
31	16 23 30	3bitri	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
32	15 31	anbi12i	⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) ↔ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
33		anidm	⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
34	8 32 33	3bitri	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
35	34	anbi2i	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
36	3 35	bitri	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )