Metamath Proof Explorer

Theorem mhmmulg

Description: A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses mhmmulg.b 
|- B = ( Base ` G )
mhmmulg.s 
|- .x. = ( .g ` G )
mhmmulg.t 
|- .X. = ( .g ` H )
Assertion mhmmulg 
|- ( ( F e. ( G MndHom H ) /\ N e. NN0 /\ X e. B ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )

Proof

Step Hyp Ref Expression
1 mhmmulg.b 
 |-  B = ( Base ` G )
2 mhmmulg.s 
 |-  .x. = ( .g ` G )
3 mhmmulg.t 
 |-  .X. = ( .g ` H )
4 fvoveq1 
 |-  ( n = 0 -> ( F ` ( n .x. X ) ) = ( F ` ( 0 .x. X ) ) )
5 oveq1 
 |-  ( n = 0 -> ( n .X. ( F ` X ) ) = ( 0 .X. ( F ` X ) ) )
6 4 5 eqeq12d 
 |-  ( n = 0 -> ( ( F ` ( n .x. X ) ) = ( n .X. ( F ` X ) ) <-> ( F ` ( 0 .x. X ) ) = ( 0 .X. ( F ` X ) ) ) )
7 6 imbi2d 
 |-  ( n = 0 -> ( ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( n .x. X ) ) = ( n .X. ( F ` X ) ) ) <-> ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( 0 .x. X ) ) = ( 0 .X. ( F ` X ) ) ) ) )
8 fvoveq1 
 |-  ( n = m -> ( F ` ( n .x. X ) ) = ( F ` ( m .x. X ) ) )
9 oveq1 
 |-  ( n = m -> ( n .X. ( F ` X ) ) = ( m .X. ( F ` X ) ) )
10 8 9 eqeq12d 
 |-  ( n = m -> ( ( F ` ( n .x. X ) ) = ( n .X. ( F ` X ) ) <-> ( F ` ( m .x. X ) ) = ( m .X. ( F ` X ) ) ) )
11 10 imbi2d 
 |-  ( n = m -> ( ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( n .x. X ) ) = ( n .X. ( F ` X ) ) ) <-> ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( m .x. X ) ) = ( m .X. ( F ` X ) ) ) ) )
12 fvoveq1 
 |-  ( n = ( m + 1 ) -> ( F ` ( n .x. X ) ) = ( F ` ( ( m + 1 ) .x. X ) ) )
13 oveq1 
 |-  ( n = ( m + 1 ) -> ( n .X. ( F ` X ) ) = ( ( m + 1 ) .X. ( F ` X ) ) )
14 12 13 eqeq12d 
 |-  ( n = ( m + 1 ) -> ( ( F ` ( n .x. X ) ) = ( n .X. ( F ` X ) ) <-> ( F ` ( ( m + 1 ) .x. X ) ) = ( ( m + 1 ) .X. ( F ` X ) ) ) )
15 14 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( n .x. X ) ) = ( n .X. ( F ` X ) ) ) <-> ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( ( m + 1 ) .x. X ) ) = ( ( m + 1 ) .X. ( F ` X ) ) ) ) )
16 fvoveq1 
 |-  ( n = N -> ( F ` ( n .x. X ) ) = ( F ` ( N .x. X ) ) )
17 oveq1 
 |-  ( n = N -> ( n .X. ( F ` X ) ) = ( N .X. ( F ` X ) ) )
18 16 17 eqeq12d 
 |-  ( n = N -> ( ( F ` ( n .x. X ) ) = ( n .X. ( F ` X ) ) <-> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) ) )
19 18 imbi2d 
 |-  ( n = N -> ( ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( n .x. X ) ) = ( n .X. ( F ` X ) ) ) <-> ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) ) ) )
20 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
21 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
22 20 21 mhm0 
 |-  ( F e. ( G MndHom H ) -> ( F ` ( 0g ` G ) ) = ( 0g ` H ) )
23 22 adantr 
 |-  ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( 0g ` G ) ) = ( 0g ` H ) )
24 1 20 2 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
25 24 adantl 
 |-  ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( 0 .x. X ) = ( 0g ` G ) )
26 25 fveq2d 
 |-  ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( 0 .x. X ) ) = ( F ` ( 0g ` G ) ) )
27 eqid 
 |-  ( Base ` H ) = ( Base ` H )
28 1 27 mhmf 
 |-  ( F e. ( G MndHom H ) -> F : B --> ( Base ` H ) )
29 28 ffvelcdmda 
 |-  ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` X ) e. ( Base ` H ) )
30 27 21 3 mulg0 
 |-  ( ( F ` X ) e. ( Base ` H ) -> ( 0 .X. ( F ` X ) ) = ( 0g ` H ) )
31 29 30 syl 
 |-  ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( 0 .X. ( F ` X ) ) = ( 0g ` H ) )
32 23 26 31 3eqtr4d 
 |-  ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( 0 .x. X ) ) = ( 0 .X. ( F ` X ) ) )
33 oveq1 
 |-  ( ( F ` ( m .x. X ) ) = ( m .X. ( F ` X ) ) -> ( ( F ` ( m .x. X ) ) ( +g ` H ) ( F ` X ) ) = ( ( m .X. ( F ` X ) ) ( +g ` H ) ( F ` X ) ) )
34 mhmrcl1 
 |-  ( F e. ( G MndHom H ) -> G e. Mnd )
35 34 ad2antrr 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> G e. Mnd )
36 simpr 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> m e. NN0 )
37 simplr 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> X e. B )
38 eqid 
 |-  ( +g ` G ) = ( +g ` G )
39 1 2 38 mulgnn0p1 
 |-  ( ( G e. Mnd /\ m e. NN0 /\ X e. B ) -> ( ( m + 1 ) .x. X ) = ( ( m .x. X ) ( +g ` G ) X ) )
40 35 36 37 39 syl3anc 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> ( ( m + 1 ) .x. X ) = ( ( m .x. X ) ( +g ` G ) X ) )
41 40 fveq2d 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> ( F ` ( ( m + 1 ) .x. X ) ) = ( F ` ( ( m .x. X ) ( +g ` G ) X ) ) )
42 simpll 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> F e. ( G MndHom H ) )
43 34 ad2antrr 
 |-  ( ( ( F e. ( G MndHom H ) /\ m e. NN0 ) /\ X e. B ) -> G e. Mnd )
44 simplr 
 |-  ( ( ( F e. ( G MndHom H ) /\ m e. NN0 ) /\ X e. B ) -> m e. NN0 )
45 simpr 
 |-  ( ( ( F e. ( G MndHom H ) /\ m e. NN0 ) /\ X e. B ) -> X e. B )
46 1 2 43 44 45 mulgnn0cld 
 |-  ( ( ( F e. ( G MndHom H ) /\ m e. NN0 ) /\ X e. B ) -> ( m .x. X ) e. B )
47 46 an32s 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> ( m .x. X ) e. B )
48 eqid 
 |-  ( +g ` H ) = ( +g ` H )
49 1 38 48 mhmlin 
 |-  ( ( F e. ( G MndHom H ) /\ ( m .x. X ) e. B /\ X e. B ) -> ( F ` ( ( m .x. X ) ( +g ` G ) X ) ) = ( ( F ` ( m .x. X ) ) ( +g ` H ) ( F ` X ) ) )
50 42 47 37 49 syl3anc 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> ( F ` ( ( m .x. X ) ( +g ` G ) X ) ) = ( ( F ` ( m .x. X ) ) ( +g ` H ) ( F ` X ) ) )
51 41 50 eqtrd 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> ( F ` ( ( m + 1 ) .x. X ) ) = ( ( F ` ( m .x. X ) ) ( +g ` H ) ( F ` X ) ) )
52 mhmrcl2 
 |-  ( F e. ( G MndHom H ) -> H e. Mnd )
53 52 ad2antrr 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> H e. Mnd )
54 29 adantr 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> ( F ` X ) e. ( Base ` H ) )
55 27 3 48 mulgnn0p1 
 |-  ( ( H e. Mnd /\ m e. NN0 /\ ( F ` X ) e. ( Base ` H ) ) -> ( ( m + 1 ) .X. ( F ` X ) ) = ( ( m .X. ( F ` X ) ) ( +g ` H ) ( F ` X ) ) )
56 53 36 54 55 syl3anc 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> ( ( m + 1 ) .X. ( F ` X ) ) = ( ( m .X. ( F ` X ) ) ( +g ` H ) ( F ` X ) ) )
57 51 56 eqeq12d 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> ( ( F ` ( ( m + 1 ) .x. X ) ) = ( ( m + 1 ) .X. ( F ` X ) ) <-> ( ( F ` ( m .x. X ) ) ( +g ` H ) ( F ` X ) ) = ( ( m .X. ( F ` X ) ) ( +g ` H ) ( F ` X ) ) ) )
58 33 57 imbitrrid 
 |-  ( ( ( F e. ( G MndHom H ) /\ X e. B ) /\ m e. NN0 ) -> ( ( F ` ( m .x. X ) ) = ( m .X. ( F ` X ) ) -> ( F ` ( ( m + 1 ) .x. X ) ) = ( ( m + 1 ) .X. ( F ` X ) ) ) )
59 58 expcom 
 |-  ( m e. NN0 -> ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( ( F ` ( m .x. X ) ) = ( m .X. ( F ` X ) ) -> ( F ` ( ( m + 1 ) .x. X ) ) = ( ( m + 1 ) .X. ( F ` X ) ) ) ) )
60 59 a2d 
 |-  ( m e. NN0 -> ( ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( m .x. X ) ) = ( m .X. ( F ` X ) ) ) -> ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( ( m + 1 ) .x. X ) ) = ( ( m + 1 ) .X. ( F ` X ) ) ) ) )
61 7 11 15 19 32 60 nn0ind 
 |-  ( N e. NN0 -> ( ( F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) ) )
62 61 3impib 
 |-  ( ( N e. NN0 /\ F e. ( G MndHom H ) /\ X e. B ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )
63 62 3com12 
 |-  ( ( F e. ( G MndHom H ) /\ N e. NN0 /\ X e. B ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )