This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ressmulgnnd

Description: Values for the group multiple function in a restricted structure, a deduction version. (Contributed by metakunt, 14-May-2025)

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

Proof

Step Hyp Ref Expression
1 ressmulgnnd.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
2 ressmulgnnd.2 ⊢ ( 𝜑 → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
3 ressmulgnnd.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4 ressmulgnnd.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5 4 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
6 4 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝑁 ∈ ℕ )
7 3 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝑋 ∈ 𝐴 )
8 eqid ⊢ ( 𝐺 ↾s 𝐴 ) = ( 𝐺 ↾s 𝐴 )
9 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
10 8 9 ressbas2 ⊢ ( 𝐴 ⊆ ( Base ‘ 𝐺 ) → 𝐴 = ( Base ‘ ( 𝐺 ↾s 𝐴 ) ) )
11 2 10 syl ⊢ ( 𝜑 → 𝐴 = ( Base ‘ ( 𝐺 ↾s 𝐴 ) ) )
12 11 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝐴 = ( Base ‘ ( 𝐺 ↾s 𝐴 ) ) )
13 eqcom ⊢ ( 𝐻 = ( 𝐺 ↾s 𝐴 ) ↔ ( 𝐺 ↾s 𝐴 ) = 𝐻 )
14 1 13 mpbi ⊢ ( 𝐺 ↾s 𝐴 ) = 𝐻
15 14 fveq2i ⊢ ( Base ‘ ( 𝐺 ↾s 𝐴 ) ) = ( Base ‘ 𝐻 )
16 15 a1i ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( Base ‘ ( 𝐺 ↾s 𝐴 ) ) = ( Base ‘ 𝐻 ) )
17 12 16 eqtrd ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝐴 = ( Base ‘ 𝐻 ) )
18 7 17 eleqtrd ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐻 ) )
19 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
20 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
21 eqid ⊢ ( .g ‘ 𝐻 ) = ( .g ‘ 𝐻 )
22 eqid ⊢ seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) )
23 19 20 21 22 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( Base ‘ 𝐻 ) ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
24 6 18 23 syl2anc ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
25 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) ∈ V )
26 25 2 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
27 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
28 1 27 ressplusg ⊢ ( 𝐴 ∈ V → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
29 26 28 syl ⊢ ( 𝜑 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
30 29 eqcomd ⊢ ( 𝜑 → ( +g ‘ 𝐻 ) = ( +g ‘ 𝐺 ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( +g ‘ 𝐻 ) = ( +g ‘ 𝐺 ) )
32 31 seqeq2d ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) )
33 32 fveq1d ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
34 2 3 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐺 ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
36 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
37 eqid ⊢ seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) )
38 9 27 36 37 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑁 ( .g ‘ 𝐺 ) 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
39 6 35 38 syl2anc ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( 𝑁 ( .g ‘ 𝐺 ) 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
40 39 eqcomd ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) = ( 𝑁 ( .g ‘ 𝐺 ) 𝑋 ) )
41 24 33 40 3eqtrd ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ( .g ‘ 𝐺 ) 𝑋 ) )
42 41 ex ⊢ ( 𝜑 → ( 0 < 𝑁 → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ( .g ‘ 𝐺 ) 𝑋 ) ) )
43 5 42 mpd ⊢ ( 𝜑 → ( 𝑁 ( .g ‘ 𝐻 ) 𝑋 ) = ( 𝑁 ( .g ‘ 𝐺 ) 𝑋 ) )