Metamath Proof Explorer

Theorem marepvfval

Description: First substitution for the definition of the function replacing a column of a matrix by a vector. (Contributed by AV, 14-Feb-2019) (Revised by AV, 26-Feb-2019) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses marepvfval.a ⊢ A = N Mat R
marepvfval.b ⊢ B = Base A
marepvfval.q ⊢ Q = N matRepV R
marepvfval.v ⊢ V = Base R N
Assertion marepvfval ⊢ Q = m ∈ B , v ∈ V ⟼ k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j

Proof

Step Hyp Ref Expression
1 marepvfval.a ⊢ A = N Mat R
2 marepvfval.b ⊢ B = Base A
3 marepvfval.q ⊢ Q = N matRepV R
4 marepvfval.v ⊢ V = Base R N
5 2 fvexi ⊢ B ∈ V
6 4 ovexi ⊢ V ∈ V
7 6 a1i ⊢ N ∈ V ∧ R ∈ V → V ∈ V
8 mpoexga ⊢ B ∈ V ∧ V ∈ V → m ∈ B , v ∈ V ⟼ k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j ∈ V
9 5 7 8 sylancr ⊢ N ∈ V ∧ R ∈ V → m ∈ B , v ∈ V ⟼ k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j ∈ V
10 oveq12 ⊢ n = N ∧ r = R → n Mat r = N Mat R
11 10 1 eqtr4di ⊢ n = N ∧ r = R → n Mat r = A
12 11 fveq2d ⊢ n = N ∧ r = R → Base n Mat r = Base A
13 12 2 eqtr4di ⊢ n = N ∧ r = R → Base n Mat r = B
14 fveq2 ⊢ r = R → Base r = Base R
15 14 adantl ⊢ n = N ∧ r = R → Base r = Base R
16 simpl ⊢ n = N ∧ r = R → n = N
17 15 16 oveq12d ⊢ n = N ∧ r = R → Base r n = Base R N
18 17 4 eqtr4di ⊢ n = N ∧ r = R → Base r n = V
19 eqidd ⊢ n = N ∧ r = R → if j = k v ⁡ i i m j = if j = k v ⁡ i i m j
20 16 16 19 mpoeq123dv ⊢ n = N ∧ r = R → i ∈ n , j ∈ n ⟼ if j = k v ⁡ i i m j = i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j
21 16 20 mpteq12dv ⊢ n = N ∧ r = R → k ∈ n ⟼ i ∈ n , j ∈ n ⟼ if j = k v ⁡ i i m j = k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j
22 13 18 21 mpoeq123dv ⊢ n = N ∧ r = R → m ∈ Base n Mat r , v ∈ Base r n ⟼ k ∈ n ⟼ i ∈ n , j ∈ n ⟼ if j = k v ⁡ i i m j = m ∈ B , v ∈ V ⟼ k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j
23 df-marepv ⊢ matRepV = n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r , v ∈ Base r n ⟼ k ∈ n ⟼ i ∈ n , j ∈ n ⟼ if j = k v ⁡ i i m j
24 22 23 ovmpoga ⊢ N ∈ V ∧ R ∈ V ∧ m ∈ B , v ∈ V ⟼ k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j ∈ V → N matRepV R = m ∈ B , v ∈ V ⟼ k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j
25 9 24 mpd3an3 ⊢ N ∈ V ∧ R ∈ V → N matRepV R = m ∈ B , v ∈ V ⟼ k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j
26 23 mpondm0 ⊢ ¬ N ∈ V ∧ R ∈ V → N matRepV R = ∅
27 1 fveq2i ⊢ Base A = Base N Mat R
28 2 27 eqtri ⊢ B = Base N Mat R
29 matbas0pc ⊢ ¬ N ∈ V ∧ R ∈ V → Base N Mat R = ∅
30 28 29 eqtrid ⊢ ¬ N ∈ V ∧ R ∈ V → B = ∅
31 30 orcd ⊢ ¬ N ∈ V ∧ R ∈ V → B = ∅ ∨ V = ∅
32 0mpo0 ⊢ B = ∅ ∨ V = ∅ → m ∈ B , v ∈ V ⟼ k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j = ∅
33 31 32 syl ⊢ ¬ N ∈ V ∧ R ∈ V → m ∈ B , v ∈ V ⟼ k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j = ∅
34 26 33 eqtr4d ⊢ ¬ N ∈ V ∧ R ∈ V → N matRepV R = m ∈ B , v ∈ V ⟼ k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j
35 25 34 pm2.61i ⊢ N matRepV R = m ∈ B , v ∈ V ⟼ k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j
36 3 35 eqtri ⊢ Q = m ∈ B , v ∈ V ⟼ k ∈ N ⟼ i ∈ N , j ∈ N ⟼ if j = k v ⁡ i i m j