Metamath Proof Explorer

Theorem submaval0

Description: Second substitution for a submatrix. (Contributed by AV, 28-Dec-2018)

Ref Expression
Hypotheses submafval.a ⊢ A = N Mat R
submafval.q ⊢ Q = N subMat R
submafval.b ⊢ B = Base A
Assertion submaval0 ⊢ M ∈ B → Q ⁡ M = k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j

Proof

Step Hyp Ref Expression
1 submafval.a ⊢ A = N Mat R
2 submafval.q ⊢ Q = N subMat R
3 submafval.b ⊢ B = Base A
4 1 3 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
5 4 simpld ⊢ M ∈ B → N ∈ Fin
6 mpoexga ⊢ N ∈ Fin ∧ N ∈ Fin → k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j ∈ V
7 5 5 6 syl2anc ⊢ M ∈ B → k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j ∈ V
8 oveq ⊢ m = M → i m j = i M j
9 8 mpoeq3dv ⊢ m = M → i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j = i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j
10 9 mpoeq3dv ⊢ m = M → k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j = k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j
11 1 2 3 submafval ⊢ Q = m ∈ B ⟼ k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j
12 10 11 fvmptg ⊢ M ∈ B ∧ k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j ∈ V → Q ⁡ M = k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j
13 7 12 mpdan ⊢ M ∈ B → Q ⁡ M = k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j