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

Theorem issubg2 19171
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
issubg2 (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))))
Distinct variable groups:   𝑥,𝑦,𝐺   𝑥,𝐼,𝑦   𝑥, + ,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦)

Proof of Theorem issubg2
Dummy variables 𝑣 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 issubg2.b . . . 4 𝐵 = (Base‘𝐺)
21subgss 19157 . . 3 (𝑆 ∈ (SubGrp‘𝐺) → 𝑆𝐵)
3 eqid 2734 . . . . 5 (𝐺s 𝑆) = (𝐺s 𝑆)
43subgbas 19160 . . . 4 (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘(𝐺s 𝑆)))
53subggrp 19159 . . . . 5 (𝑆 ∈ (SubGrp‘𝐺) → (𝐺s 𝑆) ∈ Grp)
6 eqid 2734 . . . . . 6 (Base‘(𝐺s 𝑆)) = (Base‘(𝐺s 𝑆))
76grpbn0 18996 . . . . 5 ((𝐺s 𝑆) ∈ Grp → (Base‘(𝐺s 𝑆)) ≠ ∅)
85, 7syl 17 . . . 4 (𝑆 ∈ (SubGrp‘𝐺) → (Base‘(𝐺s 𝑆)) ≠ ∅)
94, 8eqnetrd 3005 . . 3 (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ≠ ∅)
10 issubg2.p . . . . . . . 8 + = (+g𝐺)
1110subgcl 19166 . . . . . . 7 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥𝑆𝑦𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
12113expa 1117 . . . . . 6 (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥𝑆) ∧ 𝑦𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
1312ralrimiva 3143 . . . . 5 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥𝑆) → ∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆)
14 issubg2.i . . . . . 6 𝐼 = (invg𝐺)
1514subginvcl 19165 . . . . 5 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥𝑆) → (𝐼𝑥) ∈ 𝑆)
1613, 15jca 511 . . . 4 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥𝑆) → (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))
1716ralrimiva 3143 . . 3 (𝑆 ∈ (SubGrp‘𝐺) → ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))
182, 9, 173jca 1127 . 2 (𝑆 ∈ (SubGrp‘𝐺) → (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆)))
19 simpl 482 . . . 4 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → 𝐺 ∈ Grp)
20 simpr1 1193 . . . 4 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → 𝑆𝐵)
213, 1ressbas2 17282 . . . . . 6 (𝑆𝐵𝑆 = (Base‘(𝐺s 𝑆)))
2220, 21syl 17 . . . . 5 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → 𝑆 = (Base‘(𝐺s 𝑆)))
23 fvex 6919 . . . . . . 7 (Base‘(𝐺s 𝑆)) ∈ V
2422, 23eqeltrdi 2846 . . . . . 6 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → 𝑆 ∈ V)
253, 10ressplusg 17335 . . . . . 6 (𝑆 ∈ V → + = (+g‘(𝐺s 𝑆)))
2624, 25syl 17 . . . . 5 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → + = (+g‘(𝐺s 𝑆)))
27 simpr3 1195 . . . . . . . 8 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))
28 simpl 482 . . . . . . . . 9 ((∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆) → ∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆)
2928ralimi 3080 . . . . . . . 8 (∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆) → ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆)
3027, 29syl 17 . . . . . . 7 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆)
31 oveq1 7437 . . . . . . . . 9 (𝑥 = 𝑢 → (𝑥 + 𝑦) = (𝑢 + 𝑦))
3231eleq1d 2823 . . . . . . . 8 (𝑥 = 𝑢 → ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑢 + 𝑦) ∈ 𝑆))
33 oveq2 7438 . . . . . . . . 9 (𝑦 = 𝑣 → (𝑢 + 𝑦) = (𝑢 + 𝑣))
3433eleq1d 2823 . . . . . . . 8 (𝑦 = 𝑣 → ((𝑢 + 𝑦) ∈ 𝑆 ↔ (𝑢 + 𝑣) ∈ 𝑆))
3532, 34rspc2v 3632 . . . . . . 7 ((𝑢𝑆𝑣𝑆) → (∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 → (𝑢 + 𝑣) ∈ 𝑆))
3630, 35syl5com 31 . . . . . 6 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → ((𝑢𝑆𝑣𝑆) → (𝑢 + 𝑣) ∈ 𝑆))
37363impib 1115 . . . . 5 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ 𝑢𝑆𝑣𝑆) → (𝑢 + 𝑣) ∈ 𝑆)
3820sseld 3993 . . . . . . . 8 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → (𝑢𝑆𝑢𝐵))
3920sseld 3993 . . . . . . . 8 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → (𝑣𝑆𝑣𝐵))
4020sseld 3993 . . . . . . . 8 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → (𝑤𝑆𝑤𝐵))
4138, 39, 403anim123d 1442 . . . . . . 7 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → ((𝑢𝑆𝑣𝑆𝑤𝑆) → (𝑢𝐵𝑣𝐵𝑤𝐵)))
4241imp 406 . . . . . 6 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ (𝑢𝑆𝑣𝑆𝑤𝑆)) → (𝑢𝐵𝑣𝐵𝑤𝐵))
431, 10grpass 18972 . . . . . . 7 ((𝐺 ∈ Grp ∧ (𝑢𝐵𝑣𝐵𝑤𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
4443adantlr 715 . . . . . 6 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ (𝑢𝐵𝑣𝐵𝑤𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
4542, 44syldan 591 . . . . 5 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ (𝑢𝑆𝑣𝑆𝑤𝑆)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
46 simpr2 1194 . . . . . . 7 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → 𝑆 ≠ ∅)
47 n0 4358 . . . . . . 7 (𝑆 ≠ ∅ ↔ ∃𝑢 𝑢𝑆)
4846, 47sylib 218 . . . . . 6 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → ∃𝑢 𝑢𝑆)
4920sselda 3994 . . . . . . . 8 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ 𝑢𝑆) → 𝑢𝐵)
50 eqid 2734 . . . . . . . . . 10 (0g𝐺) = (0g𝐺)
511, 10, 50, 14grplinv 19019 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝑢𝐵) → ((𝐼𝑢) + 𝑢) = (0g𝐺))
5251adantlr 715 . . . . . . . 8 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ 𝑢𝐵) → ((𝐼𝑢) + 𝑢) = (0g𝐺))
5349, 52syldan 591 . . . . . . 7 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ 𝑢𝑆) → ((𝐼𝑢) + 𝑢) = (0g𝐺))
54 simpr 484 . . . . . . . . . . 11 ((∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆) → (𝐼𝑥) ∈ 𝑆)
5554ralimi 3080 . . . . . . . . . 10 (∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆) → ∀𝑥𝑆 (𝐼𝑥) ∈ 𝑆)
5627, 55syl 17 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → ∀𝑥𝑆 (𝐼𝑥) ∈ 𝑆)
57 fveq2 6906 . . . . . . . . . . 11 (𝑥 = 𝑢 → (𝐼𝑥) = (𝐼𝑢))
5857eleq1d 2823 . . . . . . . . . 10 (𝑥 = 𝑢 → ((𝐼𝑥) ∈ 𝑆 ↔ (𝐼𝑢) ∈ 𝑆))
5958rspccva 3620 . . . . . . . . 9 ((∀𝑥𝑆 (𝐼𝑥) ∈ 𝑆𝑢𝑆) → (𝐼𝑢) ∈ 𝑆)
6056, 59sylan 580 . . . . . . . 8 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ 𝑢𝑆) → (𝐼𝑢) ∈ 𝑆)
61 simpr 484 . . . . . . . 8 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ 𝑢𝑆) → 𝑢𝑆)
6230adantr 480 . . . . . . . 8 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ 𝑢𝑆) → ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆)
63 ovrspc2v 7456 . . . . . . . 8 ((((𝐼𝑢) ∈ 𝑆𝑢𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) → ((𝐼𝑢) + 𝑢) ∈ 𝑆)
6460, 61, 62, 63syl21anc 838 . . . . . . 7 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ 𝑢𝑆) → ((𝐼𝑢) + 𝑢) ∈ 𝑆)
6553, 64eqeltrrd 2839 . . . . . 6 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ 𝑢𝑆) → (0g𝐺) ∈ 𝑆)
6648, 65exlimddv 1932 . . . . 5 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → (0g𝐺) ∈ 𝑆)
671, 10, 50grplid 18997 . . . . . . 7 ((𝐺 ∈ Grp ∧ 𝑢𝐵) → ((0g𝐺) + 𝑢) = 𝑢)
6867adantlr 715 . . . . . 6 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ 𝑢𝐵) → ((0g𝐺) + 𝑢) = 𝑢)
6949, 68syldan 591 . . . . 5 (((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) ∧ 𝑢𝑆) → ((0g𝐺) + 𝑢) = 𝑢)
7022, 26, 37, 45, 66, 69, 60, 53isgrpd 18988 . . . 4 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → (𝐺s 𝑆) ∈ Grp)
711issubg 19156 . . . 4 (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆𝐵 ∧ (𝐺s 𝑆) ∈ Grp))
7219, 20, 70, 71syl3anbrc 1342 . . 3 ((𝐺 ∈ Grp ∧ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))) → 𝑆 ∈ (SubGrp‘𝐺))
7372ex 412 . 2 (𝐺 ∈ Grp → ((𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆)) → 𝑆 ∈ (SubGrp‘𝐺)))
7418, 73impbid2 226 1 (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑥𝑆 (∀𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼𝑥) ∈ 𝑆))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wex 1775  wcel 2105  wne 2937  wral 3058  Vcvv 3477  wss 3962  c0 4338  cfv 6562  (class class class)co 7430  Basecbs 17244  s cress 17273  +gcplusg 17297  0gc0g 17485  Grpcgrp 18963  invgcminusg 18964  SubGrpcsubg 19150
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-0g 17487  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-grp 18966  df-minusg 18967  df-subg 19153
This theorem is referenced by:  issubgrpd2  19172  issubg3  19174  issubg4  19175  grpissubg  19176  subgint  19180  0subgOLD  19182  nmzsubg  19195  cycsubgcl  19236  ghmrn  19259  ghmpreima  19268  gastacl  19339  torsubg  19886  oddvdssubg  19887  cntzsubrng  20583  subrgugrp  20607  cntzsubr  20622  lsssubg  20972  lidlsubg  21250  cnsubglem  21450  cnmsubglem  21465  pzriprnglem4  21512  mplsubglem  22036  mplind  22111  mhpsubg  22174  cpmatsubgpmat  22741  elrgspnlem1  33231  nsgqusf1olem1  33420
  Copyright terms: Public domain W3C validator