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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgcld.2 ⊢ · = ( .g ‘ 𝐺 )
mulgcld.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
mulgcld.4 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
mulgcld.5 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion mulgcld ( 𝜑 → ( 𝑁 · 𝑋 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 mulgcld.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgcld.2 ⊢ · = ( .g ‘ 𝐺 )
3 mulgcld.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
4 mulgcld.4 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5 mulgcld.5 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
7 3 4 5 6 syl3anc ⊢ ( 𝜑 → ( 𝑁 · 𝑋 ) ∈ 𝐵 )