Step |
Hyp |
Ref |
Expression |
1 |
|
ismhmd.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
2 |
|
ismhmd.c |
⊢ 𝐶 = ( Base ‘ 𝑇 ) |
3 |
|
ismhmd.p |
⊢ + = ( +g ‘ 𝑆 ) |
4 |
|
ismhmd.q |
⊢ ⨣ = ( +g ‘ 𝑇 ) |
5 |
|
ismhmd.0 |
⊢ 0 = ( 0g ‘ 𝑆 ) |
6 |
|
ismhmd.z |
⊢ 𝑍 = ( 0g ‘ 𝑇 ) |
7 |
|
ismhmd.s |
⊢ ( 𝜑 → 𝑆 ∈ Mnd ) |
8 |
|
ismhmd.t |
⊢ ( 𝜑 → 𝑇 ∈ Mnd ) |
9 |
|
ismhmd.f |
⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 ) |
10 |
|
ismhmd.a |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) |
11 |
|
ismhmd.h |
⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 𝑍 ) |
12 |
10
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) |
13 |
9 12 11
|
3jca |
⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑍 ) ) |
14 |
1 2 3 4 5 6
|
ismhm |
⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑍 ) ) ) |
15 |
7 8 13 14
|
syl21anbrc |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) |