Step | Hyp | Ref
| Expression |
1 | | mamures.i |
. . . 4
⊢ (𝜑 → 𝐼 ⊆ 𝑀) |
2 | | ssidd 3944 |
. . . 4
⊢ (𝜑 → 𝑃 ⊆ 𝑃) |
3 | | resmpo 7394 |
. . . 4
⊢ ((𝐼 ⊆ 𝑀 ∧ 𝑃 ⊆ 𝑃) → ((𝑖 ∈ 𝑀, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗))))) ↾ (𝐼 × 𝑃)) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))))) |
4 | 1, 2, 3 | syl2anc 584 |
. . 3
⊢ (𝜑 → ((𝑖 ∈ 𝑀, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗))))) ↾ (𝐼 × 𝑃)) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))))) |
5 | | ovres 7438 |
. . . . . . . . 9
⊢ ((𝑖 ∈ 𝐼 ∧ 𝑘 ∈ 𝑁) → (𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘) = (𝑖𝑋𝑘)) |
6 | 5 | 3ad2antl2 1185 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃) ∧ 𝑘 ∈ 𝑁) → (𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘) = (𝑖𝑋𝑘)) |
7 | 6 | eqcomd 2744 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃) ∧ 𝑘 ∈ 𝑁) → (𝑖𝑋𝑘) = (𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)) |
8 | 7 | oveq1d 7290 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃) ∧ 𝑘 ∈ 𝑁) → ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗)) = ((𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)(.r‘𝑅)(𝑘𝑌𝑗))) |
9 | 8 | mpteq2dva 5174 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃) → (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗))) = (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))) |
10 | 9 | oveq2d 7291 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝑃) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)(.r‘𝑅)(𝑘𝑌𝑗))))) |
11 | 10 | mpoeq3dva 7352 |
. . 3
⊢ (𝜑 → (𝑖 ∈ 𝐼, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗))))) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))))) |
12 | 4, 11 | eqtrd 2778 |
. 2
⊢ (𝜑 → ((𝑖 ∈ 𝑀, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗))))) ↾ (𝐼 × 𝑃)) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))))) |
13 | | mamures.f |
. . . 4
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) |
14 | | mamures.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
15 | | eqid 2738 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
16 | | mamures.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
17 | | mamures.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ Fin) |
18 | | mamures.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ Fin) |
19 | | mamures.p |
. . . 4
⊢ (𝜑 → 𝑃 ∈ Fin) |
20 | | mamures.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
21 | | mamures.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃))) |
22 | 13, 14, 15, 16, 17, 18, 19, 20, 21 | mamuval 21535 |
. . 3
⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑖 ∈ 𝑀, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))))) |
23 | 22 | reseq1d 5890 |
. 2
⊢ (𝜑 → ((𝑋𝐹𝑌) ↾ (𝐼 × 𝑃)) = ((𝑖 ∈ 𝑀, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑗))))) ↾ (𝐼 × 𝑃))) |
24 | | mamures.g |
. . 3
⊢ 𝐺 = (𝑅 maMul 〈𝐼, 𝑁, 𝑃〉) |
25 | 17, 1 | ssfid 9042 |
. . 3
⊢ (𝜑 → 𝐼 ∈ Fin) |
26 | | elmapi 8637 |
. . . . . 6
⊢ (𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)) → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
27 | 20, 26 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
28 | | xpss1 5608 |
. . . . . 6
⊢ (𝐼 ⊆ 𝑀 → (𝐼 × 𝑁) ⊆ (𝑀 × 𝑁)) |
29 | 1, 28 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐼 × 𝑁) ⊆ (𝑀 × 𝑁)) |
30 | 27, 29 | fssresd 6641 |
. . . 4
⊢ (𝜑 → (𝑋 ↾ (𝐼 × 𝑁)):(𝐼 × 𝑁)⟶𝐵) |
31 | 14 | fvexi 6788 |
. . . . . 6
⊢ 𝐵 ∈ V |
32 | 31 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ V) |
33 | | xpfi 9085 |
. . . . . 6
⊢ ((𝐼 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝐼 × 𝑁) ∈ Fin) |
34 | 25, 18, 33 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐼 × 𝑁) ∈ Fin) |
35 | 32, 34 | elmapd 8629 |
. . . 4
⊢ (𝜑 → ((𝑋 ↾ (𝐼 × 𝑁)) ∈ (𝐵 ↑m (𝐼 × 𝑁)) ↔ (𝑋 ↾ (𝐼 × 𝑁)):(𝐼 × 𝑁)⟶𝐵)) |
36 | 30, 35 | mpbird 256 |
. . 3
⊢ (𝜑 → (𝑋 ↾ (𝐼 × 𝑁)) ∈ (𝐵 ↑m (𝐼 × 𝑁))) |
37 | 24, 14, 15, 16, 25, 18, 19, 36, 21 | mamuval 21535 |
. 2
⊢ (𝜑 → ((𝑋 ↾ (𝐼 × 𝑁))𝐺𝑌) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑋 ↾ (𝐼 × 𝑁))𝑘)(.r‘𝑅)(𝑘𝑌𝑗)))))) |
38 | 12, 23, 37 | 3eqtr4d 2788 |
1
⊢ (𝜑 → ((𝑋𝐹𝑌) ↾ (𝐼 × 𝑃)) = ((𝑋 ↾ (𝐼 × 𝑁))𝐺𝑌)) |