Metamath Proof Explorer

Theorem ressmulgnn0d

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

Ref Expression
Hypotheses ressmulgnn0d.1 ⊢ ( 𝜑 → ( 𝐺 ↾s 𝐴 ) = 𝐻 )
ressmulgnn0d.2 ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
ressmulgnn0d.3 ⊢ ( 𝜑 → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
ressmulgnn0d.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
ressmulgnn0d.5 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion ressmulgnn0d ( 𝜑 → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ( .g ‘ 𝐺 ) 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ressmulgnn0d.1 ⊢ ( 𝜑 → ( 𝐺 ↾s 𝐴 ) = 𝐻 )
2 ressmulgnn0d.2 ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
3 ressmulgnn0d.3 ⊢ ( 𝜑 → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
4 ressmulgnn0d.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 ressmulgnn0d.5 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
6 1 fveq2d ⊢ ( 𝜑 → ( .g ‘ ( 𝐺 ↾s 𝐴 ) ) = ( .g ‘ 𝐻 ) )
7 6 oveqd ⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( 𝐺 ↾s 𝐴 ) ) 𝑋 ) = ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ( .g ‘ ( 𝐺 ↾s 𝐴 ) ) 𝑋 ) = ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) )
9 eqid ⊢ ( 𝐺 ↾s 𝐴 ) = ( 𝐺 ↾s 𝐴 )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
11 5 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑋 ∈ 𝐴 )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
13 9 10 11 12 ressmulgnnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ( .g ‘ ( 𝐺 ↾s 𝐴 ) ) 𝑋 ) = ( 𝑁 ( .g ‘ 𝐺 ) 𝑋 ) )
14 8 13 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ( .g ‘ 𝐺 ) 𝑋 ) )
15 5 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝑋 ∈ 𝐴 )
16 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
17 9 16 ressbas2 ⊢ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) → 𝐴 = ( Base ‘ ( 𝐺 ↾s 𝐴 ) ) )
18 3 17 syl ⊢ ( 𝜑 → 𝐴 = ( Base ‘ ( 𝐺 ↾s 𝐴 ) ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝐴 = ( Base ‘ ( 𝐺 ↾s 𝐴 ) ) )
20 15 19 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝑋 ∈ ( Base ‘ ( 𝐺 ↾s 𝐴 ) ) )
21 eqid ⊢ ( Base ‘ ( 𝐺 ↾s 𝐴 ) ) = ( Base ‘ ( 𝐺 ↾s 𝐴 ) )
22 eqid ⊢ ( 0g ‘ ( 𝐺 ↾s 𝐴 ) ) = ( 0g ‘ ( 𝐺 ↾s 𝐴 ) )
23 eqid ⊢ ( .g ‘ ( 𝐺 ↾s 𝐴 ) ) = ( .g ‘ ( 𝐺 ↾s 𝐴 ) )
24 21 22 23 mulg0 ⊢ ( 𝑋 ∈ ( Base ‘ ( 𝐺 ↾s 𝐴 ) ) → ( 0 ( .g ‘ ( 𝐺 ↾s 𝐴 ) ) 𝑋 ) = ( 0g ‘ ( 𝐺 ↾s 𝐴 ) ) )
25 20 24 syl ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 0 ( .g ‘ ( 𝐺 ↾s 𝐴 ) ) 𝑋 ) = ( 0g ‘ ( 𝐺 ↾s 𝐴 ) ) )
26 6 oveqd ⊢ ( 𝜑 → ( 0 ( .g ‘ ( 𝐺 ↾s 𝐴 ) ) 𝑋 ) = ( 0 ( .g ‘ 𝐻 ) 𝑋 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 0 ( .g ‘ ( 𝐺 ↾s 𝐴 ) ) 𝑋 ) = ( 0 ( .g ‘ 𝐻 ) 𝑋 ) )
28 1 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 𝐺 ↾s 𝐴 ) = 𝐻 )
29 28 fveq2d ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 0g ‘ ( 𝐺 ↾s 𝐴 ) ) = ( 0g ‘ 𝐻 ) )
30 2 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
31 29 30 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 0g ‘ ( 𝐺 ↾s 𝐴 ) ) = ( 0g ‘ 𝐺 ) )
32 25 27 31 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 0 ( .g ‘ 𝐻 ) 𝑋 ) = ( 0g ‘ 𝐺 ) )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
34 33 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 0 ( .g ‘ 𝐻 ) 𝑋 ) )
35 3 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
36 35 15 sseldd ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
37 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
38 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
39 16 37 38 mulg0 ⊢ ( 𝑋 ∈ ( Base ‘ 𝐺 ) → ( 0 ( .g ‘ 𝐺 ) 𝑋 ) = ( 0g ‘ 𝐺 ) )
40 36 39 syl ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 0 ( .g ‘ 𝐺 ) 𝑋 ) = ( 0g ‘ 𝐺 ) )
41 32 34 40 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 0 ( .g ‘ 𝐺 ) 𝑋 ) )
42 33 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 𝑁 ( .g ‘ 𝐺 ) 𝑋 ) = ( 0 ( .g ‘ 𝐺 ) 𝑋 ) )
43 41 42 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ( .g ‘ 𝐺 ) 𝑋 ) )
44 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
45 4 44 sylib ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
46 14 43 45 mpjaodan ⊢ ( 𝜑 → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ( .g ‘ 𝐺 ) 𝑋 ) )