Metamath Proof Explorer

Theorem scmatrngiso

Description: There is a ring isomorphism from a ring to the ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019)

Ref Expression
Hypotheses scmatrhmval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
scmatrhmval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
scmatrhmval.o ⊢ 1 = ( 1r ‘ 𝐴 )
scmatrhmval.t ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
scmatrhmval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ∗ 1 ) )
scmatrhmval.c ⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
scmatghm.s ⊢ 𝑆 = ( 𝐴 ↾s 𝐶 )
Assertion scmatrngiso ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) )

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 scmatghm.s ⊢ 𝑆 = ( 𝐴 ↾s 𝐶 )
8 1 2 3 4 5 6 7 scmatrhm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
9 8 3adant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
10 1 2 3 4 5 6 scmatf1o ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 –1-1-onto→ 𝐶 )
11 2 6 7 scmatstrbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑆 ) = 𝐶 )
12 11 3adant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑆 ) = 𝐶 )
13 12 f1oeq3d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → ( 𝐹 : 𝐾 –1-1-onto→ ( Base ‘ 𝑆 ) ↔ 𝐹 : 𝐾 –1-1-onto→ 𝐶 ) )
14 10 13 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 –1-1-onto→ ( Base ‘ 𝑆 ) )
15 simp3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
16 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
17 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
18 2 16 1 17 6 scmatsrng ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ ( SubRing ‘ 𝐴 ) )
19 7 subrgring ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝐴 ) → 𝑆 ∈ Ring )
20 18 19 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ Ring )
21 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
22 1 21 isrim ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐾 –1-1-onto→ ( Base ‘ 𝑆 ) ) ) )
23 15 20 22 3imp3i2an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐾 –1-1-onto→ ( Base ‘ 𝑆 ) ) ) )
24 9 14 23 mpbir2and ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) )