issubgrpd

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

	Ref	Expression
Hypotheses	issubgrpd.s	$⊢ φ \to S = I ↾_{𝑠} D$
	issubgrpd.z	$⊢ φ \to \underset{˙}{0} = 0_{I}$
	issubgrpd.p	$⊢ φ \to \underset{˙}{+} = +_{I}$
	issubgrpd.ss	$⊢ φ \to D \subseteq {Base}_{I}$
	issubgrpd.zcl	$⊢ φ \to \underset{˙}{0} \in D$
	issubgrpd.acl	$⊢ (φ \land x \in D \land y \in D) \to x \underset{˙}{+} y \in D$
	issubgrpd.ncl	$⊢ (φ \land x \in D) \to {inv}_{g} (I) (x) \in D$
	issubgrpd.g	$⊢ φ \to I \in Grp$
Assertion	issubgrpd	$⊢ φ \to S \in Grp$

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

Metamath Proof Explorer