Metamath Proof Explorer


Theorem issubgrpd

Description: Prove a subgroup by closure. (Contributed by Stefan O'Rear, 7-Dec-2014)

Ref Expression
Hypotheses issubgrpd.s φ S = I 𝑠 D
issubgrpd.z φ 0 ˙ = 0 I
issubgrpd.p φ + ˙ = + I
issubgrpd.ss φ D Base I
issubgrpd.zcl φ 0 ˙ D
issubgrpd.acl φ x D y D x + ˙ y D
issubgrpd.ncl φ x D inv g I x D
issubgrpd.g φ I Grp
Assertion issubgrpd φ S Grp

Proof

Step Hyp Ref Expression
1 issubgrpd.s φ S = I 𝑠 D
2 issubgrpd.z φ 0 ˙ = 0 I
3 issubgrpd.p φ + ˙ = + I
4 issubgrpd.ss φ D Base I
5 issubgrpd.zcl φ 0 ˙ D
6 issubgrpd.acl φ x D y D x + ˙ y D
7 issubgrpd.ncl φ x D inv g I x D
8 issubgrpd.g φ I Grp
9 1 2 3 4 5 6 7 8 issubgrpd2 φ D SubGrp I
10 eqid I 𝑠 D = I 𝑠 D
11 10 subggrp D SubGrp I I 𝑠 D Grp
12 9 11 syl φ I 𝑠 D Grp
13 1 12 eqeltrd φ S Grp