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

Theorem matsc 19406
 Description: The identity matrix multiplied with a scalar. (Contributed by Stefan O'Rear, 16-Jul-2018.)
Hypotheses
Ref Expression
matsc.a Mat
matsc.k
matsc.m
matsc.z
Assertion
Ref Expression
matsc
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,,

Proof of Theorem matsc
StepHypRef Expression
1 simp3 1007 . . 3
2 3simpa 1002 . . . 4
3 matsc.a . . . . 5 Mat
43matring 19399 . . . 4
5 eqid 2429 . . . . 5
6 eqid 2429 . . . . 5
75, 6ringidcl 17736 . . . 4
82, 4, 73syl 18 . . 3
9 matsc.k . . . 4
10 matsc.m . . . 4
11 eqid 2429 . . . 4
12 eqid 2429 . . . 4
133, 5, 9, 10, 11, 12matvsca2 19384 . . 3
141, 8, 13syl2anc 665 . 2
15 simp1 1005 . . 3
16 simp13 1037 . . 3
17 fvex 5891 . . . . 5
18 matsc.z . . . . . 6
19 fvex 5891 . . . . . 6
2018, 19eqeltri 2513 . . . . 5
2117, 20ifex 3983 . . . 4
2221a1i 11 . . 3
23 fconstmpt2 6405 . . . 4
2423a1i 11 . . 3
25 eqid 2429 . . . . 5
263, 25, 18mat1 19403 . . . 4