Metamath Proof Explorer

Theorem submaval

Description: Third 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 submaval ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → K Q ⁡ M L = 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 2 3 submaval0 ⊢ M ∈ B → Q ⁡ M = k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j
5 4 3ad2ant1 ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → Q ⁡ M = k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j
6 simp2 ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → K ∈ N
7 simpl3 ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ k = K → L ∈ N
8 1 3 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
9 8 simpld ⊢ M ∈ B → N ∈ Fin
10 diffi ⊢ N ∈ Fin → N ∖ k ∈ Fin
11 9 10 syl ⊢ M ∈ B → N ∖ k ∈ Fin
12 diffi ⊢ N ∈ Fin → N ∖ l ∈ Fin
13 9 12 syl ⊢ M ∈ B → N ∖ l ∈ Fin
14 11 13 jca ⊢ M ∈ B → N ∖ k ∈ Fin ∧ N ∖ l ∈ Fin
15 14 3ad2ant1 ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → N ∖ k ∈ Fin ∧ N ∖ l ∈ Fin
16 15 adantr ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ k = K ∧ l = L → N ∖ k ∈ Fin ∧ N ∖ l ∈ Fin
17 mpoexga ⊢ N ∖ k ∈ Fin ∧ N ∖ l ∈ Fin → i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j ∈ V
18 16 17 syl ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ k = K ∧ l = L → i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j ∈ V
19 sneq ⊢ k = K → k = K
20 19 difeq2d ⊢ k = K → N ∖ k = N ∖ K
21 20 adantr ⊢ k = K ∧ l = L → N ∖ k = N ∖ K
22 sneq ⊢ l = L → l = L
23 22 difeq2d ⊢ l = L → N ∖ l = N ∖ L
24 23 adantl ⊢ k = K ∧ l = L → N ∖ l = N ∖ L
25 eqidd ⊢ k = K ∧ l = L → i M j = i M j
26 21 24 25 mpoeq123dv ⊢ k = K ∧ l = L → i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j = i ∈ N ∖ K , j ∈ N ∖ L ⟼ i M j
27 26 adantl ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ k = K ∧ l = L → i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j = i ∈ N ∖ K , j ∈ N ∖ L ⟼ i M j
28 6 7 18 27 ovmpodv2 ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → Q ⁡ M = k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i M j → K Q ⁡ M L = i ∈ N ∖ K , j ∈ N ∖ L ⟼ i M j
29 5 28 mpd ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → K Q ⁡ M L = i ∈ N ∖ K , j ∈ N ∖ L ⟼ i M j