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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
marepvfval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
marepvfval.q ⊢ 𝑄 = ( 𝑁 matRepV 𝑅 )
marepvfval.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
Assertion marepveval ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( ( 𝑀 𝑄 𝐶 ) ‘ 𝐾 ) 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐼 ) , ( 𝐼 𝑀 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 marepvfval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 marepvfval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 marepvfval.q ⊢ 𝑄 = ( 𝑁 matRepV 𝑅 )
4 marepvfval.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
5 1 2 3 4 marepvval ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → ( ( 𝑀 𝑄 𝐶 ) ‘ 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 𝐶 ‘ 𝑖 ) , ( 𝑖 𝑀 𝑗 ) ) ) )
6 5 adantr ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( 𝑀 𝑄 𝐶 ) ‘ 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 𝐶 ‘ 𝑖 ) , ( 𝑖 𝑀 𝑗 ) ) ) )
7 simprl ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐼 ∈ 𝑁 )
8 simplrr ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ 𝑖 = 𝐼 ) → 𝐽 ∈ 𝑁 )
9 fvexd ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ V )
10 ovexd ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ V )
11 9 10 ifcld ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → if ( 𝑗 = 𝐾 , ( 𝐶 ‘ 𝑖 ) , ( 𝑖 𝑀 𝑗 ) ) ∈ V )
12 11 adantr ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → if ( 𝑗 = 𝐾 , ( 𝐶 ‘ 𝑖 ) , ( 𝑖 𝑀 𝑗 ) ) ∈ V )
13 eqeq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 = 𝐾 ↔ 𝐽 = 𝐾 ) )
14 13 adantl ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( 𝑗 = 𝐾 ↔ 𝐽 = 𝐾 ) )
15 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ 𝐼 ) )
16 15 adantr ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ 𝐼 ) )
17 oveq12 ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( 𝑖 𝑀 𝑗 ) = ( 𝐼 𝑀 𝐽 ) )
18 14 16 17 ifbieq12d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → if ( 𝑗 = 𝐾 , ( 𝐶 ‘ 𝑖 ) , ( 𝑖 𝑀 𝑗 ) ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐼 ) , ( 𝐼 𝑀 𝐽 ) ) )
19 18 adantl ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → if ( 𝑗 = 𝐾 , ( 𝐶 ‘ 𝑖 ) , ( 𝑖 𝑀 𝑗 ) ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐼 ) , ( 𝐼 𝑀 𝐽 ) ) )
20 7 8 12 19 ovmpodv2 ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( ( 𝑀 𝑄 𝐶 ) ‘ 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 𝐶 ‘ 𝑖 ) , ( 𝑖 𝑀 𝑗 ) ) ) → ( 𝐼 ( ( 𝑀 𝑄 𝐶 ) ‘ 𝐾 ) 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐼 ) , ( 𝐼 𝑀 𝐽 ) ) ) )
21 6 20 mpd ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( ( 𝑀 𝑄 𝐶 ) ‘ 𝐾 ) 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐼 ) , ( 𝐼 𝑀 𝐽 ) ) )