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

Metamath Proof Explorer

Theorem mulgcld

Description: Deduction associated with mulgcl . (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses mulgcld.1 ⊢ B = Base G
mulgcld.2 ⊢ · ˙ = ⋅ G
mulgcld.3 ⊢ φ → G ∈ Grp
mulgcld.4 ⊢ φ → N ∈ ℤ
mulgcld.5 ⊢ φ → X ∈ B
Assertion mulgcld ⊢ φ → N · ˙ X ∈ B

Proof

Step Hyp Ref Expression
1 mulgcld.1 ⊢ B = Base G
2 mulgcld.2 ⊢ · ˙ = ⋅ G
3 mulgcld.3 ⊢ φ → G ∈ Grp
4 mulgcld.4 ⊢ φ → N ∈ ℤ
5 mulgcld.5 ⊢ φ → X ∈ B
6 1 2 mulgcl ⊢ G ∈ Grp ∧ N ∈ ℤ ∧ X ∈ B → N · ˙ X ∈ B
7 3 4 5 6 syl3anc ⊢ φ → N · ˙ X ∈ B