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 ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ∗ 𝑋 ) )