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 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
ressmulgnn.2 ⊢ 𝐴 ⊆ ( Base ‘ 𝐺 )
ressmulgnn.3 ⊢ ∗ = ( .g ‘ 𝐺 )
ressmulgnn.4 ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion ressmulgnn ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ∗ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ressmulgnn.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
2 ressmulgnn.2 ⊢ 𝐴 ⊆ ( Base ‘ 𝐺 )
3 ressmulgnn.3 ⊢ ∗ = ( .g ‘ 𝐺 )
4 ressmulgnn.4 ⊢ 𝐼 = ( invg ‘ 𝐺 )
5 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 1 5 ressbas2 ⊢ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) → 𝐴 = ( Base ‘ 𝐻 ) )
7 2 6 ax-mp ⊢ 𝐴 = ( Base ‘ 𝐻 )
8 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
9 eqid ⊢ ( .g ‘ 𝐻 ) = ( .g ‘ 𝐻 )
10 fvex ⊢ ( Base ‘ 𝐺 ) ∈ V
11 10 2 ssexi ⊢ 𝐴 ∈ V
12 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
13 1 12 ressplusg ⊢ ( 𝐴 ∈ V → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
14 11 13 ax-mp ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 )
15 seqeq2 ⊢ ( ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) → seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) )
16 14 15 ax-mp ⊢ seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) )
17 7 8 9 16 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
18 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
19 2 18 sselid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
20 eqid ⊢ seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) )
21 5 12 3 20 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑁 ∗ 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
22 19 21 syldan ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴 ) → ( 𝑁 ∗ 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
23 17 22 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ∗ 𝑋 ) )