Theorem issubgrpd2

Description: Prove a subgroup by closure (definition version). (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	issubgrpd2	$$⊢\phi \to D\in \mathrm{SubGrp}\left(I\right)$$

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	5	ne0d	$$⊢\phi \to D\ne \varnothing$$
10	3	oveqd	$$⊢\phi \to x\underset{\dot{}}{+}y=x{+}_{I}y$$
11	10	ad2antrr	$$⊢\left(\left(\phi \wedge x\in D\right)\wedge y\in D\right)\to x\underset{\dot{}}{+}y=x{+}_{I}y$$
12	6	3expa	$$⊢\left(\left(\phi \wedge x\in D\right)\wedge y\in D\right)\to x\underset{\dot{}}{+}y\in D$$
13	11 12	eqeltrrd	$$⊢\left(\left(\phi \wedge x\in D\right)\wedge y\in D\right)\to x{+}_{I}y\in D$$
14	13	ralrimiva	$$⊢\left(\phi \wedge x\in D\right)\to \forall y\in Dx{+}_{I}y\in D$$
15	14 7	jca	$$⊢\left(\phi \wedge x\in D\right)\to \left(\forall y\in Dx{+}_{I}y\in D\wedge {inv}_g\left(I\right)\left(x\right)\in D\right)$$
16	15	ralrimiva	$$⊢\phi \to \forall x\in D\left(\forall y\in Dx{+}_{I}y\in D\wedge {inv}_g\left(I\right)\left(x\right)\in D\right)$$
17		eqid	$$⊢{\mathrm{Base}}_I={\mathrm{Base}}_I$$
18		eqid	$$⊢{+}_I={+}_I$$
19		eqid	$$⊢{inv}_g\left(I\right)={inv}_g\left(I\right)$$
20	17 18 19	issubg2	$$⊢I\in \mathrm{Grp}\to \left(D\in \mathrm{SubGrp}\left(I\right)\leftrightarrow \left(D\subseteq {\mathrm{Base}}_I\wedge D\ne \varnothing \wedge \forall x\in D\left(\forall y\in Dx{+}_{I}y\in D\wedge {inv}_g\left(I\right)\left(x\right)\in D\right)\right)\right)$$
21	8 20	syl	$$⊢\phi \to \left(D\in \mathrm{SubGrp}\left(I\right)\leftrightarrow \left(D\subseteq {\mathrm{Base}}_I\wedge D\ne \varnothing \wedge \forall x\in D\left(\forall y\in Dx{+}_{I}y\in D\wedge {inv}_g\left(I\right)\left(x\right)\in D\right)\right)\right)$$
22	4 9 16 21	mpbir3and	$$⊢\phi \to D\in \mathrm{SubGrp}\left(I\right)$$