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