Metamath Proof Explorer

Theorem marepveval

Description: An entry of a matrix with a replaced column. (Contributed by AV, 14-Feb-2019) (Revised by AV, 26-Feb-2019)

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 marepveval ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ I ∈ N ∧ J ∈ N → I M Q C ⁡ K J = if J = K C ⁡ 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 1 2 3 4 marepvval ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N → M Q C ⁡ K = i ∈ N , j ∈ N ⟼ if j = K C ⁡ i i M j
6 5 adantr ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ I ∈ N ∧ J ∈ N → M Q C ⁡ K = i ∈ N , j ∈ N ⟼ if j = K C ⁡ i i M j
7 simprl ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ I ∈ N ∧ J ∈ N → I ∈ N
8 simplrr ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ I ∈ N ∧ J ∈ N ∧ i = I → J ∈ N
9 fvexd ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ I ∈ N ∧ J ∈ N → C ⁡ i ∈ V
10 ovexd ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ I ∈ N ∧ J ∈ N → i M j ∈ V
11 9 10 ifcld ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ I ∈ N ∧ J ∈ N → if j = K C ⁡ i i M j ∈ V
12 11 adantr ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ I ∈ N ∧ J ∈ N ∧ i = I ∧ j = J → if j = K C ⁡ i i M j ∈ V
13 eqeq1 ⊢ j = J → j = K ↔ J = K
14 13 adantl ⊢ i = I ∧ j = J → j = K ↔ J = K
15 fveq2 ⊢ i = I → C ⁡ i = C ⁡ I
16 15 adantr ⊢ i = I ∧ j = J → C ⁡ i = C ⁡ I
17 oveq12 ⊢ i = I ∧ j = J → i M j = I M J
18 14 16 17 ifbieq12d ⊢ i = I ∧ j = J → if j = K C ⁡ i i M j = if J = K C ⁡ I I M J
19 18 adantl ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ I ∈ N ∧ J ∈ N ∧ i = I ∧ j = J → if j = K C ⁡ i i M j = if J = K C ⁡ I I M J
20 7 8 12 19 ovmpodv2 ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ I ∈ N ∧ J ∈ N → M Q C ⁡ K = i ∈ N , j ∈ N ⟼ if j = K C ⁡ i i M j → I M Q C ⁡ K J = if J = K C ⁡ I I M J
21 6 20 mpd ⊢ M ∈ B ∧ C ∈ V ∧ K ∈ N ∧ I ∈ N ∧ J ∈ N → I M Q C ⁡ K J = if J = K C ⁡ I I M J