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 ( 𝜑 → ( 𝑁 · 𝑋 ) ∈ 𝐵 )