Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  scmatscmide Structured version   Unicode version

Theorem scmatscmide 18882
 Description: An entry of a scalar matrix expressed as a multiplication of a scalar with the identity matrix. (Contributed by AV, 30-Oct-2019.)
Hypotheses
Ref Expression
scmatscmide.a Mat
scmatscmide.b
scmatscmide.0
scmatscmide.1
scmatscmide.m
Assertion
Ref Expression
scmatscmide

Proof of Theorem scmatscmide
StepHypRef Expression
1 simpl2 1001 . . 3
2 simp3 999 . . . . 5
3 scmatscmide.a . . . . . . . 8 Mat
43matring 18818 . . . . . . 7
5 eqid 2443 . . . . . . . 8
6 scmatscmide.1 . . . . . . . 8
75, 6ringidcl 17093 . . . . . . 7
84, 7syl 16 . . . . . 6
983adant3 1017 . . . . 5
102, 9jca 532 . . . 4
12 simpr 461 . . 3
13 scmatscmide.b . . . 4
14 scmatscmide.m . . . 4
15 eqid 2443 . . . 4
163, 5, 13, 14, 15matvscacell 18811 . . 3
171, 11, 12, 16syl3anc 1229 . 2
18 eqid 2443 . . . 4
19 scmatscmide.0 . . . 4
20 simpl1 1000 . . . 4
21 simprl 756 . . . 4
22 simprr 757 . . . 4
233, 18, 19, 20, 1, 21, 22, 6mat1ov 18823 . . 3
2423oveq2d 6297 . 2
25 ovif2 6365 . . . 4
2613, 15, 18ringridm 17097 . . . . . 6
27263adant1 1015 . . . . 5
2813, 15, 19ringrz 17110 . . . . . 6
29283adant1 1015 . . . . 5
3027, 29ifeq12d 3946 . . . 4
3125, 30syl5eq 2496 . . 3