Metamath Proof Explorer

Theorem submaeval

Description: An entry of a submatrix of a square matrix. (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 submaeval ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ I ∈ N ∖ K ∧ J ∈ N ∖ L → I K Q ⁡ M L J = 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 2 3 submaval ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → K Q ⁡ M L = i ∈ N ∖ K , j ∈ N ∖ L ⟼ i M j
5 4 3expb ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → K Q ⁡ M L = i ∈ N ∖ K , j ∈ N ∖ L ⟼ i M j
6 5 3adant3 ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ I ∈ N ∖ K ∧ J ∈ N ∖ L → K Q ⁡ M L = i ∈ N ∖ K , j ∈ N ∖ L ⟼ i M j
7 simp3l ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ I ∈ N ∖ K ∧ J ∈ N ∖ L → I ∈ N ∖ K
8 simpl3r ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ I ∈ N ∖ K ∧ J ∈ N ∖ L ∧ i = I → J ∈ N ∖ L
9 ovexd ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ I ∈ N ∖ K ∧ J ∈ N ∖ L ∧ i = I ∧ j = J → i M j ∈ V
10 oveq12 ⊢ i = I ∧ j = J → i M j = I M J
11 10 adantl ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ I ∈ N ∖ K ∧ J ∈ N ∖ L ∧ i = I ∧ j = J → i M j = I M J
12 7 8 9 11 ovmpodv2 ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ I ∈ N ∖ K ∧ J ∈ N ∖ L → K Q ⁡ M L = i ∈ N ∖ K , j ∈ N ∖ L ⟼ i M j → I K Q ⁡ M L J = I M J
13 6 12 mpd ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ I ∈ N ∖ K ∧ J ∈ N ∖ L → I K Q ⁡ M L J = I M J