Metamath Proof Explorer

Theorem scmatrhmcl

Description: The value of the ring homomorphism F is a scalar matrix. (Contributed by AV, 22-Dec-2019)

Ref Expression
Hypotheses scmatrhmval.k ⊢ K = Base R
scmatrhmval.a ⊢ A = N Mat R
scmatrhmval.o ⊢ 1 ˙ = 1 A
scmatrhmval.t ⊢ ∗ ˙ = ⋅ A
scmatrhmval.f ⊢ F = x ∈ K ⟼ x ∗ ˙ 1 ˙
scmatrhmval.c ⊢ C = N ScMat R
Assertion scmatrhmcl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K → F ⁡ X ∈ C

Proof

Step Hyp Ref Expression
1 scmatrhmval.k ⊢ K = Base R
2 scmatrhmval.a ⊢ A = N Mat R
3 scmatrhmval.o ⊢ 1 ˙ = 1 A
4 scmatrhmval.t ⊢ ∗ ˙ = ⋅ A
5 scmatrhmval.f ⊢ F = x ∈ K ⟼ x ∗ ˙ 1 ˙
6 scmatrhmval.c ⊢ C = N ScMat R
7 1 2 3 4 5 scmatrhmval ⊢ R ∈ Ring ∧ X ∈ K → F ⁡ X = X ∗ ˙ 1 ˙
8 7 3adant1 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K → F ⁡ X = X ∗ ˙ 1 ˙
9 3simpa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K → N ∈ Fin ∧ R ∈ Ring
10 simp3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K → X ∈ K
11 2 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
12 11 3adant3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K → A ∈ Ring
13 eqid ⊢ Base A = Base A
14 13 3 ringidcl ⊢ A ∈ Ring → 1 ˙ ∈ Base A
15 12 14 syl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K → 1 ˙ ∈ Base A
16 1 2 13 4 matvscl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K ∧ 1 ˙ ∈ Base A → X ∗ ˙ 1 ˙ ∈ Base A
17 9 10 15 16 syl12anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K → X ∗ ˙ 1 ˙ ∈ Base A
18 oveq1 ⊢ c = X → c ∗ ˙ 1 ˙ = X ∗ ˙ 1 ˙
19 18 eqeq2d ⊢ c = X → X ∗ ˙ 1 ˙ = c ∗ ˙ 1 ˙ ↔ X ∗ ˙ 1 ˙ = X ∗ ˙ 1 ˙
20 19 adantl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K ∧ c = X → X ∗ ˙ 1 ˙ = c ∗ ˙ 1 ˙ ↔ X ∗ ˙ 1 ˙ = X ∗ ˙ 1 ˙
21 eqidd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K → X ∗ ˙ 1 ˙ = X ∗ ˙ 1 ˙
22 10 20 21 rspcedvd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K → ∃ c ∈ K X ∗ ˙ 1 ˙ = c ∗ ˙ 1 ˙
23 1 2 13 3 4 6 scmatel ⊢ N ∈ Fin ∧ R ∈ Ring → X ∗ ˙ 1 ˙ ∈ C ↔ X ∗ ˙ 1 ˙ ∈ Base A ∧ ∃ c ∈ K X ∗ ˙ 1 ˙ = c ∗ ˙ 1 ˙
24 23 3adant3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K → X ∗ ˙ 1 ˙ ∈ C ↔ X ∗ ˙ 1 ˙ ∈ Base A ∧ ∃ c ∈ K X ∗ ˙ 1 ˙ = c ∗ ˙ 1 ˙
25 17 22 24 mpbir2and ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K → X ∗ ˙ 1 ˙ ∈ C
26 8 25 eqeltrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ X ∈ K → F ⁡ X ∈ C