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 |
|
mndmgm |
|- ( S e. Mnd -> S e. Mgm ) |
5 |
4
|
anim1i |
|- ( ( S e. Mnd /\ T e. Mgm ) -> ( S e. Mgm /\ T e. Mgm ) ) |
6 |
5
|
3adant3 |
|- ( ( S e. Mnd /\ T e. Mgm /\ ( # ` B ) = 1 ) -> ( S e. Mgm /\ T e. Mgm ) ) |
7 |
6
|
ancomd |
|- ( ( S e. Mnd /\ T e. Mgm /\ ( # ` B ) = 1 ) -> ( T e. Mgm /\ S e. Mgm ) ) |
8 |
1
|
fvexi |
|- B e. _V |
9 |
|
hash1snb |
|- ( B e. _V -> ( ( # ` B ) = 1 <-> E. b B = { b } ) ) |
10 |
8 9
|
ax-mp |
|- ( ( # ` B ) = 1 <-> E. b B = { b } ) |
11 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
12 |
11 2
|
mndidcl |
|- ( S e. Mnd -> .0. e. ( Base ` S ) ) |
13 |
12
|
adantr |
|- ( ( S e. Mnd /\ T e. Mgm ) -> .0. e. ( Base ` S ) ) |
14 |
13
|
adantr |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> .0. e. ( Base ` S ) ) |
15 |
14
|
adantr |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ x e. B ) -> .0. e. ( Base ` S ) ) |
16 |
15 3
|
fmptd |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> H : B --> ( Base ` S ) ) |
17 |
3
|
a1i |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> H = ( x e. B |-> .0. ) ) |
18 |
|
eqidd |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ x = b ) -> .0. = .0. ) |
19 |
|
vsnid |
|- b e. { b } |
20 |
19
|
a1i |
|- ( B = { b } -> b e. { b } ) |
21 |
|
eleq2 |
|- ( B = { b } -> ( b e. B <-> b e. { b } ) ) |
22 |
20 21
|
mpbird |
|- ( B = { b } -> b e. B ) |
23 |
22
|
adantl |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> b e. B ) |
24 |
17 18 23 14
|
fvmptd |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( H ` b ) = .0. ) |
25 |
|
simpr |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ ( H ` b ) = .0. ) -> ( H ` b ) = .0. ) |
26 |
25 25
|
oveq12d |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ ( H ` b ) = .0. ) -> ( ( H ` b ) ( +g ` S ) ( H ` b ) ) = ( .0. ( +g ` S ) .0. ) ) |
27 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
28 |
11 27 2
|
mndlid |
|- ( ( S e. Mnd /\ .0. e. ( Base ` S ) ) -> ( .0. ( +g ` S ) .0. ) = .0. ) |
29 |
12 28
|
mpdan |
|- ( S e. Mnd -> ( .0. ( +g ` S ) .0. ) = .0. ) |
30 |
29
|
adantr |
|- ( ( S e. Mnd /\ T e. Mgm ) -> ( .0. ( +g ` S ) .0. ) = .0. ) |
31 |
30
|
adantr |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( .0. ( +g ` S ) .0. ) = .0. ) |
32 |
31
|
adantr |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ ( H ` b ) = .0. ) -> ( .0. ( +g ` S ) .0. ) = .0. ) |
33 |
|
simpr |
|- ( ( S e. Mnd /\ T e. Mgm ) -> T e. Mgm ) |
34 |
33
|
adantr |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> T e. Mgm ) |
35 |
34
|
adantr |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ b e. B ) -> T e. Mgm ) |
36 |
|
simpr |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ b e. B ) -> b e. B ) |
37 |
|
eqid |
|- ( +g ` T ) = ( +g ` T ) |
38 |
1 37
|
mgmcl |
|- ( ( T e. Mgm /\ b e. B /\ b e. B ) -> ( b ( +g ` T ) b ) e. B ) |
39 |
35 36 36 38
|
syl3anc |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ b e. B ) -> ( b ( +g ` T ) b ) e. B ) |
40 |
|
eleq2 |
|- ( B = { b } -> ( ( b ( +g ` T ) b ) e. B <-> ( b ( +g ` T ) b ) e. { b } ) ) |
41 |
|
elsni |
|- ( ( b ( +g ` T ) b ) e. { b } -> ( b ( +g ` T ) b ) = b ) |
42 |
40 41
|
syl6bi |
|- ( B = { b } -> ( ( b ( +g ` T ) b ) e. B -> ( b ( +g ` T ) b ) = b ) ) |
43 |
42
|
adantl |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( ( b ( +g ` T ) b ) e. B -> ( b ( +g ` T ) b ) = b ) ) |
44 |
43
|
adantr |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ b e. B ) -> ( ( b ( +g ` T ) b ) e. B -> ( b ( +g ` T ) b ) = b ) ) |
45 |
39 44
|
mpd |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ b e. B ) -> ( b ( +g ` T ) b ) = b ) |
46 |
23 45
|
mpdan |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( b ( +g ` T ) b ) = b ) |
47 |
46
|
fveq2d |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( H ` ( b ( +g ` T ) b ) ) = ( H ` b ) ) |
48 |
47
|
adantr |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ ( H ` b ) = .0. ) -> ( H ` ( b ( +g ` T ) b ) ) = ( H ` b ) ) |
49 |
48 25
|
eqtr2d |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ ( H ` b ) = .0. ) -> .0. = ( H ` ( b ( +g ` T ) b ) ) ) |
50 |
26 32 49
|
3eqtrrd |
|- ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ ( H ` b ) = .0. ) -> ( H ` ( b ( +g ` T ) b ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) ) |
51 |
24 50
|
mpdan |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( H ` ( b ( +g ` T ) b ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) ) |
52 |
|
id |
|- ( B = { b } -> B = { b } ) |
53 |
52
|
raleqdv |
|- ( B = { b } -> ( A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> A. c e. { b } ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) |
54 |
52 53
|
raleqbidv |
|- ( B = { b } -> ( A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> A. a e. { b } A. c e. { b } ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) |
55 |
54
|
adantl |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> A. a e. { b } A. c e. { b } ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) |
56 |
|
fvoveq1 |
|- ( a = b -> ( H ` ( a ( +g ` T ) c ) ) = ( H ` ( b ( +g ` T ) c ) ) ) |
57 |
|
fveq2 |
|- ( a = b -> ( H ` a ) = ( H ` b ) ) |
58 |
57
|
oveq1d |
|- ( a = b -> ( ( H ` a ) ( +g ` S ) ( H ` c ) ) = ( ( H ` b ) ( +g ` S ) ( H ` c ) ) ) |
59 |
56 58
|
eqeq12d |
|- ( a = b -> ( ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> ( H ` ( b ( +g ` T ) c ) ) = ( ( H ` b ) ( +g ` S ) ( H ` c ) ) ) ) |
60 |
|
oveq2 |
|- ( c = b -> ( b ( +g ` T ) c ) = ( b ( +g ` T ) b ) ) |
61 |
60
|
fveq2d |
|- ( c = b -> ( H ` ( b ( +g ` T ) c ) ) = ( H ` ( b ( +g ` T ) b ) ) ) |
62 |
|
fveq2 |
|- ( c = b -> ( H ` c ) = ( H ` b ) ) |
63 |
62
|
oveq2d |
|- ( c = b -> ( ( H ` b ) ( +g ` S ) ( H ` c ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) ) |
64 |
61 63
|
eqeq12d |
|- ( c = b -> ( ( H ` ( b ( +g ` T ) c ) ) = ( ( H ` b ) ( +g ` S ) ( H ` c ) ) <-> ( H ` ( b ( +g ` T ) b ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) ) ) |
65 |
59 64
|
2ralsng |
|- ( ( b e. _V /\ b e. _V ) -> ( A. a e. { b } A. c e. { b } ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> ( H ` ( b ( +g ` T ) b ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) ) ) |
66 |
65
|
el2v |
|- ( A. a e. { b } A. c e. { b } ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> ( H ` ( b ( +g ` T ) b ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) ) |
67 |
55 66
|
syl6bb |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> ( H ` ( b ( +g ` T ) b ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) ) ) |
68 |
51 67
|
mpbird |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) |
69 |
16 68
|
jca |
|- ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( H : B --> ( Base ` S ) /\ A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) |
70 |
69
|
ex |
|- ( ( S e. Mnd /\ T e. Mgm ) -> ( B = { b } -> ( H : B --> ( Base ` S ) /\ A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) ) |
71 |
70
|
exlimdv |
|- ( ( S e. Mnd /\ T e. Mgm ) -> ( E. b B = { b } -> ( H : B --> ( Base ` S ) /\ A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) ) |
72 |
10 71
|
syl5bi |
|- ( ( S e. Mnd /\ T e. Mgm ) -> ( ( # ` B ) = 1 -> ( H : B --> ( Base ` S ) /\ A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) ) |
73 |
72
|
3impia |
|- ( ( S e. Mnd /\ T e. Mgm /\ ( # ` B ) = 1 ) -> ( H : B --> ( Base ` S ) /\ A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) |
74 |
1 11 37 27
|
ismgmhm |
|- ( H e. ( T MgmHom S ) <-> ( ( T e. Mgm /\ S e. Mgm ) /\ ( H : B --> ( Base ` S ) /\ A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) ) |
75 |
7 73 74
|
sylanbrc |
|- ( ( S e. Mnd /\ T e. Mgm /\ ( # ` B ) = 1 ) -> H e. ( T MgmHom S ) ) |