Metamath Proof Explorer

Theorem submafval

Description: First 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 submafval ⊢ Q = m ∈ B ⟼ 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 oveq12 ⊢ n = N ∧ r = R → n Mat r = N Mat R
5 4 1 eqtr4di ⊢ n = N ∧ r = R → n Mat r = A
6 5 fveq2d ⊢ n = N ∧ r = R → Base n Mat r = Base A
7 6 3 eqtr4di ⊢ n = N ∧ r = R → Base n Mat r = B
8 simpl ⊢ n = N ∧ r = R → n = N
9 difeq1 ⊢ n = N → n ∖ k = N ∖ k
10 9 adantr ⊢ n = N ∧ r = R → n ∖ k = N ∖ k
11 difeq1 ⊢ n = N → n ∖ l = N ∖ l
12 11 adantr ⊢ n = N ∧ r = R → n ∖ l = N ∖ l
13 eqidd ⊢ n = N ∧ r = R → i m j = i m j
14 10 12 13 mpoeq123dv ⊢ n = N ∧ r = R → i ∈ n ∖ k , j ∈ n ∖ l ⟼ i m j = i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j
15 8 8 14 mpoeq123dv ⊢ n = N ∧ r = R → 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
16 7 15 mpteq12dv ⊢ n = N ∧ r = R → m ∈ Base n Mat r ⟼ k ∈ n , l ∈ n ⟼ i ∈ n ∖ k , j ∈ n ∖ l ⟼ i m j = m ∈ B ⟼ k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j
17 df-subma ⊢ subMat = n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r ⟼ k ∈ n , l ∈ n ⟼ i ∈ n ∖ k , j ∈ n ∖ l ⟼ i m j
18 3 fvexi ⊢ B ∈ V
19 18 mptex ⊢ m ∈ B ⟼ k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j ∈ V
20 16 17 19 ovmpoa ⊢ N ∈ V ∧ R ∈ V → N subMat R = m ∈ B ⟼ k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j
21 17 mpondm0 ⊢ ¬ N ∈ V ∧ R ∈ V → N subMat R = ∅
22 mpt0 ⊢ m ∈ ∅ ⟼ k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j = ∅
23 21 22 eqtr4di ⊢ ¬ N ∈ V ∧ R ∈ V → N subMat R = m ∈ ∅ ⟼ k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j
24 1 fveq2i ⊢ Base A = Base N Mat R
25 3 24 eqtri ⊢ B = Base N Mat R
26 matbas0pc ⊢ ¬ N ∈ V ∧ R ∈ V → Base N Mat R = ∅
27 25 26 syl5eq ⊢ ¬ N ∈ V ∧ R ∈ V → B = ∅
28 27 mpteq1d ⊢ ¬ N ∈ V ∧ R ∈ V → m ∈ B ⟼ k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j = m ∈ ∅ ⟼ k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j
29 23 28 eqtr4d ⊢ ¬ N ∈ V ∧ R ∈ V → N subMat R = m ∈ B ⟼ k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j
30 20 29 pm2.61i ⊢ N subMat R = m ∈ B ⟼ k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j
31 2 30 eqtri ⊢ Q = m ∈ B ⟼ k ∈ N , l ∈ N ⟼ i ∈ N ∖ k , j ∈ N ∖ l ⟼ i m j