Metamath Proof Explorer

Theorem ma1repveval

Description: An entry of an identity matrix with a replaced column. (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 ma1repveval ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 𝐸 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐼 ) , if ( 𝐽 = 𝐼 , ( 1r ‘ 𝑅 ) , 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 1 2 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
8 7 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
9 1 fveq2i ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
10 4 9 eqtri ⊢ 1 = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
11 1 2 10 mat1bas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 1 ∈ 𝐵 )
12 11 expcom ⊢ ( 𝑁 ∈ Fin → ( 𝑅 ∈ Ring → 1 ∈ 𝐵 ) )
13 8 12 syl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑅 ∈ Ring → 1 ∈ 𝐵 ) )
14 13 3ad2ant1 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 ∈ Ring → 1 ∈ 𝐵 ) )
15 14 impcom ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → 1 ∈ 𝐵 )
16 simpr2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → 𝐶 ∈ 𝑉 )
17 simpr3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → 𝐾 ∈ 𝑁 )
18 15 16 17 3jca ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ) → ( 1 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) )
19 6 a1i ⊢ ( ( ( 1 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐸 = ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 ) )
20 19 oveqd ⊢ ( ( ( 1 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 𝐸 𝐽 ) = ( 𝐼 ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 ) 𝐽 ) )
21 eqid ⊢ ( 𝑁 matRepV 𝑅 ) = ( 𝑁 matRepV 𝑅 )
22 1 2 21 3 marepveval ⊢ ( ( ( 1 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝐶 ) ‘ 𝐾 ) 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐼 ) , ( 𝐼 1 𝐽 ) ) )
23 20 22 eqtrd ⊢ ( ( ( 1 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 𝐸 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐼 ) , ( 𝐼 1 𝐽 ) ) )
24 18 23 stoic3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 𝐸 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐼 ) , ( 𝐼 1 𝐽 ) ) )
25 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
26 8 3ad2ant1 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝑁 ∈ Fin )
27 26 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
28 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
29 simp3l ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐼 ∈ 𝑁 )
30 simp3r ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐽 ∈ 𝑁 )
31 1 25 5 27 28 29 30 4 mat1ov ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 1 𝐽 ) = if ( 𝐼 = 𝐽 , ( 1r ‘ 𝑅 ) , 0 ) )
32 eqcom ⊢ ( 𝐼 = 𝐽 ↔ 𝐽 = 𝐼 )
33 32 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 = 𝐽 ↔ 𝐽 = 𝐼 ) )
34 33 ifbid ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → if ( 𝐼 = 𝐽 , ( 1r ‘ 𝑅 ) , 0 ) = if ( 𝐽 = 𝐼 , ( 1r ‘ 𝑅 ) , 0 ) )
35 31 34 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 1 𝐽 ) = if ( 𝐽 = 𝐼 , ( 1r ‘ 𝑅 ) , 0 ) )
36 35 ifeq2d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐼 ) , ( 𝐼 1 𝐽 ) ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐼 ) , if ( 𝐽 = 𝐼 , ( 1r ‘ 𝑅 ) , 0 ) ) )
37 24 36 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 𝐸 𝐽 ) = if ( 𝐽 = 𝐾 , ( 𝐶 ‘ 𝐼 ) , if ( 𝐽 = 𝐼 , ( 1r ‘ 𝑅 ) , 0 ) ) )