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 ⊢ A = N Mat R
mat1.o ⊢ 1 ˙ = 1 R
mat1.z ⊢ 0 ˙ = 0 R
Assertion mat1 ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A = i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙

Proof

Step Hyp Ref Expression
1 mat1.a ⊢ A = N Mat R
2 mat1.o ⊢ 1 ˙ = 1 R
3 mat1.z ⊢ 0 ˙ = 0 R
4 eqid ⊢ Base R = Base R
5 simpr ⊢ N ∈ Fin ∧ R ∈ Ring → R ∈ Ring
6 eqid ⊢ i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ = i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙
7 simpl ⊢ N ∈ Fin ∧ R ∈ Ring → N ∈ Fin
8 4 5 2 3 6 7 mamumat1cl ⊢ N ∈ Fin ∧ R ∈ Ring → i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ ∈ Base R N × N
9 1 4 matbas2 ⊢ N ∈ Fin ∧ R ∈ Ring → Base R N × N = Base A
10 8 9 eleqtrd ⊢ N ∈ Fin ∧ R ∈ Ring → i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ ∈ Base A
11 eqid ⊢ R maMul N N N = R maMul N N N
12 1 11 matmulr ⊢ N ∈ Fin ∧ R ∈ Ring → R maMul N N N = ⋅ A
13 12 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base A → R maMul N N N = ⋅ A
14 13 oveqd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base A → i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ R maMul N N N x = i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ ⋅ A x
15 simplr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base A → R ∈ Ring
16 simpll ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base A → N ∈ Fin
17 9 eleq2d ⊢ N ∈ Fin ∧ R ∈ Ring → x ∈ Base R N × N ↔ x ∈ Base A
18 17 biimpar ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base A → x ∈ Base R N × N
19 4 15 2 3 6 16 16 11 18 mamulid ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base A → i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ R maMul N N N x = x
20 14 19 eqtr3d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base A → i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ ⋅ A x = x
21 13 oveqd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base A → x R maMul N N N i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ = x ⋅ A i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙
22 4 15 2 3 6 16 16 11 18 mamurid ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base A → x R maMul N N N i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ = x
23 21 22 eqtr3d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base A → x ⋅ A i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ = x
24 20 23 jca ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ Base A → i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ ⋅ A x = x ∧ x ⋅ A i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ = x
25 24 ralrimiva ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ x ∈ Base A i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ ⋅ A x = x ∧ x ⋅ A i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ = x
26 1 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
27 eqid ⊢ Base A = Base A
28 eqid ⊢ ⋅ A = ⋅ A
29 eqid ⊢ 1 A = 1 A
30 27 28 29 isringid ⊢ A ∈ Ring → i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ ∈ Base A ∧ ∀ x ∈ Base A i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ ⋅ A x = x ∧ x ⋅ A i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ = x ↔ 1 A = i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙
31 26 30 syl ⊢ N ∈ Fin ∧ R ∈ Ring → i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ ∈ Base A ∧ ∀ x ∈ Base A i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ ⋅ A x = x ∧ x ⋅ A i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙ = x ↔ 1 A = i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙
32 10 25 31 mpbi2and ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A = i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙