Metamath Proof Explorer

Theorem issubg2

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

Ref Expression
Hypotheses issubg2.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
issubg2.p ⊢ + = ( +g ‘ 𝐺 )
issubg2.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion issubg2 ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) )

Proof

Step Hyp Ref Expression
1 issubg2.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 issubg2.p ⊢ + = ( +g ‘ 𝐺 )
3 issubg2.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
4 1 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝐵 )
5 eqid ⊢ ( 𝐺 ↾s 𝑆 ) = ( 𝐺 ↾s 𝑆 )
6 5 subgbas ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
7 5 subggrp ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp )
8 eqid ⊢ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) = ( Base ‘ ( 𝐺 ↾s 𝑆 ) )
9 8 grpbn0 ⊢ ( ( 𝐺 ↾s 𝑆 ) ∈ Grp → ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ≠ ∅ )
10 7 9 syl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ≠ ∅ )
11 6 10 eqnetrd ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ≠ ∅ )
12 2 subgcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
13 12 3expa ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
14 13 ralrimiva ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 )
15 3 subginvcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )
16 14 15 jca ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )
17 16 ralrimiva ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )
18 4 11 17 3jca ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) )
19 simpl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → 𝐺 ∈ Grp )
20 simpr1 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → 𝑆 ⊆ 𝐵 )
21 5 1 ressbas2 ⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
22 20 21 syl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
23 fvex ⊢ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ∈ V
24 22 23 eqeltrdi ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → 𝑆 ∈ V )
25 5 2 ressplusg ⊢ ( 𝑆 ∈ V → + = ( +g ‘ ( 𝐺 ↾s 𝑆 ) ) )
26 24 25 syl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → + = ( +g ‘ ( 𝐺 ↾s 𝑆 ) ) )
27 simpr3 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )
28 simpl ⊢ ( ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 )
29 28 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 )
30 27 29 syl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 )
31 oveq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 + 𝑦 ) = ( 𝑢 + 𝑦 ) )
32 31 eleq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑢 + 𝑦 ) ∈ 𝑆 ) )
33 oveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝑢 + 𝑦 ) = ( 𝑢 + 𝑣 ) )
34 33 eleq1d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑢 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑢 + 𝑣 ) ∈ 𝑆 ) )
35 32 34 rspc2v ⊢ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑢 + 𝑣 ) ∈ 𝑆 ) )
36 30 35 syl5com ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 + 𝑣 ) ∈ 𝑆 ) )
37 36 3impib ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 + 𝑣 ) ∈ 𝑆 )
38 20 sseld ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → ( 𝑢 ∈ 𝑆 → 𝑢 ∈ 𝐵 ) )
39 20 sseld ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → ( 𝑣 ∈ 𝑆 → 𝑣 ∈ 𝐵 ) )
40 20 sseld ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → ( 𝑤 ∈ 𝑆 → 𝑤 ∈ 𝐵 ) )
41 38 39 40 3anim123d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) → ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) )
42 41 imp ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) )
43 1 2 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑣 ) + 𝑤 ) = ( 𝑢 + ( 𝑣 + 𝑤 ) ) )
44 43 adantlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑣 ) + 𝑤 ) = ( 𝑢 + ( 𝑣 + 𝑤 ) ) )
45 42 44 syldan ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( 𝑢 + 𝑣 ) + 𝑤 ) = ( 𝑢 + ( 𝑣 + 𝑤 ) ) )
46 simpr2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → 𝑆 ≠ ∅ )
47 n0 ⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑢 𝑢 ∈ 𝑆 )
48 46 47 sylib ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → ∃ 𝑢 𝑢 ∈ 𝑆 )
49 20 sselda ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ 𝑢 ∈ 𝑆 ) → 𝑢 ∈ 𝐵 )
50 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
51 1 2 50 3 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝐼 ‘ 𝑢 ) + 𝑢 ) = ( 0g ‘ 𝐺 ) )
52 51 adantlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝐼 ‘ 𝑢 ) + 𝑢 ) = ( 0g ‘ 𝐺 ) )
53 49 52 syldan ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ 𝑢 ∈ 𝑆 ) → ( ( 𝐼 ‘ 𝑢 ) + 𝑢 ) = ( 0g ‘ 𝐺 ) )
54 simpr ⊢ ( ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )
55 54 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )
56 27 55 syl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )
57 fveq2 ⊢ ( 𝑥 = 𝑢 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑢 ) )
58 57 eleq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ↔ ( 𝐼 ‘ 𝑢 ) ∈ 𝑆 ) )
59 58 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑢 ) ∈ 𝑆 )
60 56 59 sylan ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ 𝑢 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑢 ) ∈ 𝑆 )
61 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ 𝑢 ∈ 𝑆 ) → 𝑢 ∈ 𝑆 )
62 30 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ 𝑢 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 )
63 ovrspc2v ⊢ ( ( ( ( 𝐼 ‘ 𝑢 ) ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → ( ( 𝐼 ‘ 𝑢 ) + 𝑢 ) ∈ 𝑆 )
64 60 61 62 63 syl21anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ 𝑢 ∈ 𝑆 ) → ( ( 𝐼 ‘ 𝑢 ) + 𝑢 ) ∈ 𝑆 )
65 53 64 eqeltrrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ 𝑢 ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
66 48 65 exlimddv ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
67 1 2 50 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑢 ) = 𝑢 )
68 67 adantlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑢 ) = 𝑢 )
69 49 68 syldan ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) ∧ 𝑢 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) + 𝑢 ) = 𝑢 )
70 22 26 37 45 66 69 60 53 isgrpd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp )
71 1 issubg ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )
72 19 20 70 71 syl3anbrc ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
73 72 ex ⊢ ( 𝐺 ∈ Grp → ( ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) )
74 18 73 impbid2 ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) )