Metamath Proof Explorer


Theorem scmate

Description: An entry of an N x N scalar matrix over the ring R . (Contributed by AV, 18-Dec-2019)

Ref Expression
Hypotheses scmatmat.a A=NMatR
scmatmat.b B=BaseA
scmatmat.s S=NScMatR
scmate.k K=BaseR
scmate.0 0˙=0R
Assertion scmate NFinRRingMSINJNcKIMJ=ifI=Jc0˙

Proof

Step Hyp Ref Expression
1 scmatmat.a A=NMatR
2 scmatmat.b B=BaseA
3 scmatmat.s S=NScMatR
4 scmate.k K=BaseR
5 scmate.0 0˙=0R
6 eqid 1A=1A
7 eqid A=A
8 4 1 2 6 7 3 scmatscmid NFinRRingMScKM=cA1A
9 oveq M=cA1AIMJ=IcA1AJ
10 simpll1 NFinRRingMSINJNcKNFin
11 simpll2 NFinRRingMSINJNcKRRing
12 simpr NFinRRingMSINJNcKcK
13 simplr NFinRRingMSINJNcKINJN
14 1 4 5 6 7 scmatscmide NFinRRingcKINJNIcA1AJ=ifI=Jc0˙
15 10 11 12 13 14 syl31anc NFinRRingMSINJNcKIcA1AJ=ifI=Jc0˙
16 9 15 sylan9eqr NFinRRingMSINJNcKM=cA1AIMJ=ifI=Jc0˙
17 16 ex NFinRRingMSINJNcKM=cA1AIMJ=ifI=Jc0˙
18 17 reximdva NFinRRingMSINJNcKM=cA1AcKIMJ=ifI=Jc0˙
19 18 ex NFinRRingMSINJNcKM=cA1AcKIMJ=ifI=Jc0˙
20 8 19 mpid NFinRRingMSINJNcKIMJ=ifI=Jc0˙
21 20 imp NFinRRingMSINJNcKIMJ=ifI=Jc0˙