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 ⊢ 𝐾 = ( Base ‘ 𝑅 )
scmatrhmval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
scmatrhmval.o ⊢ 1 = ( 1r ‘ 𝐴 )
scmatrhmval.t ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
scmatrhmval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ∗ 1 ) )
scmatrhmval.c ⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
Assertion scmatrhmcl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 scmatrhmval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 scmatrhmval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 scmatrhmval.o ⊢ 1 = ( 1r ‘ 𝐴 )
4 scmatrhmval.t ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
5 scmatrhmval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ∗ 1 ) )
6 scmatrhmval.c ⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
7 1 2 3 4 5 scmatrhmval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 ∗ 1 ) )
8 7 3adant1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 ∗ 1 ) )
9 3simpa ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
10 simp3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → 𝑋 ∈ 𝐾 )
11 2 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
12 11 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → 𝐴 ∈ Ring )
13 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
14 13 3 ringidcl ⊢ ( 𝐴 ∈ Ring → 1 ∈ ( Base ‘ 𝐴 ) )
15 12 14 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → 1 ∈ ( Base ‘ 𝐴 ) )
16 1 2 13 4 matvscl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐾 ∧ 1 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑋 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) )
17 9 10 15 16 syl12anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) )
18 oveq1 ⊢ ( 𝑐 = 𝑋 → ( 𝑐 ∗ 1 ) = ( 𝑋 ∗ 1 ) )
19 18 eqeq2d ⊢ ( 𝑐 = 𝑋 → ( ( 𝑋 ∗ 1 ) = ( 𝑐 ∗ 1 ) ↔ ( 𝑋 ∗ 1 ) = ( 𝑋 ∗ 1 ) ) )
20 19 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) ∧ 𝑐 = 𝑋 ) → ( ( 𝑋 ∗ 1 ) = ( 𝑐 ∗ 1 ) ↔ ( 𝑋 ∗ 1 ) = ( 𝑋 ∗ 1 ) ) )
21 eqidd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 ∗ 1 ) = ( 𝑋 ∗ 1 ) )
22 10 20 21 rspcedvd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ∃ 𝑐 ∈ 𝐾 ( 𝑋 ∗ 1 ) = ( 𝑐 ∗ 1 ) )
23 1 2 13 3 4 6 scmatel ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑋 ∗ 1 ) ∈ 𝐶 ↔ ( ( 𝑋 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) ∧ ∃ 𝑐 ∈ 𝐾 ( 𝑋 ∗ 1 ) = ( 𝑐 ∗ 1 ) ) ) )
24 23 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝑋 ∗ 1 ) ∈ 𝐶 ↔ ( ( 𝑋 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) ∧ ∃ 𝑐 ∈ 𝐾 ( 𝑋 ∗ 1 ) = ( 𝑐 ∗ 1 ) ) ) )
25 17 22 24 mpbir2and ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 ∗ 1 ) ∈ 𝐶 )
26 8 25 eqeltrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐶 )