Step | Hyp | Ref
| Expression |
1 | | id 22 |
. 2
⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) → (𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd)) |
2 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑁) =
(Base‘𝑁) |
3 | | 0mhm.z |
. . . . . 6
⊢ 0 =
(0g‘𝑁) |
4 | 2, 3 | mndidcl 17308 |
. . . . 5
⊢ (𝑁 ∈ Mnd → 0 ∈
(Base‘𝑁)) |
5 | 4 | adantl 482 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) → 0 ∈
(Base‘𝑁)) |
6 | | fconst6g 6094 |
. . . 4
⊢ ( 0 ∈
(Base‘𝑁) →
(𝐵 × { 0 }):𝐵⟶(Base‘𝑁)) |
7 | 5, 6 | syl 17 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) → (𝐵 × { 0 }):𝐵⟶(Base‘𝑁)) |
8 | | simpr 477 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) → 𝑁 ∈ Mnd) |
9 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘𝑁) = (+g‘𝑁) |
10 | 2, 9, 3 | mndlid 17311 |
. . . . . . . 8
⊢ ((𝑁 ∈ Mnd ∧ 0 ∈
(Base‘𝑁)) → (
0
(+g‘𝑁)
0 ) =
0
) |
11 | 10 | eqcomd 2628 |
. . . . . . 7
⊢ ((𝑁 ∈ Mnd ∧ 0 ∈
(Base‘𝑁)) →
0 = (
0
(+g‘𝑁)
0
)) |
12 | 8, 5, 11 | syl2anc 693 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) → 0 = ( 0
(+g‘𝑁)
0
)) |
13 | 12 | adantr 481 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 0 = ( 0 (+g‘𝑁) 0 )) |
14 | | 0mhm.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑀) |
15 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘𝑀) = (+g‘𝑀) |
16 | 14, 15 | mndcl 17301 |
. . . . . . . 8
⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
17 | 16 | 3expb 1266 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
18 | 17 | adantlr 751 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
19 | | fvex 6201 |
. . . . . . . 8
⊢
(0g‘𝑁) ∈ V |
20 | 3, 19 | eqeltri 2697 |
. . . . . . 7
⊢ 0 ∈
V |
21 | 20 | fvconst2 6469 |
. . . . . 6
⊢ ((𝑥(+g‘𝑀)𝑦) ∈ 𝐵 → ((𝐵 × { 0 })‘(𝑥(+g‘𝑀)𝑦)) = 0 ) |
22 | 18, 21 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐵 × { 0 })‘(𝑥(+g‘𝑀)𝑦)) = 0 ) |
23 | 20 | fvconst2 6469 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 → ((𝐵 × { 0 })‘𝑥) = 0 ) |
24 | 20 | fvconst2 6469 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → ((𝐵 × { 0 })‘𝑦) = 0 ) |
25 | 23, 24 | oveqan12d 6669 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (((𝐵 × { 0 })‘𝑥)(+g‘𝑁)((𝐵 × { 0 })‘𝑦)) = ( 0 (+g‘𝑁) 0 )) |
26 | 25 | adantl 482 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((𝐵 × { 0 })‘𝑥)(+g‘𝑁)((𝐵 × { 0 })‘𝑦)) = ( 0 (+g‘𝑁) 0 )) |
27 | 13, 22, 26 | 3eqtr4d 2666 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐵 × { 0 })‘(𝑥(+g‘𝑀)𝑦)) = (((𝐵 × { 0 })‘𝑥)(+g‘𝑁)((𝐵 × { 0 })‘𝑦))) |
28 | 27 | ralrimivva 2971 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝐵 × { 0 })‘(𝑥(+g‘𝑀)𝑦)) = (((𝐵 × { 0 })‘𝑥)(+g‘𝑁)((𝐵 × { 0 })‘𝑦))) |
29 | | eqid 2622 |
. . . . . 6
⊢
(0g‘𝑀) = (0g‘𝑀) |
30 | 14, 29 | mndidcl 17308 |
. . . . 5
⊢ (𝑀 ∈ Mnd →
(0g‘𝑀)
∈ 𝐵) |
31 | 30 | adantr 481 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) →
(0g‘𝑀)
∈ 𝐵) |
32 | 20 | fvconst2 6469 |
. . . 4
⊢
((0g‘𝑀) ∈ 𝐵 → ((𝐵 × { 0
})‘(0g‘𝑀)) = 0 ) |
33 | 31, 32 | syl 17 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) → ((𝐵 × { 0
})‘(0g‘𝑀)) = 0 ) |
34 | 7, 28, 33 | 3jca 1242 |
. 2
⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) → ((𝐵 × { 0 }):𝐵⟶(Base‘𝑁) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝐵 × { 0 })‘(𝑥(+g‘𝑀)𝑦)) = (((𝐵 × { 0 })‘𝑥)(+g‘𝑁)((𝐵 × { 0 })‘𝑦)) ∧ ((𝐵 × { 0
})‘(0g‘𝑀)) = 0 )) |
35 | 14, 2, 15, 9, 29, 3 | ismhm 17337 |
. 2
⊢ ((𝐵 × { 0 }) ∈ (𝑀 MndHom 𝑁) ↔ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) ∧ ((𝐵 × { 0 }):𝐵⟶(Base‘𝑁) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝐵 × { 0 })‘(𝑥(+g‘𝑀)𝑦)) = (((𝐵 × { 0 })‘𝑥)(+g‘𝑁)((𝐵 × { 0 })‘𝑦)) ∧ ((𝐵 × { 0
})‘(0g‘𝑀)) = 0 ))) |
36 | 1, 34, 35 | sylanbrc 698 |
1
⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) → (𝐵 × { 0 }) ∈ (𝑀 MndHom 𝑁)) |