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 
|- H = ( G |`s A )
ressmulgnnd.2 
|- ( ph -> A C_ ( Base ` G ) )
ressmulgnnd.3 
|- ( ph -> X e. A )
ressmulgnnd.4 
|- ( ph -> N e. NN )
Assertion ressmulgnnd 
|- ( ph -> ( N ( .g ` H ) X ) = ( N ( .g ` G ) X ) )

Proof

Step Hyp Ref Expression
1 ressmulgnnd.1 
 |-  H = ( G |`s A )
2 ressmulgnnd.2 
 |-  ( ph -> A C_ ( Base ` G ) )
3 ressmulgnnd.3 
 |-  ( ph -> X e. A )
4 ressmulgnnd.4 
 |-  ( ph -> N e. NN )
5 4 nngt0d 
 |-  ( ph -> 0 < N )
6 4 adantr 
 |-  ( ( ph /\ 0 < N ) -> N e. NN )
7 3 adantr 
 |-  ( ( ph /\ 0 < N ) -> X e. A )
8 eqid 
 |-  ( G |`s A ) = ( G |`s A )
9 eqid 
 |-  ( Base ` G ) = ( Base ` G )
10 8 9 ressbas2 
 |-  ( A C_ ( Base ` G ) -> A = ( Base ` ( G |`s A ) ) )
11 2 10 syl 
 |-  ( ph -> A = ( Base ` ( G |`s A ) ) )
12 11 adantr 
 |-  ( ( ph /\ 0 < N ) -> A = ( Base ` ( G |`s A ) ) )
13 eqcom 
 |-  ( H = ( G |`s A ) <-> ( G |`s A ) = H )
14 1 13 mpbi 
 |-  ( G |`s A ) = H
15 14 fveq2i 
 |-  ( Base ` ( G |`s A ) ) = ( Base ` H )
16 15 a1i 
 |-  ( ( ph /\ 0 < N ) -> ( Base ` ( G |`s A ) ) = ( Base ` H ) )
17 12 16 eqtrd 
 |-  ( ( ph /\ 0 < N ) -> A = ( Base ` H ) )
18 7 17 eleqtrd 
 |-  ( ( ph /\ 0 < N ) -> X e. ( Base ` H ) )
19 eqid 
 |-  ( Base ` H ) = ( Base ` H )
20 eqid 
 |-  ( +g ` H ) = ( +g ` H )
21 eqid 
 |-  ( .g ` H ) = ( .g ` H )
22 eqid 
 |-  seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) )
23 19 20 21 22 mulgnn 
 |-  ( ( N e. NN /\ X e. ( Base ` H ) ) -> ( N ( .g ` H ) X ) = ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) )
24 6 18 23 syl2anc 
 |-  ( ( ph /\ 0 < N ) -> ( N ( .g ` H ) X ) = ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) )
25 fvexd 
 |-  ( ph -> ( Base ` G ) e. _V )
26 25 2 ssexd 
 |-  ( ph -> A e. _V )
27 eqid 
 |-  ( +g ` G ) = ( +g ` G )
28 1 27 ressplusg 
 |-  ( A e. _V -> ( +g ` G ) = ( +g ` H ) )
29 26 28 syl 
 |-  ( ph -> ( +g ` G ) = ( +g ` H ) )
30 29 eqcomd 
 |-  ( ph -> ( +g ` H ) = ( +g ` G ) )
31 30 adantr 
 |-  ( ( ph /\ 0 < N ) -> ( +g ` H ) = ( +g ` G ) )
32 31 seqeq2d 
 |-  ( ( ph /\ 0 < N ) -> seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) )
33 32 fveq1d 
 |-  ( ( ph /\ 0 < N ) -> ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) )
34 2 3 sseldd 
 |-  ( ph -> X e. ( Base ` G ) )
35 34 adantr 
 |-  ( ( ph /\ 0 < N ) -> X e. ( Base ` G ) )
36 eqid 
 |-  ( .g ` G ) = ( .g ` G )
37 eqid 
 |-  seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` G ) , ( NN X. { X } ) )
38 9 27 36 37 mulgnn 
 |-  ( ( N e. NN /\ X e. ( Base ` G ) ) -> ( N ( .g ` G ) X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) )
39 6 35 38 syl2anc 
 |-  ( ( ph /\ 0 < N ) -> ( N ( .g ` G ) X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) )
40 39 eqcomd 
 |-  ( ( ph /\ 0 < N ) -> ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) = ( N ( .g ` G ) X ) )
41 24 33 40 3eqtrd 
 |-  ( ( ph /\ 0 < N ) -> ( N ( .g ` H ) X ) = ( N ( .g ` G ) X ) )
42 41 ex 
 |-  ( ph -> ( 0 < N -> ( N ( .g ` H ) X ) = ( N ( .g ` G ) X ) ) )
43 5 42 mpd 
 |-  ( ph -> ( N ( .g ` H ) X ) = ( N ( .g ` G ) X ) )