Metamath Proof Explorer

Theorem mat1scmat

Description: A 1-dimensional matrix over a ring is always a scalar matrix (and therefore, by scmatdmat , also a diagonal matrix). (Contributed by AV, 21-Dec-2019)

Ref Expression
Hypotheses mat1scmat.a ⊢ A = N Mat R
mat1scmat.b ⊢ B = Base A
Assertion mat1scmat ⊢ N ∈ V ∧ N = 1 ∧ R ∈ Ring → M ∈ B → M ∈ N ScMat R

Proof

Step Hyp Ref Expression
1 mat1scmat.a ⊢ A = N Mat R
2 mat1scmat.b ⊢ B = Base A
3 hash1snb ⊢ N ∈ V → N = 1 ↔ ∃ e N = e
4 simpr ⊢ R ∈ Ring ∧ M ∈ Base e Mat R → M ∈ Base e Mat R
5 eqid ⊢ e Mat R = e Mat R
6 eqid ⊢ Base R = Base R
7 eqid ⊢ e e = e e
8 5 6 7 mat1dimelbas ⊢ R ∈ Ring ∧ e ∈ V → M ∈ Base e Mat R ↔ ∃ c ∈ Base R M = e e c
9 8 elvd ⊢ R ∈ Ring → M ∈ Base e Mat R ↔ ∃ c ∈ Base R M = e e c
10 simpr ⊢ R ∈ Ring ∧ c ∈ Base R ∧ M = e e c → M = e e c
11 vex ⊢ e ∈ V
12 11 a1i ⊢ c ∈ Base R → e ∈ V
13 5 6 7 mat1dimid ⊢ R ∈ Ring ∧ e ∈ V → 1 e Mat R = e e 1 R
14 12 13 sylan2 ⊢ R ∈ Ring ∧ c ∈ Base R → 1 e Mat R = e e 1 R
15 14 oveq2d ⊢ R ∈ Ring ∧ c ∈ Base R → c ⋅ e Mat R 1 e Mat R = c ⋅ e Mat R e e 1 R
16 simpl ⊢ R ∈ Ring ∧ c ∈ Base R → R ∈ Ring
17 16 11 jctir ⊢ R ∈ Ring ∧ c ∈ Base R → R ∈ Ring ∧ e ∈ V
18 simpr ⊢ R ∈ Ring ∧ c ∈ Base R → c ∈ Base R
19 eqid ⊢ 1 R = 1 R
20 6 19 ringidcl ⊢ R ∈ Ring → 1 R ∈ Base R
21 20 adantr ⊢ R ∈ Ring ∧ c ∈ Base R → 1 R ∈ Base R
22 5 6 7 mat1dimscm ⊢ R ∈ Ring ∧ e ∈ V ∧ c ∈ Base R ∧ 1 R ∈ Base R → c ⋅ e Mat R e e 1 R = e e c ⋅ R 1 R
23 17 18 21 22 syl12anc ⊢ R ∈ Ring ∧ c ∈ Base R → c ⋅ e Mat R e e 1 R = e e c ⋅ R 1 R
24 eqid ⊢ ⋅ R = ⋅ R
25 6 24 19 ringridm ⊢ R ∈ Ring ∧ c ∈ Base R → c ⋅ R 1 R = c
26 25 opeq2d ⊢ R ∈ Ring ∧ c ∈ Base R → e e c ⋅ R 1 R = e e c
27 26 sneqd ⊢ R ∈ Ring ∧ c ∈ Base R → e e c ⋅ R 1 R = e e c
28 15 23 27 3eqtrrd ⊢ R ∈ Ring ∧ c ∈ Base R → e e c = c ⋅ e Mat R 1 e Mat R
29 28 adantr ⊢ R ∈ Ring ∧ c ∈ Base R ∧ M = e e c → e e c = c ⋅ e Mat R 1 e Mat R
30 10 29 eqtrd ⊢ R ∈ Ring ∧ c ∈ Base R ∧ M = e e c → M = c ⋅ e Mat R 1 e Mat R
31 30 ex ⊢ R ∈ Ring ∧ c ∈ Base R → M = e e c → M = c ⋅ e Mat R 1 e Mat R
32 31 reximdva ⊢ R ∈ Ring → ∃ c ∈ Base R M = e e c → ∃ c ∈ Base R M = c ⋅ e Mat R 1 e Mat R
33 9 32 sylbid ⊢ R ∈ Ring → M ∈ Base e Mat R → ∃ c ∈ Base R M = c ⋅ e Mat R 1 e Mat R
34 33 imp ⊢ R ∈ Ring ∧ M ∈ Base e Mat R → ∃ c ∈ Base R M = c ⋅ e Mat R 1 e Mat R
35 snfi ⊢ e ∈ Fin
36 simpl ⊢ R ∈ Ring ∧ M ∈ Base e Mat R → R ∈ Ring
37 eqid ⊢ Base e Mat R = Base e Mat R
38 eqid ⊢ 1 e Mat R = 1 e Mat R
39 eqid ⊢ ⋅ e Mat R = ⋅ e Mat R
40 eqid ⊢ e ScMat R = e ScMat R
41 6 5 37 38 39 40 scmatel ⊢ e ∈ Fin ∧ R ∈ Ring → M ∈ e ScMat R ↔ M ∈ Base e Mat R ∧ ∃ c ∈ Base R M = c ⋅ e Mat R 1 e Mat R
42 35 36 41 sylancr ⊢ R ∈ Ring ∧ M ∈ Base e Mat R → M ∈ e ScMat R ↔ M ∈ Base e Mat R ∧ ∃ c ∈ Base R M = c ⋅ e Mat R 1 e Mat R
43 4 34 42 mpbir2and ⊢ R ∈ Ring ∧ M ∈ Base e Mat R → M ∈ e ScMat R
44 43 ex ⊢ R ∈ Ring → M ∈ Base e Mat R → M ∈ e ScMat R
45 1 fveq2i ⊢ Base A = Base N Mat R
46 2 45 eqtri ⊢ B = Base N Mat R
47 fvoveq1 ⊢ N = e → Base N Mat R = Base e Mat R
48 46 47 eqtrid ⊢ N = e → B = Base e Mat R
49 48 eleq2d ⊢ N = e → M ∈ B ↔ M ∈ Base e Mat R
50 oveq1 ⊢ N = e → N ScMat R = e ScMat R
51 50 eleq2d ⊢ N = e → M ∈ N ScMat R ↔ M ∈ e ScMat R
52 49 51 imbi12d ⊢ N = e → M ∈ B → M ∈ N ScMat R ↔ M ∈ Base e Mat R → M ∈ e ScMat R
53 44 52 syl5ibr ⊢ N = e → R ∈ Ring → M ∈ B → M ∈ N ScMat R
54 53 exlimiv ⊢ ∃ e N = e → R ∈ Ring → M ∈ B → M ∈ N ScMat R
55 3 54 syl6bi ⊢ N ∈ V → N = 1 → R ∈ Ring → M ∈ B → M ∈ N ScMat R
56 55 3imp ⊢ N ∈ V ∧ N = 1 ∧ R ∈ Ring → M ∈ B → M ∈ N ScMat R