| Step | Hyp | Ref
| Expression |
| 1 | | submafval.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 2 | | submafval.q |
. . . 4
⊢ 𝑄 = (𝑁 subMat 𝑅) |
| 3 | | submafval.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
| 4 | 1, 2, 3 | submaval0 22586 |
. . 3
⊢ (𝑀 ∈ 𝐵 → (𝑄‘𝑀) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)))) |
| 5 | 4 | 3ad2ant1 1134 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑄‘𝑀) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)))) |
| 6 | | simp2 1138 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → 𝐾 ∈ 𝑁) |
| 7 | | simpl3 1194 |
. . 3
⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ 𝑘 = 𝐾) → 𝐿 ∈ 𝑁) |
| 8 | 1, 3 | matrcl 22416 |
. . . . . . . . 9
⊢ (𝑀 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
| 9 | 8 | simpld 494 |
. . . . . . . 8
⊢ (𝑀 ∈ 𝐵 → 𝑁 ∈ Fin) |
| 10 | | diffi 9215 |
. . . . . . . 8
⊢ (𝑁 ∈ Fin → (𝑁 ∖ {𝑘}) ∈ Fin) |
| 11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → (𝑁 ∖ {𝑘}) ∈ Fin) |
| 12 | | diffi 9215 |
. . . . . . . 8
⊢ (𝑁 ∈ Fin → (𝑁 ∖ {𝑙}) ∈ Fin) |
| 13 | 9, 12 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → (𝑁 ∖ {𝑙}) ∈ Fin) |
| 14 | 11, 13 | jca 511 |
. . . . . 6
⊢ (𝑀 ∈ 𝐵 → ((𝑁 ∖ {𝑘}) ∈ Fin ∧ (𝑁 ∖ {𝑙}) ∈ Fin)) |
| 15 | 14 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → ((𝑁 ∖ {𝑘}) ∈ Fin ∧ (𝑁 ∖ {𝑙}) ∈ Fin)) |
| 16 | 15 | adantr 480 |
. . . 4
⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝑘 = 𝐾 ∧ 𝑙 = 𝐿)) → ((𝑁 ∖ {𝑘}) ∈ Fin ∧ (𝑁 ∖ {𝑙}) ∈ Fin)) |
| 17 | | mpoexga 8102 |
. . . 4
⊢ (((𝑁 ∖ {𝑘}) ∈ Fin ∧ (𝑁 ∖ {𝑙}) ∈ Fin) → (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)) ∈ V) |
| 18 | 16, 17 | syl 17 |
. . 3
⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝑘 = 𝐾 ∧ 𝑙 = 𝐿)) → (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)) ∈ V) |
| 19 | | sneq 4636 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → {𝑘} = {𝐾}) |
| 20 | 19 | difeq2d 4126 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑁 ∖ {𝑘}) = (𝑁 ∖ {𝐾})) |
| 21 | 20 | adantr 480 |
. . . . 5
⊢ ((𝑘 = 𝐾 ∧ 𝑙 = 𝐿) → (𝑁 ∖ {𝑘}) = (𝑁 ∖ {𝐾})) |
| 22 | | sneq 4636 |
. . . . . . 7
⊢ (𝑙 = 𝐿 → {𝑙} = {𝐿}) |
| 23 | 22 | difeq2d 4126 |
. . . . . 6
⊢ (𝑙 = 𝐿 → (𝑁 ∖ {𝑙}) = (𝑁 ∖ {𝐿})) |
| 24 | 23 | adantl 481 |
. . . . 5
⊢ ((𝑘 = 𝐾 ∧ 𝑙 = 𝐿) → (𝑁 ∖ {𝑙}) = (𝑁 ∖ {𝐿})) |
| 25 | | eqidd 2738 |
. . . . 5
⊢ ((𝑘 = 𝐾 ∧ 𝑙 = 𝐿) → (𝑖𝑀𝑗) = (𝑖𝑀𝑗)) |
| 26 | 21, 24, 25 | mpoeq123dv 7508 |
. . . 4
⊢ ((𝑘 = 𝐾 ∧ 𝑙 = 𝐿) → (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝑀𝑗))) |
| 27 | 26 | adantl 481 |
. . 3
⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝑘 = 𝐾 ∧ 𝑙 = 𝐿)) → (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝑀𝑗))) |
| 28 | 6, 7, 18, 27 | ovmpodv2 7591 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → ((𝑄‘𝑀) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗))) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝑀𝑗)))) |
| 29 | 5, 28 | mpd 15 |
1
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝑀𝑗))) |