Metamath Proof Explorer

Theorem marrepval0

Description: Second substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019)

Ref Expression
Hypotheses marrepfval.a ⊢ A = N Mat R
marrepfval.b ⊢ B = Base A
marrepfval.q ⊢ Q = N matRRep R
marrepfval.z ⊢ 0 ˙ = 0 R
Assertion marrepval0 ⊢ M ∈ B ∧ S ∈ Base R → M Q S = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l S 0 ˙ i M j

Proof

Step Hyp Ref Expression
1 marrepfval.a ⊢ A = N Mat R
2 marrepfval.b ⊢ B = Base A
3 marrepfval.q ⊢ Q = N matRRep R
4 marrepfval.z ⊢ 0 ˙ = 0 R
5 1 2 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
6 5 simpld ⊢ M ∈ B → N ∈ Fin
7 6 6 jca ⊢ M ∈ B → N ∈ Fin ∧ N ∈ Fin
8 7 adantr ⊢ M ∈ B ∧ S ∈ Base R → N ∈ Fin ∧ N ∈ Fin
9 mpoexga ⊢ N ∈ Fin ∧ N ∈ Fin → k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l S 0 ˙ i M j ∈ V
10 8 9 syl ⊢ M ∈ B ∧ S ∈ Base R → k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l S 0 ˙ i M j ∈ V
11 ifeq1 ⊢ s = S → if j = l s 0 ˙ = if j = l S 0 ˙
12 11 adantl ⊢ m = M ∧ s = S → if j = l s 0 ˙ = if j = l S 0 ˙
13 oveq ⊢ m = M → i m j = i M j
14 13 adantr ⊢ m = M ∧ s = S → i m j = i M j
15 12 14 ifeq12d ⊢ m = M ∧ s = S → if i = k if j = l s 0 ˙ i m j = if i = k if j = l S 0 ˙ i M j
16 15 mpoeq3dv ⊢ m = M ∧ s = S → i ∈ N , j ∈ N ⟼ if i = k if j = l s 0 ˙ i m j = i ∈ N , j ∈ N ⟼ if i = k if j = l S 0 ˙ i M j
17 16 mpoeq3dv ⊢ m = M ∧ s = S → k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l s 0 ˙ i m j = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l S 0 ˙ i M j
18 1 2 3 4 marrepfval ⊢ Q = m ∈ B , s ∈ Base R ⟼ k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l s 0 ˙ i m j
19 17 18 ovmpoga ⊢ M ∈ B ∧ S ∈ Base R ∧ k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l S 0 ˙ i M j ∈ V → M Q S = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l S 0 ˙ i M j
20 10 19 mpd3an3 ⊢ M ∈ B ∧ S ∈ Base R → M Q S = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l S 0 ˙ i M j