Theorem isnsg2 13094

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

Hypotheses

Ref	Expression
isnsg.1	⊢ 𝑋 = (Base‘𝐺)
isnsg.2	⊢ + = (+g‘𝐺)

Assertion

Ref	Expression
isnsg2	⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 → (𝑦 + 𝑥) ∈ 𝑆)))

Distinct variable groups:   𝑥,𝑦,𝐺   𝑥, + ,𝑦   𝑥,𝑆,𝑦   𝑥,𝑋,𝑦

Proof of Theorem isnsg2

Dummy variable 𝑧 is distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1363   ∈ wcel 2158  ∀wral 2465  ‘cfv 5228  (class class class)co 5888  Basecbs 12475  +_gcplusg 12550  SubGrpcsubg 13058  NrmSGrpcnsg 13059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-cnex 7915  ax-resscn 7916  ax-1re 7918  ax-addrcl 7921

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-un 3145  df-in 3147  df-ss 3154  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-br 4016  df-opab 4077  df-mpt 4078  df-id 4305  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-fv 5236  df-ov 5891  df-inn 8933  df-2 8991  df-ndx 12478  df-slot 12479  df-base 12481  df-plusg 12563  df-subg 13061  df-nsg 13062

This theorem is referenced by:  isnsg3  13098  subrngringnsg  13420