Metamath Proof Explorer

Theorem mat1

Description: Value of an identity matrix, see also the statement in Lang p. 504: "The unit element of the ring of n x n matrices is the matrix I_n ... whose components are equal to 0 except on the diagonal, in which case they are equal to 1.". (Contributed by Stefan O'Rear, 7-Sep-2015)

Ref Expression
Hypotheses mat1.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mat1.o ⊢ 1 = ( 1r ‘ 𝑅 )
mat1.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion mat1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 mat1.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mat1.o ⊢ 1 = ( 1r ‘ 𝑅 )
3 mat1.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 simpr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
6 eqid ⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) )
7 simpl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin )
8 4 5 2 3 6 7 mamumat1cl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
9 1 4 matbas2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
10 8 9 eleqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ∈ ( Base ‘ 𝐴 ) )
11 eqid ⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
12 1 11 matmulr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
13 12 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
14 13 oveqd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑥 ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ( .r ‘ 𝐴 ) 𝑥 ) )
15 simplr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝑅 ∈ Ring )
16 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝑁 ∈ Fin )
17 9 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ↔ 𝑥 ∈ ( Base ‘ 𝐴 ) ) )
18 17 biimpar ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
19 4 15 2 3 6 16 16 11 18 mamulid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑥 ) = 𝑥 )
20 14 19 eqtr3d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ( .r ‘ 𝐴 ) 𝑥 ) = 𝑥 )
21 13 oveqd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ) = ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ) )
22 4 15 2 3 6 16 16 11 18 mamurid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ) = 𝑥 )
23 21 22 eqtr3d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ) = 𝑥 )
24 20 23 jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ( .r ‘ 𝐴 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ) = 𝑥 ) )
25 24 ralrimiva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ( .r ‘ 𝐴 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ) = 𝑥 ) )
26 1 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
27 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
28 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
29 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
30 27 28 29 isringid ⊢ ( 𝐴 ∈ Ring → ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ∈ ( Base ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ( .r ‘ 𝐴 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ) = 𝑥 ) ) ↔ ( 1r ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ) )
31 26 30 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ∈ ( Base ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ( .r ‘ 𝐴 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ) = 𝑥 ) ) ↔ ( 1r ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) ) )
32 10 25 31 mpbi2and ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) )