Metamath Proof Explorer

Theorem matsc

Description: The identity matrix multiplied with a scalar. (Contributed by Stefan O'Rear, 16-Jul-2018)

Ref Expression
Hypotheses matsc.a ⊢ A = N Mat R
matsc.k ⊢ K = Base R
matsc.m ⊢ · ˙ = ⋅ A
matsc.z ⊢ 0 ˙ = 0 R
Assertion matsc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → L · ˙ 1 A = i ∈ N , j ∈ N ⟼ if i = j L 0 ˙

Proof

Step Hyp Ref Expression
1 matsc.a ⊢ A = N Mat R
2 matsc.k ⊢ K = Base R
3 matsc.m ⊢ · ˙ = ⋅ A
4 matsc.z ⊢ 0 ˙ = 0 R
5 simp3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → L ∈ K
6 3simpa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → N ∈ Fin ∧ R ∈ Ring
7 1 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
8 eqid ⊢ Base A = Base A
9 eqid ⊢ 1 A = 1 A
10 8 9 ringidcl ⊢ A ∈ Ring → 1 A ∈ Base A
11 6 7 10 3syl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → 1 A ∈ Base A
12 eqid ⊢ ⋅ R = ⋅ R
13 eqid ⊢ N × N = N × N
14 1 8 2 3 12 13 matvsca2 ⊢ L ∈ K ∧ 1 A ∈ Base A → L · ˙ 1 A = N × N × L ⋅ R f 1 A
15 5 11 14 syl2anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → L · ˙ 1 A = N × N × L ⋅ R f 1 A
16 simp1 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → N ∈ Fin
17 simp13 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K ∧ i ∈ N ∧ j ∈ N → L ∈ K
18 fvex ⊢ 1 R ∈ V
19 4 fvexi ⊢ 0 ˙ ∈ V
20 18 19 ifex ⊢ if i = j 1 R 0 ˙ ∈ V
21 20 a1i ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K ∧ i ∈ N ∧ j ∈ N → if i = j 1 R 0 ˙ ∈ V
22 fconstmpo ⊢ N × N × L = i ∈ N , j ∈ N ⟼ L
23 22 a1i ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → N × N × L = i ∈ N , j ∈ N ⟼ L
24 eqid ⊢ 1 R = 1 R
25 1 24 4 mat1 ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A = i ∈ N , j ∈ N ⟼ if i = j 1 R 0 ˙
26 25 3adant3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → 1 A = i ∈ N , j ∈ N ⟼ if i = j 1 R 0 ˙
27 16 16 17 21 23 26 offval22 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → N × N × L ⋅ R f 1 A = i ∈ N , j ∈ N ⟼ L ⋅ R if i = j 1 R 0 ˙
28 ovif2 ⊢ L ⋅ R if i = j 1 R 0 ˙ = if i = j L ⋅ R 1 R L ⋅ R 0 ˙
29 2 12 24 ringridm ⊢ R ∈ Ring ∧ L ∈ K → L ⋅ R 1 R = L
30 29 3adant1 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → L ⋅ R 1 R = L
31 2 12 4 ringrz ⊢ R ∈ Ring ∧ L ∈ K → L ⋅ R 0 ˙ = 0 ˙
32 31 3adant1 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → L ⋅ R 0 ˙ = 0 ˙
33 30 32 ifeq12d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → if i = j L ⋅ R 1 R L ⋅ R 0 ˙ = if i = j L 0 ˙
34 28 33 syl5eq ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → L ⋅ R if i = j 1 R 0 ˙ = if i = j L 0 ˙
35 34 mpoeq3dv ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → i ∈ N , j ∈ N ⟼ L ⋅ R if i = j 1 R 0 ˙ = i ∈ N , j ∈ N ⟼ if i = j L 0 ˙
36 15 27 35 3eqtrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → L · ˙ 1 A = i ∈ N , j ∈ N ⟼ if i = j L 0 ˙