issubg2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > issubg2		Structured version Visualization version GIF version

Theorem issubg2 19266

Description: Characterize the subgroups of a group by closure properties. (Contributed by Mario Carneiro, 2-Dec-2014.)

**Hypotheses**
Ref	Expression
issubg2.b	⊢ 𝐵 = (Base‘𝐺)
issubg2.p	⊢ + = (+_g‘𝐺)
issubg2.i	⊢ 𝐼 = (inv_g‘𝐺)

**Assertion**
Ref	Expression
issubg2	⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))))

Distinct variable groups: 𝑥,𝑦,𝐺 𝑥,𝐼,𝑦 𝑥, + ,𝑦 𝑥,𝑆,𝑦 Allowed substitution hints: 𝐵(𝑥, 𝑦)

Proof of Theorem issubg2 Dummy variables 𝑣 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		issubg2.b	. . . 4 ⊢ 𝐵 = (Base‘𝐺)
2	1	subgss 19251	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵)
3		eqid 2760	. . . . 5 ⊢ (𝐺 ↾_s 𝑆) = (𝐺 ↾_s 𝑆)
4	3	subgbas 19254	. . . 4 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘(𝐺 ↾_s 𝑆)))
5	3	subggrp 19253	. . . . 5 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐺 ↾_s 𝑆) ∈ Grp)
6		eqid 2760	. . . . . 6 ⊢ (Base‘(𝐺 ↾_s 𝑆)) = (Base‘(𝐺 ↾_s 𝑆))
7	6	grpbn0 19091	. . . . 5 ⊢ ((𝐺 ↾_s 𝑆) ∈ Grp → (Base‘(𝐺 ↾_s 𝑆)) ≠ ∅)
8	5, 7	syl 18	. . . 4 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (Base‘(𝐺 ↾_s 𝑆)) ≠ ∅)
9	4, 8	eqnetrd 3022	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ≠ ∅)
10		issubg2.p	. . . . . . . 8 ⊢ + = (+_g‘𝐺)
11	10	subgcl 19260	. . . . . . 7 ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
12	11	3expa 1136	. . . . . 6 ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
13	12	ralrimiva 3154	. . . . 5 ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) → ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)
14		issubg2.i	. . . . . 6 ⊢ 𝐼 = (inv_g‘𝐺)
15	14	subginvcl 19259	. . . . 5 ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) → (𝐼‘𝑥) ∈ 𝑆)
16	13, 15	jca 521	. . . 4 ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) → (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))
17	16	ralrimiva 3154	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))
18	2, 9, 17	3jca 1146	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)))
19		simpl 488	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝐺 ∈ Grp)
20		simpr1 1213	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 ⊆ 𝐵)
21	3, 1	ressbas2 17331	. . . . . 6 ⊢ (𝑆 ⊆ 𝐵 → 𝑆 = (Base‘(𝐺 ↾_s 𝑆)))
22	20, 21	syl 18	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 = (Base‘(𝐺 ↾_s 𝑆)))
23		fvex 6892	. . . . . . 7 ⊢ (Base‘(𝐺 ↾_s 𝑆)) ∈ V
24	22, 23	eqeltrdi 2868	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 ∈ V)
25	3, 10	ressplusg 17377	. . . . . 6 ⊢ (𝑆 ∈ V → + = (+_g‘(𝐺 ↾_s 𝑆)))
26	24, 25	syl 18	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → + = (+_g‘(𝐺 ↾_s 𝑆)))
27		simpr3 1215	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))
28		simpl 488	. . . . . . . . 9 ⊢ ((∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) → ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)
29	28	ralimi 3099	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)
30	27, 29	syl 18	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)
31		oveq1 7421	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (𝑥 + 𝑦) = (𝑢 + 𝑦))
32	31	eleq1d 2845	. . . . . . . 8 ⊢ (𝑥 = 𝑢 → ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑢 + 𝑦) ∈ 𝑆))
33		oveq2 7422	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → (𝑢 + 𝑦) = (𝑢 + 𝑣))
34	33	eleq1d 2845	. . . . . . . 8 ⊢ (𝑦 = 𝑣 → ((𝑢 + 𝑦) ∈ 𝑆 ↔ (𝑢 + 𝑣) ∈ 𝑆))
35	32, 34	rspc2v 3587	. . . . . . 7 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 → (𝑢 + 𝑣) ∈ 𝑆))
36	30, 35	syl5com 32	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 + 𝑣) ∈ 𝑆))
37	36	3impib 1134	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 + 𝑣) ∈ 𝑆)
38	20	sseld 3930	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (𝑢 ∈ 𝑆 → 𝑢 ∈ 𝐵))
39	20	sseld 3930	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (𝑣 ∈ 𝑆 → 𝑣 ∈ 𝐵))
40	20	sseld 3930	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (𝑤 ∈ 𝑆 → 𝑤 ∈ 𝐵))
41	38, 39, 40	3anim123d 1471	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)))
42	41	imp 412	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))
43	1, 10	grpass 19067	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
44	43	adantlr 728	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
45	42, 44	syldan 603	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
46		simpr2 1214	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 ≠ ∅)
47		n0 4300	. . . . . . 7 ⊢ (𝑆 ≠ ∅ ↔ ∃𝑢 𝑢 ∈ 𝑆)
48	46, 47	sylib 221	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∃𝑢 𝑢 ∈ 𝑆)
49	20	sselda 3931	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ 𝐵)
50		eqid 2760	. . . . . . . . . 10 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
51	1, 10, 50, 14	grplinv 19114	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝐵) → ((𝐼‘𝑢) + 𝑢) = (0_g‘𝐺))
52	51	adantlr 728	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝐵) → ((𝐼‘𝑢) + 𝑢) = (0_g‘𝐺))
53	49, 52	syldan 603	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → ((𝐼‘𝑢) + 𝑢) = (0_g‘𝐺))
54		simpr 490	. . . . . . . . . . 11 ⊢ ((∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) → (𝐼‘𝑥) ∈ 𝑆)
55	54	ralimi 3099	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) → ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)
56	27, 55	syl 18	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)
57		fveq2 6879	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → (𝐼‘𝑥) = (𝐼‘𝑢))
58	57	eleq1d 2845	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → ((𝐼‘𝑥) ∈ 𝑆 ↔ (𝐼‘𝑢) ∈ 𝑆))
59	58	rspccva 3575	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝐼‘𝑢) ∈ 𝑆)
60	56, 59	sylan 592	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → (𝐼‘𝑢) ∈ 𝑆)
61		simpr 490	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ 𝑆)
62	30	adantr 486	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)
63		ovrspc2v 7440	. . . . . . . 8 ⊢ ((((𝐼‘𝑢) ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → ((𝐼‘𝑢) + 𝑢) ∈ 𝑆)
64	60, 61, 62, 63	syl21anc 851	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → ((𝐼‘𝑢) + 𝑢) ∈ 𝑆)
65	53, 64	eqeltrrd 2861	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → (0_g‘𝐺) ∈ 𝑆)
66	48, 65	exlimddv 1968	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (0_g‘𝐺) ∈ 𝑆)
67	1, 10, 50	grplid 19092	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝐵) → ((0_g‘𝐺) + 𝑢) = 𝑢)
68	67	adantlr 728	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝐵) → ((0_g‘𝐺) + 𝑢) = 𝑢)
69	49, 68	syldan 603	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → ((0_g‘𝐺) + 𝑢) = 𝑢)
70	22, 26, 37, 45, 66, 69, 60, 53	isgrpd 19083	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (𝐺 ↾_s 𝑆) ∈ Grp)
71	1	issubg 19250	. . . 4 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾_s 𝑆) ∈ Grp))
72	19, 20, 70, 71	syl3anbrc 1362	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 ∈ (SubGrp‘𝐺))
73	72	ex 418	. 2 ⊢ (𝐺 ∈ Grp → ((𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)) → 𝑆 ∈ (SubGrp‘𝐺)))
74	18, 73	impbid2 229	1 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2145 ≠ wne 2955 ∀wral 3076 Vcvv 3450 ⊆ wss 3899 ∅c0 4279 ‘cfv 6533 (class class class)co 7414 Basecbs 17302 ↾_s cress 17323 +_gcplusg 17343 0_gc0g 17525 Grpcgrp 19058 inv_gcminusg 19059 SubGrpcsubg 19244

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7864 df-2nd 7988 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-er 8697 df-en 8954 df-dom 8955 df-sdom 8956 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-nn 12259 df-2 12328 df-sets 17257 df-slot 17275 df-ndx 17287 df-base 17303 df-ress 17324 df-plusg 17356 df-0g 17527 df-mgm 18731 df-sgrp 18822 df-mnd 18838 df-grp 19061 df-minusg 19062 df-subg 19247

This theorem is used by: issubgrpd2 19267 issubg3 19269 issubg4 19270 grpissubg 19271 subgint 19275 nmzsubg 19289 cycsubgcl 19335 ghmrn 19357 ghmpreima 19366 gastacl 19437 torsubg 19982 oddvdssubg 19983 cntzsubrng 20730 subrgugrp 20754 cntzsubr 20769 lsssubg 21142 lidlsubg 21412 cnsubglem 21630 cnmsubglem 21644 pzriprnglem4 21698 mplsubglem 22214 mplind 22287 mhpsubg 22382 cpmatsubgpmat 22946 elrgspnlem1 33683 nsgqusf1olem1 33843 constrsdrg 34286

W3C validator