Theorem ressmulgnn0

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

	Ref	Expression
Hypotheses	ressmulgnn.1	⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
	ressmulgnn.2	⊢ 𝐴 ⊆ ( Base ‘ 𝐺 )
	ressmulgnn.3	⊢ ∗ = ( .g ‘ 𝐺 )
	ressmulgnn.4	⊢ 𝐼 = ( invg ‘ 𝐺 )
	ressmulgnn0.4	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 )
Assertion	ressmulgnn0	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ∗ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ressmulgnn.1	⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
2		ressmulgnn.2	⊢ 𝐴 ⊆ ( Base ‘ 𝐺 )
3		ressmulgnn.3	⊢ ∗ = ( .g ‘ 𝐺 )
4		ressmulgnn.4	⊢ 𝐼 = ( invg ‘ 𝐺 )
5		ressmulgnn0.4	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 )
6		simpr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
7		simplr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑁 ∈ ℕ ) → 𝑋 ∈ 𝐴 )
8	1 2 3 4	ressmulgnn	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ∗ 𝑋 ) )
9	6 7 8	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ∗ 𝑋 ) )
10		simplr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑁 = 0 ) → 𝑋 ∈ 𝐴 )
11		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
12	1 11	ressbas2	⊢ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) → 𝐴 = ( Base ‘ 𝐻 ) )
13	2 12	ax-mp	⊢ 𝐴 = ( Base ‘ 𝐻 )
14		eqid	⊢ ( .g ‘ 𝐻 ) = ( .g ‘ 𝐻 )
15	13 5 14	mulg0	⊢ ( 𝑋 ∈ 𝐴 → ( 0 ( .g ‘ 𝐻 ) 𝑋 ) = ( 0g ‘ 𝐺 ) )
16	10 15	syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑁 = 0 ) → ( 0 ( .g ‘ 𝐻 ) 𝑋 ) = ( 0g ‘ 𝐺 ) )
17		simpr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑁 = 0 ) → 𝑁 = 0 )
18	17	oveq1d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑁 = 0 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 0 ( .g ‘ 𝐻 ) 𝑋 ) )
19	2 10	sseldi	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑁 = 0 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
20		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
21	11 20 3	mulg0	⊢ ( 𝑋 ∈ ( Base ‘ 𝐺 ) → ( 0 ∗ 𝑋 ) = ( 0g ‘ 𝐺 ) )
22	19 21	syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑁 = 0 ) → ( 0 ∗ 𝑋 ) = ( 0g ‘ 𝐺 ) )
23	16 18 22	3eqtr4d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑁 = 0 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 0 ∗ 𝑋 ) )
24	17	oveq1d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑁 = 0 ) → ( 𝑁 ∗ 𝑋 ) = ( 0 ∗ 𝑋 ) )
25	23 24	eqtr4d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑁 = 0 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ∗ 𝑋 ) )
26		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
27	26	biimpi	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
28	27	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
29	9 25 28	mpjaodan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ∗ 𝑋 ) )