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 ) ) )