Metamath Proof Explorer

Theorem scmatid

Description: The identity matrix is a scalar matrix. (Contributed by AV, 20-Aug-2019) (Revised by AV, 18-Dec-2019)

Ref Expression
Hypotheses scmatid.a ⊢ A = N Mat R
scmatid.b ⊢ B = Base A
scmatid.e ⊢ E = Base R
scmatid.0 ⊢ 0 ˙ = 0 R
scmatid.s ⊢ S = N ScMat R
Assertion scmatid ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ S

Proof

Step Hyp Ref Expression
1 scmatid.a ⊢ A = N Mat R
2 scmatid.b ⊢ B = Base A
3 scmatid.e ⊢ E = Base R
4 scmatid.0 ⊢ 0 ˙ = 0 R
5 scmatid.s ⊢ S = N ScMat R
6 1 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
7 eqid ⊢ 1 A = 1 A
8 2 7 ringidcl ⊢ A ∈ Ring → 1 A ∈ B
9 6 8 syl ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ B
10 1 matsca2 ⊢ N ∈ Fin ∧ R ∈ Ring → R = Scalar ⁡ A
11 10 eqcomd ⊢ N ∈ Fin ∧ R ∈ Ring → Scalar ⁡ A = R
12 11 fveq2d ⊢ N ∈ Fin ∧ R ∈ Ring → 1 Scalar ⁡ A = 1 R
13 eqid ⊢ Base R = Base R
14 eqid ⊢ 1 R = 1 R
15 13 14 ringidcl ⊢ R ∈ Ring → 1 R ∈ Base R
16 15 adantl ⊢ N ∈ Fin ∧ R ∈ Ring → 1 R ∈ Base R
17 12 16 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring → 1 Scalar ⁡ A ∈ Base R
18 oveq1 ⊢ c = 1 Scalar ⁡ A → c ⋅ A 1 A = 1 Scalar ⁡ A ⋅ A 1 A
19 18 eqeq2d ⊢ c = 1 Scalar ⁡ A → 1 A = c ⋅ A 1 A ↔ 1 A = 1 Scalar ⁡ A ⋅ A 1 A
20 19 adantl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ c = 1 Scalar ⁡ A → 1 A = c ⋅ A 1 A ↔ 1 A = 1 Scalar ⁡ A ⋅ A 1 A
21 1 matlmod ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ LMod
22 eqid ⊢ Scalar ⁡ A = Scalar ⁡ A
23 eqid ⊢ ⋅ A = ⋅ A
24 eqid ⊢ 1 Scalar ⁡ A = 1 Scalar ⁡ A
25 2 22 23 24 lmodvs1 ⊢ A ∈ LMod ∧ 1 A ∈ B → 1 Scalar ⁡ A ⋅ A 1 A = 1 A
26 21 9 25 syl2anc ⊢ N ∈ Fin ∧ R ∈ Ring → 1 Scalar ⁡ A ⋅ A 1 A = 1 A
27 26 eqcomd ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A = 1 Scalar ⁡ A ⋅ A 1 A
28 17 20 27 rspcedvd ⊢ N ∈ Fin ∧ R ∈ Ring → ∃ c ∈ Base R 1 A = c ⋅ A 1 A
29 13 1 2 7 23 5 scmatel ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ S ↔ 1 A ∈ B ∧ ∃ c ∈ Base R 1 A = c ⋅ A 1 A
30 9 28 29 mpbir2and ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ S