Metamath Proof Explorer

Theorem marrepval

Description: Third 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 marrepval ⊢ M ∈ B ∧ S ∈ Base R ∧ K ∈ N ∧ L ∈ N → K M Q S L = 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 3 4 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
6 5 adantr ⊢ M ∈ B ∧ S ∈ Base R ∧ K ∈ N ∧ L ∈ N → M Q S = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l S 0 ˙ i M j
7 simprl ⊢ M ∈ B ∧ S ∈ Base R ∧ K ∈ N ∧ L ∈ N → K ∈ N
8 simplrr ⊢ M ∈ B ∧ S ∈ Base R ∧ K ∈ N ∧ L ∈ N ∧ k = K → L ∈ N
9 1 2 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
10 9 simpld ⊢ M ∈ B → N ∈ Fin
11 10 10 jca ⊢ M ∈ B → N ∈ Fin ∧ N ∈ Fin
12 11 ad3antrrr ⊢ M ∈ B ∧ S ∈ Base R ∧ K ∈ N ∧ L ∈ N ∧ k = K ∧ l = L → N ∈ Fin ∧ N ∈ Fin
13 mpoexga ⊢ N ∈ Fin ∧ N ∈ Fin → i ∈ N , j ∈ N ⟼ if i = k if j = l S 0 ˙ i M j ∈ V
14 12 13 syl ⊢ M ∈ B ∧ S ∈ Base R ∧ K ∈ N ∧ L ∈ N ∧ k = K ∧ l = L → i ∈ N , j ∈ N ⟼ if i = k if j = l S 0 ˙ i M j ∈ V
15 eqeq2 ⊢ k = K → i = k ↔ i = K
16 15 adantr ⊢ k = K ∧ l = L → i = k ↔ i = K
17 eqeq2 ⊢ l = L → j = l ↔ j = L
18 17 ifbid ⊢ l = L → if j = l S 0 ˙ = if j = L S 0 ˙
19 18 adantl ⊢ k = K ∧ l = L → if j = l S 0 ˙ = if j = L S 0 ˙
20 16 19 ifbieq1d ⊢ k = K ∧ l = L → if i = k if j = l S 0 ˙ i M j = if i = K if j = L S 0 ˙ i M j
21 20 mpoeq3dv ⊢ k = K ∧ l = L → 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
22 21 adantl ⊢ M ∈ B ∧ S ∈ Base R ∧ K ∈ N ∧ L ∈ N ∧ k = K ∧ l = L → 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
23 7 8 14 22 ovmpodv2 ⊢ M ∈ B ∧ S ∈ Base R ∧ K ∈ N ∧ L ∈ N → M Q S = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l S 0 ˙ i M j → K M Q S L = i ∈ N , j ∈ N ⟼ if i = K if j = L S 0 ˙ i M j
24 6 23 mpd ⊢ M ∈ B ∧ S ∈ Base R ∧ K ∈ N ∧ L ∈ N → K M Q S L = i ∈ N , j ∈ N ⟼ if i = K if j = L S 0 ˙ i M j