Step |
Hyp |
Ref |
Expression |
1 |
|
zrrhm.b |
⊢ 𝐵 = ( Base ‘ 𝑇 ) |
2 |
|
zrrhm.0 |
⊢ 0 = ( 0g ‘ 𝑆 ) |
3 |
|
zrrhm.h |
⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 ) |
4 |
|
mndmgm |
⊢ ( 𝑆 ∈ Mnd → 𝑆 ∈ Mgm ) |
5 |
4
|
anim1i |
⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ) |
6 |
5
|
3adant3 |
⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ) |
7 |
6
|
ancomd |
⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( 𝑇 ∈ Mgm ∧ 𝑆 ∈ Mgm ) ) |
8 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
9 |
|
hash1snb |
⊢ ( 𝐵 ∈ V → ( ( ♯ ‘ 𝐵 ) = 1 ↔ ∃ 𝑏 𝐵 = { 𝑏 } ) ) |
10 |
8 9
|
ax-mp |
⊢ ( ( ♯ ‘ 𝐵 ) = 1 ↔ ∃ 𝑏 𝐵 = { 𝑏 } ) |
11 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
12 |
11 2
|
mndidcl |
⊢ ( 𝑆 ∈ Mnd → 0 ∈ ( Base ‘ 𝑆 ) ) |
13 |
12
|
adantr |
⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → 0 ∈ ( Base ‘ 𝑆 ) ) |
14 |
13
|
adantr |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → 0 ∈ ( Base ‘ 𝑆 ) ) |
15 |
14
|
adantr |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑥 ∈ 𝐵 ) → 0 ∈ ( Base ‘ 𝑆 ) ) |
16 |
15 3
|
fmptd |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ) |
17 |
3
|
a1i |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 ) ) |
18 |
|
eqidd |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑥 = 𝑏 ) → 0 = 0 ) |
19 |
|
vsnid |
⊢ 𝑏 ∈ { 𝑏 } |
20 |
19
|
a1i |
⊢ ( 𝐵 = { 𝑏 } → 𝑏 ∈ { 𝑏 } ) |
21 |
|
eleq2 |
⊢ ( 𝐵 = { 𝑏 } → ( 𝑏 ∈ 𝐵 ↔ 𝑏 ∈ { 𝑏 } ) ) |
22 |
20 21
|
mpbird |
⊢ ( 𝐵 = { 𝑏 } → 𝑏 ∈ 𝐵 ) |
23 |
22
|
adantl |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → 𝑏 ∈ 𝐵 ) |
24 |
17 18 23 14
|
fvmptd |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( 𝐻 ‘ 𝑏 ) = 0 ) |
25 |
|
simpr |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ ( 𝐻 ‘ 𝑏 ) = 0 ) → ( 𝐻 ‘ 𝑏 ) = 0 ) |
26 |
25 25
|
oveq12d |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ ( 𝐻 ‘ 𝑏 ) = 0 ) → ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) = ( 0 ( +g ‘ 𝑆 ) 0 ) ) |
27 |
|
eqid |
⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 ) |
28 |
11 27 2
|
mndlid |
⊢ ( ( 𝑆 ∈ Mnd ∧ 0 ∈ ( Base ‘ 𝑆 ) ) → ( 0 ( +g ‘ 𝑆 ) 0 ) = 0 ) |
29 |
12 28
|
mpdan |
⊢ ( 𝑆 ∈ Mnd → ( 0 ( +g ‘ 𝑆 ) 0 ) = 0 ) |
30 |
29
|
adantr |
⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → ( 0 ( +g ‘ 𝑆 ) 0 ) = 0 ) |
31 |
30
|
adantr |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( 0 ( +g ‘ 𝑆 ) 0 ) = 0 ) |
32 |
31
|
adantr |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ ( 𝐻 ‘ 𝑏 ) = 0 ) → ( 0 ( +g ‘ 𝑆 ) 0 ) = 0 ) |
33 |
|
simpr |
⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → 𝑇 ∈ Mgm ) |
34 |
33
|
adantr |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → 𝑇 ∈ Mgm ) |
35 |
34
|
adantr |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑏 ∈ 𝐵 ) → 𝑇 ∈ Mgm ) |
36 |
|
simpr |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 ) |
37 |
|
eqid |
⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 ) |
38 |
1 37
|
mgmcl |
⊢ ( ( 𝑇 ∈ Mgm ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ 𝐵 ) |
39 |
35 36 36 38
|
syl3anc |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ 𝐵 ) |
40 |
|
eleq2 |
⊢ ( 𝐵 = { 𝑏 } → ( ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ 𝐵 ↔ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ { 𝑏 } ) ) |
41 |
|
elsni |
⊢ ( ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ { 𝑏 } → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) = 𝑏 ) |
42 |
40 41
|
syl6bi |
⊢ ( 𝐵 = { 𝑏 } → ( ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ 𝐵 → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) = 𝑏 ) ) |
43 |
42
|
adantl |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ 𝐵 → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) = 𝑏 ) ) |
44 |
43
|
adantr |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ∈ 𝐵 → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) = 𝑏 ) ) |
45 |
39 44
|
mpd |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) = 𝑏 ) |
46 |
23 45
|
mpdan |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) = 𝑏 ) |
47 |
46
|
fveq2d |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( 𝐻 ‘ 𝑏 ) ) |
48 |
47
|
adantr |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ ( 𝐻 ‘ 𝑏 ) = 0 ) → ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( 𝐻 ‘ 𝑏 ) ) |
49 |
48 25
|
eqtr2d |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ ( 𝐻 ‘ 𝑏 ) = 0 ) → 0 = ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) ) |
50 |
26 32 49
|
3eqtrrd |
⊢ ( ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) ∧ ( 𝐻 ‘ 𝑏 ) = 0 ) → ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) ) |
51 |
24 50
|
mpdan |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) ) |
52 |
|
id |
⊢ ( 𝐵 = { 𝑏 } → 𝐵 = { 𝑏 } ) |
53 |
52
|
raleqdv |
⊢ ( 𝐵 = { 𝑏 } → ( ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ∀ 𝑐 ∈ { 𝑏 } ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) |
54 |
52 53
|
raleqbidv |
⊢ ( 𝐵 = { 𝑏 } → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ∀ 𝑎 ∈ { 𝑏 } ∀ 𝑐 ∈ { 𝑏 } ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) |
55 |
54
|
adantl |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ∀ 𝑎 ∈ { 𝑏 } ∀ 𝑐 ∈ { 𝑏 } ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) |
56 |
|
fvoveq1 |
⊢ ( 𝑎 = 𝑏 → ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑐 ) ) ) |
57 |
|
fveq2 |
⊢ ( 𝑎 = 𝑏 → ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) ) |
58 |
57
|
oveq1d |
⊢ ( 𝑎 = 𝑏 → ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) |
59 |
56 58
|
eqeq12d |
⊢ ( 𝑎 = 𝑏 → ( ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) |
60 |
|
oveq2 |
⊢ ( 𝑐 = 𝑏 → ( 𝑏 ( +g ‘ 𝑇 ) 𝑐 ) = ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) |
61 |
60
|
fveq2d |
⊢ ( 𝑐 = 𝑏 → ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) ) |
62 |
|
fveq2 |
⊢ ( 𝑐 = 𝑏 → ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑏 ) ) |
63 |
62
|
oveq2d |
⊢ ( 𝑐 = 𝑏 → ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) ) |
64 |
61 63
|
eqeq12d |
⊢ ( 𝑐 = 𝑏 → ( ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) ) ) |
65 |
59 64
|
2ralsng |
⊢ ( ( 𝑏 ∈ V ∧ 𝑏 ∈ V ) → ( ∀ 𝑎 ∈ { 𝑏 } ∀ 𝑐 ∈ { 𝑏 } ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) ) ) |
66 |
65
|
el2v |
⊢ ( ∀ 𝑎 ∈ { 𝑏 } ∀ 𝑐 ∈ { 𝑏 } ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) ) |
67 |
55 66
|
syl6bb |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐻 ‘ ( 𝑏 ( +g ‘ 𝑇 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑏 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑏 ) ) ) ) |
68 |
51 67
|
mpbird |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) |
69 |
16 68
|
jca |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) ∧ 𝐵 = { 𝑏 } ) → ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) |
70 |
69
|
ex |
⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → ( 𝐵 = { 𝑏 } → ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) ) |
71 |
70
|
exlimdv |
⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → ( ∃ 𝑏 𝐵 = { 𝑏 } → ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) ) |
72 |
10 71
|
syl5bi |
⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ) → ( ( ♯ ‘ 𝐵 ) = 1 → ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) ) |
73 |
72
|
3impia |
⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) |
74 |
1 11 37 27
|
ismgmhm |
⊢ ( 𝐻 ∈ ( 𝑇 MgmHom 𝑆 ) ↔ ( ( 𝑇 ∈ Mgm ∧ 𝑆 ∈ Mgm ) ∧ ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑇 ) 𝑐 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑆 ) ( 𝐻 ‘ 𝑐 ) ) ) ) ) |
75 |
7 73 74
|
sylanbrc |
⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐻 ∈ ( 𝑇 MgmHom 𝑆 ) ) |