Proof of Theorem mpomatmul
| Step | Hyp | Ref
| Expression |
| 1 | | mpomatmul.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ Fin) |
| 2 | | mpomatmul.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
| 3 | | mpomatmul.a |
. . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 4 | | eqid 2737 |
. . . . . . 7
⊢ (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) |
| 5 | 3, 4 | matmulr 22444 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (.r‘𝐴)) |
| 6 | | mpomatmul.m |
. . . . . 6
⊢ × =
(.r‘𝐴) |
| 7 | 5, 6 | eqtr4di 2795 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = × ) |
| 8 | 7 | oveqd 7448 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑋(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑌) = (𝑋 × 𝑌)) |
| 9 | 8 | eqcomd 2743 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑋 × 𝑌) = (𝑋(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑌)) |
| 10 | 1, 2, 9 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝑋 × 𝑌) = (𝑋(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑌)) |
| 11 | | eqid 2737 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 12 | | mpomatmul.t |
. . 3
⊢ · =
(.r‘𝑅) |
| 13 | | mpomatmul.x |
. . . . 5
⊢ 𝑋 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝐶) |
| 14 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐴) =
(Base‘𝐴) |
| 15 | | mpomatmul.c |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐶 ∈ 𝐵) |
| 16 | | mpomatmul.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
| 17 | 15, 16 | eleqtrdi 2851 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐶 ∈ (Base‘𝑅)) |
| 18 | 3, 11, 14, 1, 2, 17 | matbas2d 22429 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝐶) ∈ (Base‘𝐴)) |
| 19 | 13, 18 | eqeltrid 2845 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴)) |
| 20 | 3, 11 | matbas2 22427 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → ((Base‘𝑅) ↑m (𝑁 × 𝑁)) = (Base‘𝐴)) |
| 21 | 1, 2, 20 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ((Base‘𝑅) ↑m (𝑁 × 𝑁)) = (Base‘𝐴)) |
| 22 | 19, 21 | eleqtrrd 2844 |
. . 3
⊢ (𝜑 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
| 23 | | mpomatmul.y |
. . . . 5
⊢ 𝑌 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝐸) |
| 24 | | mpomatmul.e |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐸 ∈ 𝐵) |
| 25 | 24, 16 | eleqtrdi 2851 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐸 ∈ (Base‘𝑅)) |
| 26 | 3, 11, 14, 1, 2, 25 | matbas2d 22429 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝐸) ∈ (Base‘𝐴)) |
| 27 | 23, 26 | eqeltrid 2845 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ (Base‘𝐴)) |
| 28 | 27, 21 | eleqtrrd 2844 |
. . 3
⊢ (𝜑 → 𝑌 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
| 29 | 4, 11, 12, 2, 1, 1,
1, 22, 28 | mamuval 22397 |
. 2
⊢ (𝜑 → (𝑋(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑌) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑋𝑚) · (𝑚𝑌𝑙)))))) |
| 30 | 13 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑋 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝐶)) |
| 31 | | equcom 2017 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 ↔ 𝑘 = 𝑖) |
| 32 | | equcom 2017 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑚 ↔ 𝑚 = 𝑗) |
| 33 | 31, 32 | anbi12i 628 |
. . . . . . . . . . . . 13
⊢ ((𝑖 = 𝑘 ∧ 𝑗 = 𝑚) ↔ (𝑘 = 𝑖 ∧ 𝑚 = 𝑗)) |
| 34 | | mpomatmul.d |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 = 𝑖 ∧ 𝑚 = 𝑗)) → 𝐷 = 𝐶) |
| 35 | 33, 34 | sylan2b 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 = 𝑘 ∧ 𝑗 = 𝑚)) → 𝐷 = 𝐶) |
| 36 | 35 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 = 𝑘 ∧ 𝑗 = 𝑚)) → 𝐶 = 𝐷) |
| 37 | 36 | ex 412 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑖 = 𝑘 ∧ 𝑗 = 𝑚) → 𝐶 = 𝐷)) |
| 38 | 37 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → ((𝑖 = 𝑘 ∧ 𝑗 = 𝑚) → 𝐶 = 𝐷)) |
| 39 | 38 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → ((𝑖 = 𝑘 ∧ 𝑗 = 𝑚) → 𝐶 = 𝐷)) |
| 40 | 39 | imp 406 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) ∧ (𝑖 = 𝑘 ∧ 𝑗 = 𝑚)) → 𝐶 = 𝐷) |
| 41 | | simpl2 1193 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
| 42 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑚 ∈ 𝑁) |
| 43 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝜑) |
| 44 | | mpomatmul.1 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑚 ∈ 𝑁) → 𝐷 ∈ 𝑈) |
| 45 | 43, 41, 42, 44 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝐷 ∈ 𝑈) |
| 46 | 30, 40, 41, 42, 45 | ovmpod 7585 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (𝑘𝑋𝑚) = 𝐷) |
| 47 | 23 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑌 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝐸)) |
| 48 | | equcomi 2016 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑚 → 𝑚 = 𝑖) |
| 49 | | equcomi 2016 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑙 → 𝑙 = 𝑗) |
| 50 | 48, 49 | anim12i 613 |
. . . . . . . . . . . . 13
⊢ ((𝑖 = 𝑚 ∧ 𝑗 = 𝑙) → (𝑚 = 𝑖 ∧ 𝑙 = 𝑗)) |
| 51 | | mpomatmul.f |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 = 𝑖 ∧ 𝑙 = 𝑗)) → 𝐹 = 𝐸) |
| 52 | 50, 51 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 = 𝑚 ∧ 𝑗 = 𝑙)) → 𝐹 = 𝐸) |
| 53 | 52 | ex 412 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑖 = 𝑚 ∧ 𝑗 = 𝑙) → 𝐹 = 𝐸)) |
| 54 | 53 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → ((𝑖 = 𝑚 ∧ 𝑗 = 𝑙) → 𝐹 = 𝐸)) |
| 55 | 54 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → ((𝑖 = 𝑚 ∧ 𝑗 = 𝑙) → 𝐹 = 𝐸)) |
| 56 | 55 | imp 406 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) ∧ (𝑖 = 𝑚 ∧ 𝑗 = 𝑙)) → 𝐹 = 𝐸) |
| 57 | 56 | eqcomd 2743 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) ∧ (𝑖 = 𝑚 ∧ 𝑗 = 𝑙)) → 𝐸 = 𝐹) |
| 58 | | simpl3 1194 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑙 ∈ 𝑁) |
| 59 | | mpomatmul.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝐹 ∈ 𝑊) |
| 60 | 43, 42, 58, 59 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝐹 ∈ 𝑊) |
| 61 | 47, 57, 42, 58, 60 | ovmpod 7585 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (𝑚𝑌𝑙) = 𝐹) |
| 62 | 46, 61 | oveq12d 7449 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → ((𝑘𝑋𝑚) · (𝑚𝑌𝑙)) = (𝐷 · 𝐹)) |
| 63 | 62 | mpteq2dva 5242 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑚 ∈ 𝑁 ↦ ((𝑘𝑋𝑚) · (𝑚𝑌𝑙))) = (𝑚 ∈ 𝑁 ↦ (𝐷 · 𝐹))) |
| 64 | 63 | oveq2d 7447 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑋𝑚) · (𝑚𝑌𝑙)))) = (𝑅 Σg (𝑚 ∈ 𝑁 ↦ (𝐷 · 𝐹)))) |
| 65 | 64 | mpoeq3dva 7510 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑋𝑚) · (𝑚𝑌𝑙))))) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ (𝐷 · 𝐹))))) |
| 66 | 10, 29, 65 | 3eqtrd 2781 |
1
⊢ (𝜑 → (𝑋 × 𝑌) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ (𝐷 · 𝐹))))) |