Metamath Proof Explorer

Theorem 1marepvsma1

Description: The submatrix of the identity matrix with the ith column replaced by the vector obtained by removing the ith row and the ith column is an identity matrix. (Contributed by AV, 14-Feb-2019) (Revised by AV, 27-Feb-2019)

Ref Expression
Hypotheses 1marepvsma1.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
1marepvsma1.1 ⊢ 1 = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
1marepvsma1.x ⊢ 𝑋 = ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 )
Assertion 1marepvsma1 ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝐼 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑋 ) 𝐼 ) = ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 1marepvsma1.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
2 1marepvsma1.1 ⊢ 1 = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
3 1marepvsma1.x ⊢ 𝑋 = ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 )
4 3 oveqi ⊢ ( 𝑖 𝑋 𝑗 ) = ( 𝑖 ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) 𝑗 )
5 4 a1i ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑖 𝑋 𝑗 ) = ( 𝑖 ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) 𝑗 ) )
6 eqid ⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
7 eqid ⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
8 6 7 2 mat1bas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
9 8 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
10 simprr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑍 ∈ 𝑉 )
11 simprl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → 𝐼 ∈ 𝑁 )
12 9 10 11 3jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) )
13 12 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) )
14 eldifi ⊢ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) → 𝑖 ∈ 𝑁 )
15 eldifi ⊢ ( 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) → 𝑗 ∈ 𝑁 )
16 14 15 anim12i ⊢ ( ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
17 16 3adant1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
18 eqid ⊢ ( 𝑁 matRepV 𝑅 ) = ( 𝑁 matRepV 𝑅 )
19 6 7 18 1 marepveval ⊢ ( ( ( 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) 𝑗 ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) )
20 13 17 19 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑖 ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) 𝑗 ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) )
21 eldifsni ⊢ ( 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) → 𝑗 ≠ 𝐼 )
22 21 neneqd ⊢ ( 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) → ¬ 𝑗 = 𝐼 )
23 22 3ad2ant3 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ¬ 𝑗 = 𝐼 )
24 23 iffalsed ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) = ( 𝑖 1 𝑗 ) )
25 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
26 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
27 simp1lr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → 𝑁 ∈ Fin )
28 simp1ll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → 𝑅 ∈ Ring )
29 14 3ad2ant2 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → 𝑖 ∈ 𝑁 )
30 15 3ad2ant3 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → 𝑗 ∈ 𝑁 )
31 6 25 26 27 28 29 30 2 mat1ov ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑖 1 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
32 24 31 eqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
33 5 20 32 3eqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → ( 𝑖 𝑋 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
34 33 mpoeq3dva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑖 𝑋 𝑗 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
35 6 7 1 2 ma1repvcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ) → ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
36 35 ancom2s ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
37 3 36 eqeltrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑋 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
38 eqid ⊢ ( 𝑁 subMat 𝑅 ) = ( 𝑁 subMat 𝑅 )
39 6 38 7 submaval ⊢ ( ( 𝑋 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ) → ( 𝐼 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑋 ) 𝐼 ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑖 𝑋 𝑗 ) ) )
40 37 11 11 39 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝐼 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑋 ) 𝐼 ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ ( 𝑖 𝑋 𝑗 ) ) )
41 diffi ⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝐼 } ) ∈ Fin )
42 41 anim2i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 𝑅 ∈ Ring ∧ ( 𝑁 ∖ { 𝐼 } ) ∈ Fin ) )
43 42 ancomd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( 𝑁 ∖ { 𝐼 } ) ∈ Fin ∧ 𝑅 ∈ Ring ) )
44 43 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝑁 ∖ { 𝐼 } ) ∈ Fin ∧ 𝑅 ∈ Ring ) )
45 eqid ⊢ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) = ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 )
46 45 25 26 mat1 ⊢ ( ( ( 𝑁 ∖ { 𝐼 } ) ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
47 44 46 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
48 34 40 47 3eqtr4d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝐼 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑋 ) 𝐼 ) = ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) ) )