Theorem issubgrpd

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

	Ref	Expression
Hypotheses	issubgrpd.s	$$⊢\phi \to S=I{\upharpoonright }_{𝑠}D$$
	issubgrpd.z	$$⊢\phi \to \underset{\dot{}}{0}=0_I$$
	issubgrpd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_I$$
	issubgrpd.ss	$$⊢\phi \to D\subseteq {\mathrm{Base}}_I$$
	issubgrpd.zcl	$$⊢\phi \to \underset{\dot{}}{0}\in D$$
	issubgrpd.acl	$$⊢\left(\phi \wedge x\in D\wedge y\in D\right)\to x\underset{\dot{}}{+}y\in D$$
	issubgrpd.ncl	$$⊢\left(\phi \wedge x\in D\right)\to {inv}_g\left(I\right)\left(x\right)\in D$$
	issubgrpd.g	$$⊢\phi \to I\in \mathrm{Grp}$$
Assertion	issubgrpd	$$⊢\phi \to S\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		issubgrpd.s	$$⊢\phi \to S=I{\upharpoonright }_{𝑠}D$$
2		issubgrpd.z	$$⊢\phi \to \underset{\dot{}}{0}=0_I$$
3		issubgrpd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_I$$
4		issubgrpd.ss	$$⊢\phi \to D\subseteq {\mathrm{Base}}_I$$
5		issubgrpd.zcl	$$⊢\phi \to \underset{\dot{}}{0}\in D$$
6		issubgrpd.acl	$$⊢\left(\phi \wedge x\in D\wedge y\in D\right)\to x\underset{\dot{}}{+}y\in D$$
7		issubgrpd.ncl	$$⊢\left(\phi \wedge x\in D\right)\to {inv}_g\left(I\right)\left(x\right)\in D$$
8		issubgrpd.g	$$⊢\phi \to I\in \mathrm{Grp}$$
9	1 2 3 4 5 6 7 8	issubgrpd2	$$⊢\phi \to D\in \mathrm{SubGrp}\left(I\right)$$
10		eqid	$$⊢I{\upharpoonright }_{𝑠}D=I{\upharpoonright }_{𝑠}D$$
11	10	subggrp	$$⊢D\in \mathrm{SubGrp}\left(I\right)\to I{\upharpoonright }_{𝑠}D\in \mathrm{Grp}$$
12	9 11	syl	$$⊢\phi \to I{\upharpoonright }_{𝑠}D\in \mathrm{Grp}$$
13	1 12	eqeltrd	$$⊢\phi \to S\in \mathrm{Grp}$$