Metamath Proof Explorer

Theorem mulmarep1el

Description: Element by element multiplication of a matrix with an identity matrix with a column replaced by a vector. (Contributed by AV, 16-Feb-2019) (Revised by AV, 26-Feb-2019)

Ref Expression
Hypotheses marepvcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
marepvcl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
marepvcl.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
ma1repvcl.1 ⊢ 1 = ( 1r ‘ 𝐴 )
mulmarep1el.0 ⊢ 0 = ( 0g ‘ 𝑅 )
mulmarep1el.e ⊢ 𝐸 = ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 )
Assertion mulmarep1el ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 𝐿 𝐸 𝐽 ) ) = if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝐿 ) ) , if ( 𝐽 = 𝐿 , ( 𝐼 𝑋 𝐿 ) , 0 ) ) )

Proof

Step Hyp Ref Expression
1 marepvcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 marepvcl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 marepvcl.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
4 ma1repvcl.1 ⊢ 1 = ( 1r ‘ 𝐴 )
5 mulmarep1el.0 ⊢ 0 = ( 0g ‘ 𝑅 )
6 mulmarep1el.e ⊢ 𝐸 = ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 )
7 simp3 ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → 𝐿 ∈ 𝑁 )
8 simp2 ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → 𝐽 ∈ 𝑁 )
9 7 8 jca ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝐿 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) )
10 1 2 3 4 5 6 ma1repveval ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐿 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐿 𝐸 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐿 ) , if ( 𝐽 = 𝐿 , ( 1r ‘ 𝑅 ) , 0 ) ) )
11 9 10 syl3an3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐿 𝐸 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐿 ) , if ( 𝐽 = 𝐿 , ( 1r ‘ 𝑅 ) , 0 ) ) )
12 11 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 𝐿 𝐸 𝐽 ) ) = ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐿 ) , if ( 𝐽 = 𝐿 , ( 1r ‘ 𝑅 ) , 0 ) ) ) )
13 ovif2 ⊢ ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐿 ) , if ( 𝐽 = 𝐿 , ( 1r ‘ 𝑅 ) , 0 ) ) ) = if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝐿 ) ) , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) if ( 𝐽 = 𝐿 , ( 1r ‘ 𝑅 ) , 0 ) ) )
14 13 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐿 ) , if ( 𝐽 = 𝐿 , ( 1r ‘ 𝑅 ) , 0 ) ) ) = if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝐿 ) ) , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) if ( 𝐽 = 𝐿 , ( 1r ‘ 𝑅 ) , 0 ) ) ) )
15 ovif2 ⊢ ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) if ( 𝐽 = 𝐿 , ( 1r ‘ 𝑅 ) , 0 ) ) = if ( 𝐽 = 𝐿 , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) 0 ) )
16 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
17 simp1 ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → 𝐼 ∈ 𝑁 )
18 17 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → 𝐼 ∈ 𝑁 )
19 7 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → 𝐿 ∈ 𝑁 )
20 2 eleq2i ⊢ ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( Base ‘ 𝐴 ) )
21 20 biimpi ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
22 21 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
23 22 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
24 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
25 1 24 matecl ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐼 𝑋 𝐿 ) ∈ ( Base ‘ 𝑅 ) )
26 18 19 23 25 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐼 𝑋 𝐿 ) ∈ ( Base ‘ 𝑅 ) )
27 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
28 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
29 24 27 28 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 𝑋 𝐿 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝐼 𝑋 𝐿 ) )
30 16 26 29 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝐼 𝑋 𝐿 ) )
31 24 27 5 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 𝑋 𝐿 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
32 16 26 31 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
33 30 32 ifeq12d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → if ( 𝐽 = 𝐿 , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) 0 ) ) = if ( 𝐽 = 𝐿 , ( 𝐼 𝑋 𝐿 ) , 0 ) )
34 15 33 syl5eq ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) if ( 𝐽 = 𝐿 , ( 1r ‘ 𝑅 ) , 0 ) ) = if ( 𝐽 = 𝐿 , ( 𝐼 𝑋 𝐿 ) , 0 ) )
35 34 ifeq2d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝐿 ) ) , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) if ( 𝐽 = 𝐿 , ( 1r ‘ 𝑅 ) , 0 ) ) ) = if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝐿 ) ) , if ( 𝐽 = 𝐿 , ( 𝐼 𝑋 𝐿 ) , 0 ) ) )
36 12 14 35 3eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 𝐿 𝐸 𝐽 ) ) = if ( 𝐽 = 𝐾 , ( ( 𝐼 𝑋 𝐿 ) ( .r ‘ 𝑅 ) ( 𝐶 ‘ 𝐿 ) ) , if ( 𝐽 = 𝐿 , ( 𝐼 𝑋 𝐿 ) , 0 ) ) )