Step |
Hyp |
Ref |
Expression |
1 |
|
resmhm2.u |
|- U = ( T |`s X ) |
2 |
|
mhmrcl1 |
|- ( F e. ( S MndHom U ) -> S e. Mnd ) |
3 |
|
submrcl |
|- ( X e. ( SubMnd ` T ) -> T e. Mnd ) |
4 |
2 3
|
anim12i |
|- ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> ( S e. Mnd /\ T e. Mnd ) ) |
5 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
6 |
|
eqid |
|- ( Base ` U ) = ( Base ` U ) |
7 |
5 6
|
mhmf |
|- ( F e. ( S MndHom U ) -> F : ( Base ` S ) --> ( Base ` U ) ) |
8 |
1
|
submbas |
|- ( X e. ( SubMnd ` T ) -> X = ( Base ` U ) ) |
9 |
|
eqid |
|- ( Base ` T ) = ( Base ` T ) |
10 |
9
|
submss |
|- ( X e. ( SubMnd ` T ) -> X C_ ( Base ` T ) ) |
11 |
8 10
|
eqsstrrd |
|- ( X e. ( SubMnd ` T ) -> ( Base ` U ) C_ ( Base ` T ) ) |
12 |
|
fss |
|- ( ( F : ( Base ` S ) --> ( Base ` U ) /\ ( Base ` U ) C_ ( Base ` T ) ) -> F : ( Base ` S ) --> ( Base ` T ) ) |
13 |
7 11 12
|
syl2an |
|- ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> F : ( Base ` S ) --> ( Base ` T ) ) |
14 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
15 |
|
eqid |
|- ( +g ` U ) = ( +g ` U ) |
16 |
5 14 15
|
mhmlin |
|- ( ( F e. ( S MndHom U ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) ) |
17 |
16
|
3expb |
|- ( ( F e. ( S MndHom U ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) ) |
18 |
17
|
adantlr |
|- ( ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) ) |
19 |
|
eqid |
|- ( +g ` T ) = ( +g ` T ) |
20 |
1 19
|
ressplusg |
|- ( X e. ( SubMnd ` T ) -> ( +g ` T ) = ( +g ` U ) ) |
21 |
20
|
ad2antlr |
|- ( ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( +g ` T ) = ( +g ` U ) ) |
22 |
21
|
oveqd |
|- ( ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( ( F ` x ) ( +g ` T ) ( F ` y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) ) |
23 |
18 22
|
eqtr4d |
|- ( ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) ) |
24 |
23
|
ralrimivva |
|- ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) ) |
25 |
|
eqid |
|- ( 0g ` S ) = ( 0g ` S ) |
26 |
|
eqid |
|- ( 0g ` U ) = ( 0g ` U ) |
27 |
25 26
|
mhm0 |
|- ( F e. ( S MndHom U ) -> ( F ` ( 0g ` S ) ) = ( 0g ` U ) ) |
28 |
27
|
adantr |
|- ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> ( F ` ( 0g ` S ) ) = ( 0g ` U ) ) |
29 |
|
eqid |
|- ( 0g ` T ) = ( 0g ` T ) |
30 |
1 29
|
subm0 |
|- ( X e. ( SubMnd ` T ) -> ( 0g ` T ) = ( 0g ` U ) ) |
31 |
30
|
adantl |
|- ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> ( 0g ` T ) = ( 0g ` U ) ) |
32 |
28 31
|
eqtr4d |
|- ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) |
33 |
13 24 32
|
3jca |
|- ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> ( F : ( Base ` S ) --> ( Base ` T ) /\ A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) |
34 |
5 9 14 19 25 29
|
ismhm |
|- ( F e. ( S MndHom T ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( F : ( Base ` S ) --> ( Base ` T ) /\ A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) ) |
35 |
4 33 34
|
sylanbrc |
|- ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> F e. ( S MndHom T ) ) |