This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐷 ) )
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 )