Metamath Proof Explorer

Theorem issubgrpd2

Description: Prove a subgroup by closure (definition version). (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 issubgrpd2 ( 𝜑 → 𝐷 ∈ ( SubGrp ‘ 𝐼 ) )

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 5 ne0d ⊢ ( 𝜑 → 𝐷 ≠ ∅ )
10 3 oveqd ⊢ ( 𝜑 → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g ‘ 𝐼 ) 𝑦 ) )
11 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g ‘ 𝐼 ) 𝑦 ) )
12 6 3expa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 + 𝑦 ) ∈ 𝐷 )
13 11 12 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 ( +g ‘ 𝐼 ) 𝑦 ) ∈ 𝐷 )
14 13 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( +g ‘ 𝐼 ) 𝑦 ) ∈ 𝐷 )
15 14 7 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( +g ‘ 𝐼 ) 𝑦 ) ∈ 𝐷 ∧ ( ( invg ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐷 ) )
16 15 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 ( ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( +g ‘ 𝐼 ) 𝑦 ) ∈ 𝐷 ∧ ( ( invg ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐷 ) )
17 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
18 eqid ⊢ ( +g ‘ 𝐼 ) = ( +g ‘ 𝐼 )
19 eqid ⊢ ( invg ‘ 𝐼 ) = ( invg ‘ 𝐼 )
20 17 18 19 issubg2 ⊢ ( 𝐼 ∈ Grp → ( 𝐷 ∈ ( SubGrp ‘ 𝐼 ) ↔ ( 𝐷 ⊆ ( Base ‘ 𝐼 ) ∧ 𝐷 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐷 ( ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( +g ‘ 𝐼 ) 𝑦 ) ∈ 𝐷 ∧ ( ( invg ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐷 ) ) ) )
21 8 20 syl ⊢ ( 𝜑 → ( 𝐷 ∈ ( SubGrp ‘ 𝐼 ) ↔ ( 𝐷 ⊆ ( Base ‘ 𝐼 ) ∧ 𝐷 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐷 ( ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( +g ‘ 𝐼 ) 𝑦 ) ∈ 𝐷 ∧ ( ( invg ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐷 ) ) ) )
22 4 9 16 21 mpbir3and ⊢ ( 𝜑 → 𝐷 ∈ ( SubGrp ‘ 𝐼 ) )