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

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

Proof

Step Hyp Ref Expression
1 ressmulgnn0d.1 
 |-  ( ph -> ( G |`s A ) = H )
2 ressmulgnn0d.2 
 |-  ( ph -> ( 0g ` G ) = ( 0g ` H ) )
3 ressmulgnn0d.3 
 |-  ( ph -> A C_ ( Base ` G ) )
4 ressmulgnn0d.4 
 |-  ( ph -> N e. NN0 )
5 ressmulgnn0d.5 
 |-  ( ph -> X e. A )
6 1 fveq2d 
 |-  ( ph -> ( .g ` ( G |`s A ) ) = ( .g ` H ) )
7 6 oveqd 
 |-  ( ph -> ( N ( .g ` ( G |`s A ) ) X ) = ( N ( .g ` H ) X ) )
8 7 adantr 
 |-  ( ( ph /\ N e. NN ) -> ( N ( .g ` ( G |`s A ) ) X ) = ( N ( .g ` H ) X ) )
9 eqid 
 |-  ( G |`s A ) = ( G |`s A )
10 3 adantr 
 |-  ( ( ph /\ N e. NN ) -> A C_ ( Base ` G ) )
11 5 adantr 
 |-  ( ( ph /\ N e. NN ) -> X e. A )
12 simpr 
 |-  ( ( ph /\ N e. NN ) -> N e. NN )
13 9 10 11 12 ressmulgnnd 
 |-  ( ( ph /\ N e. NN ) -> ( N ( .g ` ( G |`s A ) ) X ) = ( N ( .g ` G ) X ) )
14 8 13 eqtr3d 
 |-  ( ( ph /\ N e. NN ) -> ( N ( .g ` H ) X ) = ( N ( .g ` G ) X ) )
15 5 adantr 
 |-  ( ( ph /\ N = 0 ) -> X e. A )
16 eqid 
 |-  ( Base ` G ) = ( Base ` G )
17 9 16 ressbas2 
 |-  ( A C_ ( Base ` G ) -> A = ( Base ` ( G |`s A ) ) )
18 3 17 syl 
 |-  ( ph -> A = ( Base ` ( G |`s A ) ) )
19 18 adantr 
 |-  ( ( ph /\ N = 0 ) -> A = ( Base ` ( G |`s A ) ) )
20 15 19 eleqtrd 
 |-  ( ( ph /\ N = 0 ) -> X e. ( Base ` ( G |`s A ) ) )
21 eqid 
 |-  ( Base ` ( G |`s A ) ) = ( Base ` ( G |`s A ) )
22 eqid 
 |-  ( 0g ` ( G |`s A ) ) = ( 0g ` ( G |`s A ) )
23 eqid 
 |-  ( .g ` ( G |`s A ) ) = ( .g ` ( G |`s A ) )
24 21 22 23 mulg0 
 |-  ( X e. ( Base ` ( G |`s A ) ) -> ( 0 ( .g ` ( G |`s A ) ) X ) = ( 0g ` ( G |`s A ) ) )
25 20 24 syl 
 |-  ( ( ph /\ N = 0 ) -> ( 0 ( .g ` ( G |`s A ) ) X ) = ( 0g ` ( G |`s A ) ) )
26 6 oveqd 
 |-  ( ph -> ( 0 ( .g ` ( G |`s A ) ) X ) = ( 0 ( .g ` H ) X ) )
27 26 adantr 
 |-  ( ( ph /\ N = 0 ) -> ( 0 ( .g ` ( G |`s A ) ) X ) = ( 0 ( .g ` H ) X ) )
28 1 adantr 
 |-  ( ( ph /\ N = 0 ) -> ( G |`s A ) = H )
29 28 fveq2d 
 |-  ( ( ph /\ N = 0 ) -> ( 0g ` ( G |`s A ) ) = ( 0g ` H ) )
30 2 adantr 
 |-  ( ( ph /\ N = 0 ) -> ( 0g ` G ) = ( 0g ` H ) )
31 29 30 eqtr4d 
 |-  ( ( ph /\ N = 0 ) -> ( 0g ` ( G |`s A ) ) = ( 0g ` G ) )
32 25 27 31 3eqtr3d 
 |-  ( ( ph /\ N = 0 ) -> ( 0 ( .g ` H ) X ) = ( 0g ` G ) )
33 simpr 
 |-  ( ( ph /\ N = 0 ) -> N = 0 )
34 33 oveq1d 
 |-  ( ( ph /\ N = 0 ) -> ( N ( .g ` H ) X ) = ( 0 ( .g ` H ) X ) )
35 3 adantr 
 |-  ( ( ph /\ N = 0 ) -> A C_ ( Base ` G ) )
36 35 15 sseldd 
 |-  ( ( ph /\ N = 0 ) -> X e. ( Base ` G ) )
37 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
38 eqid 
 |-  ( .g ` G ) = ( .g ` G )
39 16 37 38 mulg0 
 |-  ( X e. ( Base ` G ) -> ( 0 ( .g ` G ) X ) = ( 0g ` G ) )
40 36 39 syl 
 |-  ( ( ph /\ N = 0 ) -> ( 0 ( .g ` G ) X ) = ( 0g ` G ) )
41 32 34 40 3eqtr4d 
 |-  ( ( ph /\ N = 0 ) -> ( N ( .g ` H ) X ) = ( 0 ( .g ` G ) X ) )
42 33 oveq1d 
 |-  ( ( ph /\ N = 0 ) -> ( N ( .g ` G ) X ) = ( 0 ( .g ` G ) X ) )
43 41 42 eqtr4d 
 |-  ( ( ph /\ N = 0 ) -> ( N ( .g ` H ) X ) = ( N ( .g ` G ) X ) )
44 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
45 4 44 sylib 
 |-  ( ph -> ( N e. NN \/ N = 0 ) )
46 14 43 45 mpjaodan 
 |-  ( ph -> ( N ( .g ` H ) X ) = ( N ( .g ` G ) X ) )