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

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 = I ↾ 𝑠 D
issubgrpd.z ⊢ φ → 0 ˙ = 0 I
issubgrpd.p ⊢ φ → + ˙ = + I
issubgrpd.ss ⊢ φ → D ⊆ Base I
issubgrpd.zcl ⊢ φ → 0 ˙ ∈ D
issubgrpd.acl ⊢ φ ∧ x ∈ D ∧ y ∈ D → x + ˙ y ∈ D
issubgrpd.ncl ⊢ φ ∧ x ∈ D → inv g ⁡ I ⁡ x ∈ D
issubgrpd.g ⊢ φ → I ∈ Grp
Assertion issubgrpd2 ⊢ φ → D ∈ SubGrp ⁡ I

Proof

Step Hyp Ref Expression
1 issubgrpd.s ⊢ φ → S = I ↾ 𝑠 D
2 issubgrpd.z ⊢ φ → 0 ˙ = 0 I
3 issubgrpd.p ⊢ φ → + ˙ = + I
4 issubgrpd.ss ⊢ φ → D ⊆ Base I
5 issubgrpd.zcl ⊢ φ → 0 ˙ ∈ D
6 issubgrpd.acl ⊢ φ ∧ x ∈ D ∧ y ∈ D → x + ˙ y ∈ D
7 issubgrpd.ncl ⊢ φ ∧ x ∈ D → inv g ⁡ I ⁡ x ∈ D
8 issubgrpd.g ⊢ φ → I ∈ Grp
9 5 ne0d ⊢ φ → D ≠ ∅
10 3 oveqd ⊢ φ → x + ˙ y = x + I y
11 10 ad2antrr ⊢ φ ∧ x ∈ D ∧ y ∈ D → x + ˙ y = x + I y
12 6 3expa ⊢ φ ∧ x ∈ D ∧ y ∈ D → x + ˙ y ∈ D
13 11 12 eqeltrrd ⊢ φ ∧ x ∈ D ∧ y ∈ D → x + I y ∈ D
14 13 ralrimiva ⊢ φ ∧ x ∈ D → ∀ y ∈ D x + I y ∈ D
15 14 7 jca ⊢ φ ∧ x ∈ D → ∀ y ∈ D x + I y ∈ D ∧ inv g ⁡ I ⁡ x ∈ D
16 15 ralrimiva ⊢ φ → ∀ x ∈ D ∀ y ∈ D x + I y ∈ D ∧ inv g ⁡ I ⁡ x ∈ D
17 eqid ⊢ Base I = Base I
18 eqid ⊢ + I = + I
19 eqid ⊢ inv g ⁡ I = inv g ⁡ I
20 17 18 19 issubg2 ⊢ I ∈ Grp → D ∈ SubGrp ⁡ I ↔ D ⊆ Base I ∧ D ≠ ∅ ∧ ∀ x ∈ D ∀ y ∈ D x + I y ∈ D ∧ inv g ⁡ I ⁡ x ∈ D
21 8 20 syl ⊢ φ → D ∈ SubGrp ⁡ I ↔ D ⊆ Base I ∧ D ≠ ∅ ∧ ∀ x ∈ D ∀ y ∈ D x + I y ∈ D ∧ inv g ⁡ I ⁡ x ∈ D
22 4 9 16 21 mpbir3and ⊢ φ → D ∈ SubGrp ⁡ I