Metamath Proof Explorer


Theorem scmatel

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

Ref Expression
Hypotheses scmatval.k K=BaseR
scmatval.a A=NMatR
scmatval.b B=BaseA
scmatval.1 1˙=1A
scmatval.t ·˙=A
scmatval.s S=NScMatR
Assertion scmatel NFinRVMSMBcKM=c·˙1˙

Proof

Step Hyp Ref Expression
1 scmatval.k K=BaseR
2 scmatval.a A=NMatR
3 scmatval.b B=BaseA
4 scmatval.1 1˙=1A
5 scmatval.t ·˙=A
6 scmatval.s S=NScMatR
7 1 2 3 4 5 6 scmatval NFinRVS=mB|cKm=c·˙1˙
8 7 eleq2d NFinRVMSMmB|cKm=c·˙1˙
9 eqeq1 m=Mm=c·˙1˙M=c·˙1˙
10 9 rexbidv m=McKm=c·˙1˙cKM=c·˙1˙
11 10 elrab MmB|cKm=c·˙1˙MBcKM=c·˙1˙
12 8 11 bitrdi NFinRVMSMBcKM=c·˙1˙