Metamath Proof Explorer

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 sselid ⊢ ( ( ( 𝑁 ∈ ℕ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 birani ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
28 9 25 27 mpjaodan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ∗ 𝑋 ) )