Theorem issubgrpd

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

	Ref	Expression
Hypotheses	issubgrpd.s	⊢ ( 𝜑 → 𝑆 = ( 𝐼 ↾s 𝐷 ) )
	issubgrpd.z	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐼 ) )
	issubgrpd.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐼 ) )
	issubgrpd.ss	⊢ ( 𝜑 → 𝐷 ⊆ ( Base ‘ 𝐼 ) )
	issubgrpd.zcl	⊢ ( 𝜑 → 0 ∈ 𝐷 )
	issubgrpd.acl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 + 𝑦 ) ∈ 𝐷 )
	issubgrpd.ncl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invg ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐷 )
	issubgrpd.g	⊢ ( 𝜑 → 𝐼 ∈ Grp )
Assertion	issubgrpd	⊢ ( 𝜑 → 𝑆 ∈ Grp )

Proof

Step	Hyp	Ref	Expression
1		issubgrpd.s	⊢ ( 𝜑 → 𝑆 = ( 𝐼 ↾s 𝐷 ) )
2		issubgrpd.z	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐼 ) )
3		issubgrpd.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐼 ) )
4		issubgrpd.ss	⊢ ( 𝜑 → 𝐷 ⊆ ( Base ‘ 𝐼 ) )
5		issubgrpd.zcl	⊢ ( 𝜑 → 0 ∈ 𝐷 )
6		issubgrpd.acl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 + 𝑦 ) ∈ 𝐷 )
7		issubgrpd.ncl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invg ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐷 )
8		issubgrpd.g	⊢ ( 𝜑 → 𝐼 ∈ Grp )
9	1 2 3 4 5 6 7 8	issubgrpd2	⊢ ( 𝜑 → 𝐷 ∈ ( SubGrp ‘ 𝐼 ) )
10		eqid	⊢ ( 𝐼 ↾s 𝐷 ) = ( 𝐼 ↾s 𝐷 )
11	10	subggrp	⊢ ( 𝐷 ∈ ( SubGrp ‘ 𝐼 ) → ( 𝐼 ↾s 𝐷 ) ∈ Grp )
12	9 11	syl	⊢ ( 𝜑 → ( 𝐼 ↾s 𝐷 ) ∈ Grp )
13	1 12	eqeltrd	⊢ ( 𝜑 → 𝑆 ∈ Grp )