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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
marrepfval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
marrepfval.q ⊢ 𝑄 = ( 𝑁 matRRep 𝑅 )
marrepfval.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion marrepval0 ( ( 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑀 𝑄 𝑆 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑆 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 marrepfval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 marrepfval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 marrepfval.q ⊢ 𝑄 = ( 𝑁 matRRep 𝑅 )
4 marrepfval.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 1 2 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
6 5 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
7 6 6 jca ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
8 7 adantr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
9 mpoexga ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑆 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) ∈ V )
10 8 9 syl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑆 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) ∈ V )
11 ifeq1 ⊢ ( 𝑠 = 𝑆 → if ( 𝑗 = 𝑙 , 𝑠 , 0 ) = if ( 𝑗 = 𝑙 , 𝑆 , 0 ) )
12 11 adantl ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑠 = 𝑆 ) → if ( 𝑗 = 𝑙 , 𝑠 , 0 ) = if ( 𝑗 = 𝑙 , 𝑆 , 0 ) )
13 oveq ⊢ ( 𝑚 = 𝑀 → ( 𝑖 𝑚 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
14 13 adantr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑠 = 𝑆 ) → ( 𝑖 𝑚 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
15 12 14 ifeq12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑠 = 𝑆 ) → if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑠 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) = if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑆 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) )
16 15 mpoeq3dv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑠 = 𝑆 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑠 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑆 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) )
17 16 mpoeq3dv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑠 = 𝑆 ) → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑠 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑆 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
18 1 2 3 4 marrepfval ⊢ 𝑄 = ( 𝑚 ∈ 𝐵 , 𝑠 ∈ ( Base ‘ 𝑅 ) ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑠 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) )
19 17 18 ovmpoga ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑆 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) ∈ V ) → ( 𝑀 𝑄 𝑆 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑆 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
20 10 19 mpd3an3 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑀 𝑄 𝑆 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 𝑆 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )