Step | Hyp | Ref
| Expression |
1 | | mamures.i |
. . . 4
⊢ (𝜑 → 𝐼 ⊆ 𝑀) |
2 | | ssid 3624 |
. . . . 5
⊢ 𝑃 ⊆ 𝑃 |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑃 ⊆ 𝑃) |
4 | | resmpt2 6758 |
. . . 4
⊢ ((𝐼 ⊆ 𝑀 ∧ 𝑃 ⊆ 𝑃) → ((𝑖 ∈ 𝑀, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗))))) ↾ (𝐼 × 𝑃)) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))))) |
5 | 1, 3, 4 | syl2anc 693 |
. . 3
⊢ (𝜑 → ((𝑖 ∈ 𝑀, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗))))) ↾ (𝐼 × 𝑃)) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))))) |
6 | | ovres 6800 |
. . . . . . . . 9
⊢ ((𝑖 ∈ 𝐼 ∧ 𝑘 ∈ 𝑁) → (𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘) = (𝑖𝑋𝑘)) |
7 | 6 | 3ad2antl2 1224 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃) ∧ 𝑘 ∈ 𝑁) → (𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘) = (𝑖𝑋𝑘)) |
8 | 7 | eqcomd 2628 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃) ∧ 𝑘 ∈ 𝑁) → (𝑖𝑋𝑘) = (𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)) |
9 | 8 | oveq1d 6665 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃) ∧ 𝑘 ∈ 𝑁) → ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗)) = ((𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)(.r‘𝑅)(𝑘𝑌𝑗))) |
10 | 9 | mpteq2dva 4744 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃) → (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗))) = (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))) |
11 | 10 | oveq2d 6666 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)(.r‘𝑅)(𝑘𝑌𝑗))))) |
12 | 11 | mpt2eq3dva 6719 |
. . 3
⊢ (𝜑 → (𝑖 ∈ 𝐼, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗))))) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))))) |
13 | 5, 12 | eqtrd 2656 |
. 2
⊢ (𝜑 → ((𝑖 ∈ 𝑀, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗))))) ↾ (𝐼 × 𝑃)) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))))) |
14 | | mamures.f |
. . . 4
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) |
15 | | mamures.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
16 | | eqid 2622 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
17 | | mamures.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
18 | | mamures.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ Fin) |
19 | | mamures.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ Fin) |
20 | | mamures.p |
. . . 4
⊢ (𝜑 → 𝑃 ∈ Fin) |
21 | | mamures.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) |
22 | | mamures.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑃))) |
23 | 14, 15, 16, 17, 18, 19, 20, 21, 22 | mamuval 20192 |
. . 3
⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑖 ∈ 𝑀, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))))) |
24 | 23 | reseq1d 5395 |
. 2
⊢ (𝜑 → ((𝑋𝐹𝑌) ↾ (𝐼 × 𝑃)) = ((𝑖 ∈ 𝑀, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗))))) ↾ (𝐼 × 𝑃))) |
25 | | mamures.g |
. . 3
⊢ 𝐺 = (𝑅 maMul 〈𝐼, 𝑁, 𝑃〉) |
26 | | ssfi 8180 |
. . . 4
⊢ ((𝑀 ∈ Fin ∧ 𝐼 ⊆ 𝑀) → 𝐼 ∈ Fin) |
27 | 18, 1, 26 | syl2anc 693 |
. . 3
⊢ (𝜑 → 𝐼 ∈ Fin) |
28 | | elmapi 7879 |
. . . . . 6
⊢ (𝑋 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁)) → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
29 | 21, 28 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
30 | | xpss1 5228 |
. . . . . 6
⊢ (𝐼 ⊆ 𝑀 → (𝐼 × 𝑁) ⊆ (𝑀 × 𝑁)) |
31 | 1, 30 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐼 × 𝑁) ⊆ (𝑀 × 𝑁)) |
32 | 29, 31 | fssresd 6071 |
. . . 4
⊢ (𝜑 → (𝑋 ↾ (𝐼 × 𝑁)):(𝐼 × 𝑁)⟶𝐵) |
33 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝑅)
∈ V |
34 | 15, 33 | eqeltri 2697 |
. . . . . 6
⊢ 𝐵 ∈ V |
35 | 34 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ V) |
36 | | xpfi 8231 |
. . . . . 6
⊢ ((𝐼 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝐼 × 𝑁) ∈ Fin) |
37 | 27, 19, 36 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐼 × 𝑁) ∈ Fin) |
38 | 35, 37 | elmapd 7871 |
. . . 4
⊢ (𝜑 → ((𝑋 ↾ (𝐼 × 𝑁)) ∈ (𝐵 ↑𝑚 (𝐼 × 𝑁)) ↔ (𝑋 ↾ (𝐼 × 𝑁)):(𝐼 × 𝑁)⟶𝐵)) |
39 | 32, 38 | mpbird 247 |
. . 3
⊢ (𝜑 → (𝑋 ↾ (𝐼 × 𝑁)) ∈ (𝐵 ↑𝑚 (𝐼 × 𝑁))) |
40 | 25, 15, 16, 17, 27, 19, 20, 39, 22 | mamuval 20192 |
. 2
⊢ (𝜑 → ((𝑋 ↾ (𝐼 × 𝑁))𝐺𝑌) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))))) |
41 | 13, 24, 40 | 3eqtr4d 2666 |
1
⊢ (𝜑 → ((𝑋𝐹𝑌) ↾ (𝐼 × 𝑃)) = ((𝑋 ↾ (𝐼 × 𝑁))𝐺𝑌)) |