Theorem issubg2m 13467

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	⊢ 𝐼 = (invg‘𝐺)

Assertion

Ref	Expression
issubg2m	⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑢 𝑢 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))))

Distinct variable groups:   𝑢, + ,𝑥,𝑦   𝑢,𝐵   𝑢,𝐺,𝑥,𝑦   𝑢,𝐼,𝑥,𝑦   𝑢,𝑆,𝑥,𝑦

Allowed substitution hints:   𝐵(𝑥,𝑦)

Proof of Theorem issubg2m

Dummy variables 𝑣 𝑤 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		issubg2.b	. . . 4 ⊢ 𝐵 = (Base‘𝐺)
2	1	subgss 13452	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵)
3		eqid 2204	. . . . . . 7 ⊢ (𝐺 ↾s 𝑆) = (𝐺 ↾s 𝑆)
4	3	subggrp 13455	. . . . . 6 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑆) ∈ Grp)
5		eqid 2204	. . . . . . 7 ⊢ (Base‘(𝐺 ↾s 𝑆)) = (Base‘(𝐺 ↾s 𝑆))
6		eqid 2204	. . . . . . 7 ⊢ (0g‘(𝐺 ↾s 𝑆)) = (0g‘(𝐺 ↾s 𝑆))
7	5, 6	grpidcl 13303	. . . . . 6 ⊢ ((𝐺 ↾s 𝑆) ∈ Grp → (0g‘(𝐺 ↾s 𝑆)) ∈ (Base‘(𝐺 ↾s 𝑆)))
8	4, 7	syl 14	. . . . 5 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (0g‘(𝐺 ↾s 𝑆)) ∈ (Base‘(𝐺 ↾s 𝑆)))
9	3	subgbas 13456	. . . . 5 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘(𝐺 ↾s 𝑆)))
10	8, 9	eleqtrrd 2284	. . . 4 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (0g‘(𝐺 ↾s 𝑆)) ∈ 𝑆)
11		elex2 2787	. . . 4 ⊢ ((0g‘(𝐺 ↾s 𝑆)) ∈ 𝑆 → ∃𝑢 𝑢 ∈ 𝑆)
12	10, 11	syl 14	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → ∃𝑢 𝑢 ∈ 𝑆)
13		issubg2.p	. . . . . . . 8 ⊢ + = (+g‘𝐺)
14	13	subgcl 13462	. . . . . . 7 ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
15	14	3expa 1205	. . . . . 6 ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
16	15	ralrimiva 2578	. . . . 5 ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) → ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)
17		issubg2.i	. . . . . 6 ⊢ 𝐼 = (invg‘𝐺)
18	17	subginvcl 13461	. . . . 5 ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) → (𝐼‘𝑥) ∈ 𝑆)
19	16, 18	jca 306	. . . 4 ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) → (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))
20	19	ralrimiva 2578	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))
21	2, 12, 20	3jca 1179	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝑆 ⊆ 𝐵 ∧ ∃𝑢 𝑢 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)))
22		eleq1w 2265	. . . . 5 ⊢ (𝑟 = 𝑢 → (𝑟 ∈ 𝑆 ↔ 𝑢 ∈ 𝑆))
23	22	cbvexv 1941	. . . 4 ⊢ (∃𝑟 𝑟 ∈ 𝑆 ↔ ∃𝑢 𝑢 ∈ 𝑆)
24	23	3anbi2i 1193	. . 3 ⊢ ((𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)) ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑢 𝑢 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)))
25		simpl 109	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝐺 ∈ Grp)
26		simpr1 1005	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 ⊆ 𝐵)
27	3	a1i 9	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → (𝐺 ↾s 𝑆) = (𝐺 ↾s 𝑆))
28	1	a1i 9	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → 𝐵 = (Base‘𝐺))
29		simpl 109	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → 𝐺 ∈ Grp)
30		simpr 110	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → 𝑆 ⊆ 𝐵)
31	27, 28, 29, 30	ressbas2d 12842	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → 𝑆 = (Base‘(𝐺 ↾s 𝑆)))
32	31	3ad2antr1 1164	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 = (Base‘(𝐺 ↾s 𝑆)))
33	13	a1i 9	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → + = (+g‘𝐺))
34		basfn 12832	. . . . . . . . . . 11 ⊢ Base Fn V
35	29	elexd 2784	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → 𝐺 ∈ V)
36		funfvex 5592	. . . . . . . . . . . 12 ⊢ ((Fun Base ∧ 𝐺 ∈ dom Base) → (Base‘𝐺) ∈ V)
37	36	funfni 5375	. . . . . . . . . . 11 ⊢ ((Base Fn V ∧ 𝐺 ∈ V) → (Base‘𝐺) ∈ V)
38	34, 35, 37	sylancr 414	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → (Base‘𝐺) ∈ V)
39	1, 38	eqeltrid 2291	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → 𝐵 ∈ V)
40	39, 30	ssexd 4183	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → 𝑆 ∈ V)
41	27, 33, 40, 29	ressplusgd 12903	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → + = (+g‘(𝐺 ↾s 𝑆)))
42	41	3ad2antr1 1164	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → + = (+g‘(𝐺 ↾s 𝑆)))
43		simpr3 1007	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))
44		simpl 109	. . . . . . . . . 10 ⊢ ((∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) → ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)
45	44	ralimi 2568	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)
46	43, 45	syl 14	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)
47		oveq1 5950	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → (𝑥 + 𝑦) = (𝑢 + 𝑦))
48	47	eleq1d 2273	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑢 + 𝑦) ∈ 𝑆))
49		oveq2 5951	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → (𝑢 + 𝑦) = (𝑢 + 𝑣))
50	49	eleq1d 2273	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → ((𝑢 + 𝑦) ∈ 𝑆 ↔ (𝑢 + 𝑣) ∈ 𝑆))
51	48, 50	rspc2v 2889	. . . . . . . 8 ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 → (𝑢 + 𝑣) ∈ 𝑆))
52	46, 51	syl5com 29	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 + 𝑣) ∈ 𝑆))
53	52	3impib 1203	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 + 𝑣) ∈ 𝑆)
54	26	sseld 3191	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (𝑢 ∈ 𝑆 → 𝑢 ∈ 𝐵))
55	26	sseld 3191	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (𝑣 ∈ 𝑆 → 𝑣 ∈ 𝐵))
56	26	sseld 3191	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (𝑤 ∈ 𝑆 → 𝑤 ∈ 𝐵))
57	54, 55, 56	3anim123d 1331	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)))
58	57	imp 124	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))
59	1, 13	grpass 13283	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
60	59	adantlr 477	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
61	58, 60	syldan 282	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
62		simpr2 1006	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∃𝑟 𝑟 ∈ 𝑆)
63	62, 23	sylib 122	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∃𝑢 𝑢 ∈ 𝑆)
64	26	sselda 3192	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ 𝐵)
65		eqid 2204	. . . . . . . . . . 11 ⊢ (0g‘𝐺) = (0g‘𝐺)
66	1, 13, 65, 17	grplinv 13324	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝐵) → ((𝐼‘𝑢) + 𝑢) = (0g‘𝐺))
67	66	adantlr 477	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝐵) → ((𝐼‘𝑢) + 𝑢) = (0g‘𝐺))
68	64, 67	syldan 282	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → ((𝐼‘𝑢) + 𝑢) = (0g‘𝐺))
69		simpr 110	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) → (𝐼‘𝑥) ∈ 𝑆)
70	69	ralimi 2568	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) → ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)
71	43, 70	syl 14	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)
72		fveq2 5575	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑢 → (𝐼‘𝑥) = (𝐼‘𝑢))
73	72	eleq1d 2273	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → ((𝐼‘𝑥) ∈ 𝑆 ↔ (𝐼‘𝑢) ∈ 𝑆))
74	73	rspccva 2875	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝐼‘𝑢) ∈ 𝑆)
75	71, 74	sylan 283	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → (𝐼‘𝑢) ∈ 𝑆)
76		simpr 110	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ 𝑆)
77	46	adantr 276	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)
78		ovrspc2v 5969	. . . . . . . . 9 ⊢ ((((𝐼‘𝑢) ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → ((𝐼‘𝑢) + 𝑢) ∈ 𝑆)
79	75, 76, 77, 78	syl21anc 1248	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → ((𝐼‘𝑢) + 𝑢) ∈ 𝑆)
80	68, 79	eqeltrrd 2282	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → (0g‘𝐺) ∈ 𝑆)
81	63, 80	exlimddv 1921	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (0g‘𝐺) ∈ 𝑆)
82	1, 13, 65	grplid 13305	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝐵) → ((0g‘𝐺) + 𝑢) = 𝑢)
83	82	adantlr 477	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝐵) → ((0g‘𝐺) + 𝑢) = 𝑢)
84	64, 83	syldan 282	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → ((0g‘𝐺) + 𝑢) = 𝑢)
85	32, 42, 53, 61, 81, 84, 75, 68	isgrpd 13297	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (𝐺 ↾s 𝑆) ∈ Grp)
86	1	issubg 13451	. . . . 5 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))
87	25, 26, 85, 86	syl3anbrc 1183	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 ∈ (SubGrp‘𝐺))
88	87	ex 115	. . 3 ⊢ (𝐺 ∈ Grp → ((𝑆 ⊆ 𝐵 ∧ ∃𝑟 𝑟 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)) → 𝑆 ∈ (SubGrp‘𝐺)))
89	24, 88	biimtrrid 153	. 2 ⊢ (𝐺 ∈ Grp → ((𝑆 ⊆ 𝐵 ∧ ∃𝑢 𝑢 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)) → 𝑆 ∈ (SubGrp‘𝐺)))
90	21, 89	impbid2 143	1 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑢 𝑢 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 980   = wceq 1372  ∃wex 1514   ∈ wcel 2175  ∀wral 2483  Vcvv 2771   ⊆ wss 3165   Fn wfn 5265  ‘cfv 5270  (class class class)co 5943  Basecbs 12774   ↾_s cress 12775  +_gcplusg 12851  0_gc0g 13030  Grpcgrp 13274  inv_gcminusg 13275  SubGrpcsubg 13445

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-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-coll 4158  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4479  ax-setind 4584  ax-cnex 8015  ax-resscn 8016  ax-1cn 8017  ax-1re 8018  ax-icn 8019  ax-addcl 8020  ax-addrcl 8021  ax-mulcl 8022  ax-addcom 8024  ax-addass 8026  ax-i2m1 8029  ax-0lt1 8030  ax-0id 8032  ax-rnegex 8033  ax-pre-ltirr 8036  ax-pre-ltadd 8040

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-nel 2471  df-ral 2488  df-rex 2489  df-reu 2490  df-rmo 2491  df-rab 2492  df-v 2773  df-sbc 2998  df-csb 3093  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-nul 3460  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-iun 3928  df-br 4044  df-opab 4105  df-mpt 4106  df-id 4339  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-rn 4685  df-res 4686  df-ima 4687  df-iota 5231  df-fun 5272  df-fn 5273  df-f 5274  df-f1 5275  df-fo 5276  df-f1o 5277  df-fv 5278  df-riota 5898  df-ov 5946  df-oprab 5947  df-mpo 5948  df-pnf 8108  df-mnf 8109  df-ltxr 8111  df-inn 9036  df-2 9094  df-ndx 12777  df-slot 12778  df-base 12780  df-sets 12781  df-iress 12782  df-plusg 12864  df-0g 13032  df-mgm 13130  df-sgrp 13176  df-mnd 13191  df-grp 13277  df-minusg 13278  df-subg 13448

This theorem is referenced by:  issubgrpd2  13468  issubg3  13470  issubg4m  13471  grpissubg  13472  subgintm  13476  nmzsubg  13488  ghmrn  13535  ghmpreima  13544  subrgugrp  13944  lsssubg  14081  lidlsubg  14190  cnsubglem  14283  mplsubgfi  14405