Metamath Proof Explorer

Theorem scmatmats

Description: The set of an N x N scalar matrices over the ring R expressed as a subset of N x N matrices over the ring R with certain properties for their entries. (Contributed by AV, 31-Oct-2019) (Revised by AV, 19-Dec-2019)

Ref Expression
Hypotheses scmatmat.a ⊢ A = N Mat R
scmatmat.b ⊢ B = Base A
scmatmat.s ⊢ S = N ScMat R
scmate.k ⊢ K = Base R
scmate.0 ⊢ 0 ˙ = 0 R
Assertion scmatmats ⊢ N ∈ Fin ∧ R ∈ Ring → S = m ∈ B | ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙

Proof

Step Hyp Ref Expression
1 scmatmat.a ⊢ A = N Mat R
2 scmatmat.b ⊢ B = Base A
3 scmatmat.s ⊢ S = N ScMat R
4 scmate.k ⊢ K = Base R
5 scmate.0 ⊢ 0 ˙ = 0 R
6 eqid ⊢ 1 A = 1 A
7 eqid ⊢ ⋅ A = ⋅ A
8 4 1 2 6 7 3 scmatval ⊢ N ∈ Fin ∧ R ∈ Ring → S = m ∈ B | ∃ c ∈ K m = c ⋅ A 1 A
9 simpr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B → m ∈ B
10 9 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K → m ∈ B
11 simpll ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K → N ∈ Fin ∧ R ∈ Ring
12 1 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
13 2 6 ringidcl ⊢ A ∈ Ring → 1 A ∈ B
14 12 13 syl ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ B
15 14 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B → 1 A ∈ B
16 15 anim1ci ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K → c ∈ K ∧ 1 A ∈ B
17 4 1 2 7 matvscl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ c ∈ K ∧ 1 A ∈ B → c ⋅ A 1 A ∈ B
18 11 16 17 syl2anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K → c ⋅ A 1 A ∈ B
19 1 2 eqmat ⊢ m ∈ B ∧ c ⋅ A 1 A ∈ B → m = c ⋅ A 1 A ↔ ∀ i ∈ N ∀ j ∈ N i m j = i c ⋅ A 1 A j
20 10 18 19 syl2anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K → m = c ⋅ A 1 A ↔ ∀ i ∈ N ∀ j ∈ N i m j = i c ⋅ A 1 A j
21 simplll ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K → N ∈ Fin
22 simpllr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K → R ∈ Ring
23 simpr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K → c ∈ K
24 21 22 23 3jca ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K → N ∈ Fin ∧ R ∈ Ring ∧ c ∈ K
25 1 4 5 6 7 scmatscmide ⊢ N ∈ Fin ∧ R ∈ Ring ∧ c ∈ K ∧ i ∈ N ∧ j ∈ N → i c ⋅ A 1 A j = if i = j c 0 ˙
26 24 25 sylan ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K ∧ i ∈ N ∧ j ∈ N → i c ⋅ A 1 A j = if i = j c 0 ˙
27 26 eqeq2d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K ∧ i ∈ N ∧ j ∈ N → i m j = i c ⋅ A 1 A j ↔ i m j = if i = j c 0 ˙
28 27 2ralbidva ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K → ∀ i ∈ N ∀ j ∈ N i m j = i c ⋅ A 1 A j ↔ ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙
29 20 28 bitrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ K → m = c ⋅ A 1 A ↔ ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙
30 29 rexbidva ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B → ∃ c ∈ K m = c ⋅ A 1 A ↔ ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙
31 30 rabbidva ⊢ N ∈ Fin ∧ R ∈ Ring → m ∈ B | ∃ c ∈ K m = c ⋅ A 1 A = m ∈ B | ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙
32 8 31 eqtrd ⊢ N ∈ Fin ∧ R ∈ Ring → S = m ∈ B | ∃ c ∈ K ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙