Step | Hyp | Ref
| Expression |
1 | | submafval.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
2 | | submafval.q |
. . . 4
⊢ 𝑄 = (𝑁 subMat 𝑅) |
3 | | submafval.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
4 | 1, 2, 3 | submaval0 21331 |
. . 3
⊢ (𝑀 ∈ 𝐵 → (𝑄‘𝑀) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)))) |
5 | 4 | 3ad2ant1 1134 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑄‘𝑀) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)))) |
6 | | simp2 1138 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → 𝐾 ∈ 𝑁) |
7 | | simpl3 1194 |
. . 3
⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ 𝑘 = 𝐾) → 𝐿 ∈ 𝑁) |
8 | 1, 3 | matrcl 21163 |
. . . . . . . . 9
⊢ (𝑀 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
9 | 8 | simpld 498 |
. . . . . . . 8
⊢ (𝑀 ∈ 𝐵 → 𝑁 ∈ Fin) |
10 | | diffi 8827 |
. . . . . . . 8
⊢ (𝑁 ∈ Fin → (𝑁 ∖ {𝑘}) ∈ Fin) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → (𝑁 ∖ {𝑘}) ∈ Fin) |
12 | | diffi 8827 |
. . . . . . . 8
⊢ (𝑁 ∈ Fin → (𝑁 ∖ {𝑙}) ∈ Fin) |
13 | 9, 12 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → (𝑁 ∖ {𝑙}) ∈ Fin) |
14 | 11, 13 | jca 515 |
. . . . . 6
⊢ (𝑀 ∈ 𝐵 → ((𝑁 ∖ {𝑘}) ∈ Fin ∧ (𝑁 ∖ {𝑙}) ∈ Fin)) |
15 | 14 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → ((𝑁 ∖ {𝑘}) ∈ Fin ∧ (𝑁 ∖ {𝑙}) ∈ Fin)) |
16 | 15 | adantr 484 |
. . . 4
⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝑘 = 𝐾 ∧ 𝑙 = 𝐿)) → ((𝑁 ∖ {𝑘}) ∈ Fin ∧ (𝑁 ∖ {𝑙}) ∈ Fin)) |
17 | | mpoexga 7801 |
. . . 4
⊢ (((𝑁 ∖ {𝑘}) ∈ Fin ∧ (𝑁 ∖ {𝑙}) ∈ Fin) → (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)) ∈ V) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝑘 = 𝐾 ∧ 𝑙 = 𝐿)) → (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)) ∈ V) |
19 | | sneq 4526 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → {𝑘} = {𝐾}) |
20 | 19 | difeq2d 4013 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑁 ∖ {𝑘}) = (𝑁 ∖ {𝐾})) |
21 | 20 | adantr 484 |
. . . . 5
⊢ ((𝑘 = 𝐾 ∧ 𝑙 = 𝐿) → (𝑁 ∖ {𝑘}) = (𝑁 ∖ {𝐾})) |
22 | | sneq 4526 |
. . . . . . 7
⊢ (𝑙 = 𝐿 → {𝑙} = {𝐿}) |
23 | 22 | difeq2d 4013 |
. . . . . 6
⊢ (𝑙 = 𝐿 → (𝑁 ∖ {𝑙}) = (𝑁 ∖ {𝐿})) |
24 | 23 | adantl 485 |
. . . . 5
⊢ ((𝑘 = 𝐾 ∧ 𝑙 = 𝐿) → (𝑁 ∖ {𝑙}) = (𝑁 ∖ {𝐿})) |
25 | | eqidd 2739 |
. . . . 5
⊢ ((𝑘 = 𝐾 ∧ 𝑙 = 𝐿) → (𝑖𝑀𝑗) = (𝑖𝑀𝑗)) |
26 | 21, 24, 25 | mpoeq123dv 7243 |
. . . 4
⊢ ((𝑘 = 𝐾 ∧ 𝑙 = 𝐿) → (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝑀𝑗))) |
27 | 26 | adantl 485 |
. . 3
⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝑘 = 𝐾 ∧ 𝑙 = 𝐿)) → (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝑀𝑗))) |
28 | 6, 7, 18, 27 | ovmpodv2 7323 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → ((𝑄‘𝑀) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗))) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝑀𝑗)))) |
29 | 5, 28 | mpd 15 |
1
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝑀𝑗))) |