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=NMatR
mat1.o 1˙=1R
mat1.z 0˙=0R
Assertion mat1 NFinRRing1A=iN,jNifi=j1˙0˙

Proof

Step Hyp Ref Expression
1 mat1.a A=NMatR
2 mat1.o 1˙=1R
3 mat1.z 0˙=0R
4 eqid BaseR=BaseR
5 simpr NFinRRingRRing
6 eqid iN,jNifi=j1˙0˙=iN,jNifi=j1˙0˙
7 simpl NFinRRingNFin
8 4 5 2 3 6 7 mamumat1cl NFinRRingiN,jNifi=j1˙0˙BaseRN×N
9 1 4 matbas2 NFinRRingBaseRN×N=BaseA
10 8 9 eleqtrd NFinRRingiN,jNifi=j1˙0˙BaseA
11 eqid RmaMulNNN=RmaMulNNN
12 1 11 matmulr NFinRRingRmaMulNNN=A
13 12 adantr NFinRRingxBaseARmaMulNNN=A
14 13 oveqd NFinRRingxBaseAiN,jNifi=j1˙0˙RmaMulNNNx=iN,jNifi=j1˙0˙Ax
15 simplr NFinRRingxBaseARRing
16 simpll NFinRRingxBaseANFin
17 9 eleq2d NFinRRingxBaseRN×NxBaseA
18 17 biimpar NFinRRingxBaseAxBaseRN×N
19 4 15 2 3 6 16 16 11 18 mamulid NFinRRingxBaseAiN,jNifi=j1˙0˙RmaMulNNNx=x
20 14 19 eqtr3d NFinRRingxBaseAiN,jNifi=j1˙0˙Ax=x
21 13 oveqd NFinRRingxBaseAxRmaMulNNNiN,jNifi=j1˙0˙=xAiN,jNifi=j1˙0˙
22 4 15 2 3 6 16 16 11 18 mamurid NFinRRingxBaseAxRmaMulNNNiN,jNifi=j1˙0˙=x
23 21 22 eqtr3d NFinRRingxBaseAxAiN,jNifi=j1˙0˙=x
24 20 23 jca NFinRRingxBaseAiN,jNifi=j1˙0˙Ax=xxAiN,jNifi=j1˙0˙=x
25 24 ralrimiva NFinRRingxBaseAiN,jNifi=j1˙0˙Ax=xxAiN,jNifi=j1˙0˙=x
26 1 matring NFinRRingARing
27 eqid BaseA=BaseA
28 eqid A=A
29 eqid 1A=1A
30 27 28 29 isringid ARingiN,jNifi=j1˙0˙BaseAxBaseAiN,jNifi=j1˙0˙Ax=xxAiN,jNifi=j1˙0˙=x1A=iN,jNifi=j1˙0˙
31 26 30 syl NFinRRingiN,jNifi=j1˙0˙BaseAxBaseAiN,jNifi=j1˙0˙Ax=xxAiN,jNifi=j1˙0˙=x1A=iN,jNifi=j1˙0˙
32 10 25 31 mpbi2and NFinRRing1A=iN,jNifi=j1˙0˙