Metamath Proof Explorer

Theorem scmatscmide

Description: An entry of a scalar matrix expressed as a multiplication of a scalar with the identity matrix. (Contributed by AV, 30-Oct-2019)

Ref Expression
Hypotheses scmatscmide.a ⊢A=NMatR
scmatscmide.b ⊢B=BaseR
scmatscmide.0 ⊢0˙=0R
scmatscmide.1 ⊢1˙=1A
scmatscmide.m ⊢∗˙=⋅A
Assertion scmatscmide ⊢N∈Fin∧R∈Ring∧C∈B∧I∈N∧J∈N→IC∗˙1˙J=ifI=JC0˙

Proof

Step Hyp Ref Expression
1 scmatscmide.a ⊢A=NMatR
2 scmatscmide.b ⊢B=BaseR
3 scmatscmide.0 ⊢0˙=0R
4 scmatscmide.1 ⊢1˙=1A
5 scmatscmide.m ⊢∗˙=⋅A
6 simpl2 ⊢N∈Fin∧R∈Ring∧C∈B∧I∈N∧J∈N→R∈Ring
7 simp3 ⊢N∈Fin∧R∈Ring∧C∈B→C∈B
8 1 matring ⊢N∈Fin∧R∈Ring→A∈Ring
9 eqid ⊢BaseA=BaseA
10 9 4 ringidcl ⊢A∈Ring→1˙∈BaseA
11 8 10 syl ⊢N∈Fin∧R∈Ring→1˙∈BaseA
12 11 3adant3 ⊢N∈Fin∧R∈Ring∧C∈B→1˙∈BaseA
13 7 12 jca ⊢N∈Fin∧R∈Ring∧C∈B→C∈B∧1˙∈BaseA
14 13 adantr ⊢N∈Fin∧R∈Ring∧C∈B∧I∈N∧J∈N→C∈B∧1˙∈BaseA
15 simpr ⊢N∈Fin∧R∈Ring∧C∈B∧I∈N∧J∈N→I∈N∧J∈N
16 eqid ⊢⋅R=⋅R
17 1 9 2 5 16 matvscacell ⊢R∈Ring∧C∈B∧1˙∈BaseA∧I∈N∧J∈N→IC∗˙1˙J=C⋅RI1˙J
18 6 14 15 17 syl3anc ⊢N∈Fin∧R∈Ring∧C∈B∧I∈N∧J∈N→IC∗˙1˙J=C⋅RI1˙J
19 eqid ⊢1R=1R
20 simpl1 ⊢N∈Fin∧R∈Ring∧C∈B∧I∈N∧J∈N→N∈Fin
21 simprl ⊢N∈Fin∧R∈Ring∧C∈B∧I∈N∧J∈N→I∈N
22 simprr ⊢N∈Fin∧R∈Ring∧C∈B∧I∈N∧J∈N→J∈N
23 1 19 3 20 6 21 22 4 mat1ov ⊢N∈Fin∧R∈Ring∧C∈B∧I∈N∧J∈N→I1˙J=ifI=J1R0˙
24 23 oveq2d ⊢N∈Fin∧R∈Ring∧C∈B∧I∈N∧J∈N→C⋅RI1˙J=C⋅RifI=J1R0˙
25 ovif2 ⊢C⋅RifI=J1R0˙=ifI=JC⋅R1RC⋅R0˙
26 2 16 19 ringridm ⊢R∈Ring∧C∈B→C⋅R1R=C
27 26 3adant1 ⊢N∈Fin∧R∈Ring∧C∈B→C⋅R1R=C
28 2 16 3 ringrz ⊢R∈Ring∧C∈B→C⋅R0˙=0˙
29 28 3adant1 ⊢N∈Fin∧R∈Ring∧C∈B→C⋅R0˙=0˙
30 27 29 ifeq12d ⊢N∈Fin∧R∈Ring∧C∈B→ifI=JC⋅R1RC⋅R0˙=ifI=JC0˙
31 25 30 eqtrid ⊢N∈Fin∧R∈Ring∧C∈B→C⋅RifI=J1R0˙=ifI=JC0˙
32 31 adantr ⊢N∈Fin∧R∈Ring∧C∈B∧I∈N∧J∈N→C⋅RifI=J1R0˙=ifI=JC0˙
33 18 24 32 3eqtrd ⊢N∈Fin∧R∈Ring∧C∈B∧I∈N∧J∈N→IC∗˙1˙J=ifI=JC0˙