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 = N Mat R
scmatscmide.b ⊢ B = Base R
scmatscmide.0 ⊢ 0 ˙ = 0 R
scmatscmide.1 ⊢ 1 ˙ = 1 A
scmatscmide.m ⊢ ∗ ˙ = ⋅ A
Assertion scmatscmide ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ B ∧ I ∈ N ∧ J ∈ N → I C ∗ ˙ 1 ˙ J = if I = J C 0 ˙

Proof

Step Hyp Ref Expression
1 scmatscmide.a ⊢ A = N Mat R
2 scmatscmide.b ⊢ B = Base R
3 scmatscmide.0 ⊢ 0 ˙ = 0 R
4 scmatscmide.1 ⊢ 1 ˙ = 1 A
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 ⊢ Base A = Base A
10 9 4 ringidcl ⊢ A ∈ Ring → 1 ˙ ∈ Base A
11 8 10 syl ⊢ N ∈ Fin ∧ R ∈ Ring → 1 ˙ ∈ Base A
12 11 3adant3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ B → 1 ˙ ∈ Base A
13 7 12 jca ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ B → C ∈ B ∧ 1 ˙ ∈ Base A
14 13 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ B ∧ I ∈ N ∧ J ∈ N → C ∈ B ∧ 1 ˙ ∈ Base A
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 ˙ ∈ Base A ∧ I ∈ N ∧ J ∈ N → I C ∗ ˙ 1 ˙ J = C ⋅ R I 1 ˙ J
18 6 14 15 17 syl3anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ B ∧ I ∈ N ∧ J ∈ N → I C ∗ ˙ 1 ˙ J = C ⋅ R I 1 ˙ J
19 eqid ⊢ 1 R = 1 R
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 → I 1 ˙ J = if I = J 1 R 0 ˙
24 23 oveq2d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ B ∧ I ∈ N ∧ J ∈ N → C ⋅ R I 1 ˙ J = C ⋅ R if I = J 1 R 0 ˙
25 ovif2 ⊢ C ⋅ R if I = J 1 R 0 ˙ = if I = J C ⋅ R 1 R C ⋅ R 0 ˙
26 2 16 19 ringridm ⊢ R ∈ Ring ∧ C ∈ B → C ⋅ R 1 R = C
27 26 3adant1 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ B → C ⋅ R 1 R = C
28 2 16 3 ringrz ⊢ R ∈ Ring ∧ C ∈ B → C ⋅ R 0 ˙ = 0 ˙
29 28 3adant1 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ B → C ⋅ R 0 ˙ = 0 ˙
30 27 29 ifeq12d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ B → if I = J C ⋅ R 1 R C ⋅ R 0 ˙ = if I = J C 0 ˙
31 25 30 syl5eq ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ B → C ⋅ R if I = J 1 R 0 ˙ = if I = J C 0 ˙
32 31 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ B ∧ I ∈ N ∧ J ∈ N → C ⋅ R if I = J 1 R 0 ˙ = if I = J C 0 ˙
33 18 24 32 3eqtrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ C ∈ B ∧ I ∈ N ∧ J ∈ N → I C ∗ ˙ 1 ˙ J = if I = J C 0 ˙