Metamath Proof Explorer


Theorem mhmvlin

Description: Tuple extension of monoid homomorphisms. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses mhmvlin.b
|- B = ( Base ` M )
mhmvlin.p
|- .+ = ( +g ` M )
mhmvlin.q
|- .+^ = ( +g ` N )
Assertion mhmvlin
|- ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> ( F o. ( X oF .+ Y ) ) = ( ( F o. X ) oF .+^ ( F o. Y ) ) )

Proof

Step Hyp Ref Expression
1 mhmvlin.b
 |-  B = ( Base ` M )
2 mhmvlin.p
 |-  .+ = ( +g ` M )
3 mhmvlin.q
 |-  .+^ = ( +g ` N )
4 simpl1
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) /\ y e. I ) -> F e. ( M MndHom N ) )
5 elmapi
 |-  ( X e. ( B ^m I ) -> X : I --> B )
6 5 3ad2ant2
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> X : I --> B )
7 6 ffvelrnda
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) /\ y e. I ) -> ( X ` y ) e. B )
8 elmapi
 |-  ( Y e. ( B ^m I ) -> Y : I --> B )
9 8 3ad2ant3
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> Y : I --> B )
10 9 ffvelrnda
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) /\ y e. I ) -> ( Y ` y ) e. B )
11 1 2 3 mhmlin
 |-  ( ( F e. ( M MndHom N ) /\ ( X ` y ) e. B /\ ( Y ` y ) e. B ) -> ( F ` ( ( X ` y ) .+ ( Y ` y ) ) ) = ( ( F ` ( X ` y ) ) .+^ ( F ` ( Y ` y ) ) ) )
12 4 7 10 11 syl3anc
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) /\ y e. I ) -> ( F ` ( ( X ` y ) .+ ( Y ` y ) ) ) = ( ( F ` ( X ` y ) ) .+^ ( F ` ( Y ` y ) ) ) )
13 12 mpteq2dva
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> ( y e. I |-> ( F ` ( ( X ` y ) .+ ( Y ` y ) ) ) ) = ( y e. I |-> ( ( F ` ( X ` y ) ) .+^ ( F ` ( Y ` y ) ) ) ) )
14 mhmrcl1
 |-  ( F e. ( M MndHom N ) -> M e. Mnd )
15 14 adantr
 |-  ( ( F e. ( M MndHom N ) /\ y e. I ) -> M e. Mnd )
16 15 3ad2antl1
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) /\ y e. I ) -> M e. Mnd )
17 1 2 mndcl
 |-  ( ( M e. Mnd /\ ( X ` y ) e. B /\ ( Y ` y ) e. B ) -> ( ( X ` y ) .+ ( Y ` y ) ) e. B )
18 16 7 10 17 syl3anc
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) /\ y e. I ) -> ( ( X ` y ) .+ ( Y ` y ) ) e. B )
19 elmapex
 |-  ( Y e. ( B ^m I ) -> ( B e. _V /\ I e. _V ) )
20 19 simprd
 |-  ( Y e. ( B ^m I ) -> I e. _V )
21 20 3ad2ant3
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> I e. _V )
22 6 feqmptd
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> X = ( y e. I |-> ( X ` y ) ) )
23 9 feqmptd
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> Y = ( y e. I |-> ( Y ` y ) ) )
24 21 7 10 22 23 offval2
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> ( X oF .+ Y ) = ( y e. I |-> ( ( X ` y ) .+ ( Y ` y ) ) ) )
25 eqid
 |-  ( Base ` N ) = ( Base ` N )
26 1 25 mhmf
 |-  ( F e. ( M MndHom N ) -> F : B --> ( Base ` N ) )
27 26 3ad2ant1
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> F : B --> ( Base ` N ) )
28 27 feqmptd
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> F = ( z e. B |-> ( F ` z ) ) )
29 fveq2
 |-  ( z = ( ( X ` y ) .+ ( Y ` y ) ) -> ( F ` z ) = ( F ` ( ( X ` y ) .+ ( Y ` y ) ) ) )
30 18 24 28 29 fmptco
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> ( F o. ( X oF .+ Y ) ) = ( y e. I |-> ( F ` ( ( X ` y ) .+ ( Y ` y ) ) ) ) )
31 fvexd
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) /\ y e. I ) -> ( F ` ( X ` y ) ) e. _V )
32 fvexd
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) /\ y e. I ) -> ( F ` ( Y ` y ) ) e. _V )
33 fcompt
 |-  ( ( F : B --> ( Base ` N ) /\ X : I --> B ) -> ( F o. X ) = ( y e. I |-> ( F ` ( X ` y ) ) ) )
34 27 6 33 syl2anc
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> ( F o. X ) = ( y e. I |-> ( F ` ( X ` y ) ) ) )
35 fcompt
 |-  ( ( F : B --> ( Base ` N ) /\ Y : I --> B ) -> ( F o. Y ) = ( y e. I |-> ( F ` ( Y ` y ) ) ) )
36 27 9 35 syl2anc
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> ( F o. Y ) = ( y e. I |-> ( F ` ( Y ` y ) ) ) )
37 21 31 32 34 36 offval2
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> ( ( F o. X ) oF .+^ ( F o. Y ) ) = ( y e. I |-> ( ( F ` ( X ` y ) ) .+^ ( F ` ( Y ` y ) ) ) ) )
38 13 30 37 3eqtr4d
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> ( F o. ( X oF .+ Y ) ) = ( ( F o. X ) oF .+^ ( F o. Y ) ) )