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

Metamath Proof Explorer

Theorem ressmulgnn

Description: Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 12-Jun-2017)

Ref Expression
Hypotheses ressmulgnn.1 ⊢ H = G ↾ 𝑠 A
ressmulgnn.2 ⊢ A ⊆ Base G
ressmulgnn.3 ⊢ ∗ ˙ = ⋅ G
ressmulgnn.4 ⊢ I = inv g ⁡ G
Assertion ressmulgnn ⊢ N ∈ ℕ ∧ X ∈ A → N ⋅ H X = N ∗ ˙ X

Proof

Step Hyp Ref Expression
1 ressmulgnn.1 ⊢ H = G ↾ 𝑠 A
2 ressmulgnn.2 ⊢ A ⊆ Base G
3 ressmulgnn.3 ⊢ ∗ ˙ = ⋅ G
4 ressmulgnn.4 ⊢ I = inv g ⁡ G
5 eqid ⊢ Base G = Base G
6 1 5 ressbas2 ⊢ A ⊆ Base G → A = Base H
7 2 6 ax-mp ⊢ A = Base H
8 eqid ⊢ + H = + H
9 eqid ⊢ ⋅ H = ⋅ H
10 fvex ⊢ Base G ∈ V
11 10 2 ssexi ⊢ A ∈ V
12 eqid ⊢ + G = + G
13 1 12 ressplusg ⊢ A ∈ V → + G = + H
14 11 13 ax-mp ⊢ + G = + H
15 seqeq2 ⊢ + G = + H → seq 1 + G ℕ × X = seq 1 + H ℕ × X
16 14 15 ax-mp ⊢ seq 1 + G ℕ × X = seq 1 + H ℕ × X
17 7 8 9 16 mulgnn ⊢ N ∈ ℕ ∧ X ∈ A → N ⋅ H X = seq 1 + G ℕ × X ⁡ N
18 simpr ⊢ N ∈ ℕ ∧ X ∈ A → X ∈ A
19 2 18 sselid ⊢ N ∈ ℕ ∧ X ∈ A → X ∈ Base G
20 eqid ⊢ seq 1 + G ℕ × X = seq 1 + G ℕ × X
21 5 12 3 20 mulgnn ⊢ N ∈ ℕ ∧ X ∈ Base G → N ∗ ˙ X = seq 1 + G ℕ × X ⁡ N
22 19 21 syldan ⊢ N ∈ ℕ ∧ X ∈ A → N ∗ ˙ X = seq 1 + G ℕ × X ⁡ N
23 17 22 eqtr4d ⊢ N ∈ ℕ ∧ X ∈ A → N ⋅ H X = N ∗ ˙ X