Step | Hyp | Ref
| Expression |
1 | | simpl1 1057 |
. . . 4
⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) ∧ 𝑦 ∈ 𝐼) → 𝐹 ∈ (𝑀 MndHom 𝑁)) |
2 | | elmapi 7765 |
. . . . . 6
⊢ (𝑋 ∈ (𝐵 ↑𝑚 𝐼) → 𝑋:𝐼⟶𝐵) |
3 | 2 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → 𝑋:𝐼⟶𝐵) |
4 | 3 | ffvelrnda 6267 |
. . . 4
⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) ∧ 𝑦 ∈ 𝐼) → (𝑋‘𝑦) ∈ 𝐵) |
5 | | elmapi 7765 |
. . . . . 6
⊢ (𝑌 ∈ (𝐵 ↑𝑚 𝐼) → 𝑌:𝐼⟶𝐵) |
6 | 5 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → 𝑌:𝐼⟶𝐵) |
7 | 6 | ffvelrnda 6267 |
. . . 4
⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) ∧ 𝑦 ∈ 𝐼) → (𝑌‘𝑦) ∈ 𝐵) |
8 | | mhmvlin.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑀) |
9 | | mhmvlin.p |
. . . . 5
⊢ + =
(+g‘𝑀) |
10 | | mhmvlin.q |
. . . . 5
⊢ ⨣ =
(+g‘𝑁) |
11 | 8, 9, 10 | mhmlin 17165 |
. . . 4
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ (𝑋‘𝑦) ∈ 𝐵 ∧ (𝑌‘𝑦) ∈ 𝐵) → (𝐹‘((𝑋‘𝑦) + (𝑌‘𝑦))) = ((𝐹‘(𝑋‘𝑦)) ⨣ (𝐹‘(𝑌‘𝑦)))) |
12 | 1, 4, 7, 11 | syl3anc 1318 |
. . 3
⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) ∧ 𝑦 ∈ 𝐼) → (𝐹‘((𝑋‘𝑦) + (𝑌‘𝑦))) = ((𝐹‘(𝑋‘𝑦)) ⨣ (𝐹‘(𝑌‘𝑦)))) |
13 | 12 | mpteq2dva 4672 |
. 2
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → (𝑦 ∈ 𝐼 ↦ (𝐹‘((𝑋‘𝑦) + (𝑌‘𝑦)))) = (𝑦 ∈ 𝐼 ↦ ((𝐹‘(𝑋‘𝑦)) ⨣ (𝐹‘(𝑌‘𝑦))))) |
14 | | mhmrcl1 17161 |
. . . . . 6
⊢ (𝐹 ∈ (𝑀 MndHom 𝑁) → 𝑀 ∈ Mnd) |
15 | 14 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑦 ∈ 𝐼) → 𝑀 ∈ Mnd) |
16 | 15 | 3ad2antl1 1216 |
. . . 4
⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) ∧ 𝑦 ∈ 𝐼) → 𝑀 ∈ Mnd) |
17 | 8, 9 | mndcl 17124 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ (𝑋‘𝑦) ∈ 𝐵 ∧ (𝑌‘𝑦) ∈ 𝐵) → ((𝑋‘𝑦) + (𝑌‘𝑦)) ∈ 𝐵) |
18 | 16, 4, 7, 17 | syl3anc 1318 |
. . 3
⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) ∧ 𝑦 ∈ 𝐼) → ((𝑋‘𝑦) + (𝑌‘𝑦)) ∈ 𝐵) |
19 | | elmapex 7764 |
. . . . . 6
⊢ (𝑌 ∈ (𝐵 ↑𝑚 𝐼) → (𝐵 ∈ V ∧ 𝐼 ∈ V)) |
20 | 19 | simprd 478 |
. . . . 5
⊢ (𝑌 ∈ (𝐵 ↑𝑚 𝐼) → 𝐼 ∈ V) |
21 | 20 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → 𝐼 ∈ V) |
22 | 3 | feqmptd 6159 |
. . . 4
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → 𝑋 = (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦))) |
23 | 6 | feqmptd 6159 |
. . . 4
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → 𝑌 = (𝑦 ∈ 𝐼 ↦ (𝑌‘𝑦))) |
24 | 21, 4, 7, 22, 23 | offval2 6812 |
. . 3
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → (𝑋 ∘𝑓 + 𝑌) = (𝑦 ∈ 𝐼 ↦ ((𝑋‘𝑦) + (𝑌‘𝑦)))) |
25 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑁) =
(Base‘𝑁) |
26 | 8, 25 | mhmf 17163 |
. . . . 5
⊢ (𝐹 ∈ (𝑀 MndHom 𝑁) → 𝐹:𝐵⟶(Base‘𝑁)) |
27 | 26 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → 𝐹:𝐵⟶(Base‘𝑁)) |
28 | 27 | feqmptd 6159 |
. . 3
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → 𝐹 = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))) |
29 | | fveq2 6103 |
. . 3
⊢ (𝑧 = ((𝑋‘𝑦) + (𝑌‘𝑦)) → (𝐹‘𝑧) = (𝐹‘((𝑋‘𝑦) + (𝑌‘𝑦)))) |
30 | 18, 24, 28, 29 | fmptco 6303 |
. 2
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → (𝐹 ∘ (𝑋 ∘𝑓 + 𝑌)) = (𝑦 ∈ 𝐼 ↦ (𝐹‘((𝑋‘𝑦) + (𝑌‘𝑦))))) |
31 | | fvex 6113 |
. . . 4
⊢ (𝐹‘(𝑋‘𝑦)) ∈ V |
32 | 31 | a1i 11 |
. . 3
⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) ∧ 𝑦 ∈ 𝐼) → (𝐹‘(𝑋‘𝑦)) ∈ V) |
33 | | fvex 6113 |
. . . 4
⊢ (𝐹‘(𝑌‘𝑦)) ∈ V |
34 | 33 | a1i 11 |
. . 3
⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) ∧ 𝑦 ∈ 𝐼) → (𝐹‘(𝑌‘𝑦)) ∈ V) |
35 | | fcompt 6306 |
. . . 4
⊢ ((𝐹:𝐵⟶(Base‘𝑁) ∧ 𝑋:𝐼⟶𝐵) → (𝐹 ∘ 𝑋) = (𝑦 ∈ 𝐼 ↦ (𝐹‘(𝑋‘𝑦)))) |
36 | 27, 3, 35 | syl2anc 691 |
. . 3
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → (𝐹 ∘ 𝑋) = (𝑦 ∈ 𝐼 ↦ (𝐹‘(𝑋‘𝑦)))) |
37 | | fcompt 6306 |
. . . 4
⊢ ((𝐹:𝐵⟶(Base‘𝑁) ∧ 𝑌:𝐼⟶𝐵) → (𝐹 ∘ 𝑌) = (𝑦 ∈ 𝐼 ↦ (𝐹‘(𝑌‘𝑦)))) |
38 | 27, 6, 37 | syl2anc 691 |
. . 3
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → (𝐹 ∘ 𝑌) = (𝑦 ∈ 𝐼 ↦ (𝐹‘(𝑌‘𝑦)))) |
39 | 21, 32, 34, 36, 38 | offval2 6812 |
. 2
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → ((𝐹 ∘ 𝑋) ∘𝑓 ⨣ (𝐹 ∘ 𝑌)) = (𝑦 ∈ 𝐼 ↦ ((𝐹‘(𝑋‘𝑦)) ⨣ (𝐹‘(𝑌‘𝑦))))) |
40 | 13, 30, 39 | 3eqtr4d 2654 |
1
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑𝑚 𝐼) ∧ 𝑌 ∈ (𝐵 ↑𝑚 𝐼)) → (𝐹 ∘ (𝑋 ∘𝑓 + 𝑌)) = ((𝐹 ∘ 𝑋) ∘𝑓 ⨣ (𝐹 ∘ 𝑌))) |