Step |
Hyp |
Ref |
Expression |
1 |
|
zrrhm.b |
|- B = ( Base ` T ) |
2 |
|
zrrhm.0 |
|- .0. = ( 0g ` S ) |
3 |
|
zrrhm.h |
|- H = ( x e. B |-> .0. ) |
4 |
|
c0snmhm.z |
|- Z = ( 0g ` T ) |
5 |
|
pm3.22 |
|- ( ( S e. Mnd /\ T e. Mnd ) -> ( T e. Mnd /\ S e. Mnd ) ) |
6 |
5
|
3adant3 |
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> ( T e. Mnd /\ S e. Mnd ) ) |
7 |
|
simp1 |
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> S e. Mnd ) |
8 |
|
mndmgm |
|- ( T e. Mnd -> T e. Mgm ) |
9 |
8
|
3ad2ant2 |
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> T e. Mgm ) |
10 |
|
fveq2 |
|- ( B = { Z } -> ( # ` B ) = ( # ` { Z } ) ) |
11 |
4
|
fvexi |
|- Z e. _V |
12 |
|
hashsng |
|- ( Z e. _V -> ( # ` { Z } ) = 1 ) |
13 |
11 12
|
ax-mp |
|- ( # ` { Z } ) = 1 |
14 |
10 13
|
eqtrdi |
|- ( B = { Z } -> ( # ` B ) = 1 ) |
15 |
14
|
3ad2ant3 |
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> ( # ` B ) = 1 ) |
16 |
1 2 3
|
c0snmgmhm |
|- ( ( S e. Mnd /\ T e. Mgm /\ ( # ` B ) = 1 ) -> H e. ( T MgmHom S ) ) |
17 |
7 9 15 16
|
syl3anc |
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> H e. ( T MgmHom S ) ) |
18 |
3
|
a1i |
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> H = ( x e. B |-> .0. ) ) |
19 |
|
eqidd |
|- ( ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) /\ x = Z ) -> .0. = .0. ) |
20 |
11
|
snid |
|- Z e. { Z } |
21 |
|
eleq2 |
|- ( B = { Z } -> ( Z e. B <-> Z e. { Z } ) ) |
22 |
20 21
|
mpbiri |
|- ( B = { Z } -> Z e. B ) |
23 |
22
|
3ad2ant3 |
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> Z e. B ) |
24 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
25 |
24 2
|
mndidcl |
|- ( S e. Mnd -> .0. e. ( Base ` S ) ) |
26 |
25
|
3ad2ant1 |
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> .0. e. ( Base ` S ) ) |
27 |
18 19 23 26
|
fvmptd |
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> ( H ` Z ) = .0. ) |
28 |
17 27
|
jca |
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> ( H e. ( T MgmHom S ) /\ ( H ` Z ) = .0. ) ) |
29 |
|
eqid |
|- ( +g ` T ) = ( +g ` T ) |
30 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
31 |
1 24 29 30 4 2
|
ismhm0 |
|- ( H e. ( T MndHom S ) <-> ( ( T e. Mnd /\ S e. Mnd ) /\ ( H e. ( T MgmHom S ) /\ ( H ` Z ) = .0. ) ) ) |
32 |
6 28 31
|
sylanbrc |
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> H e. ( T MndHom S ) ) |