Theorem mat1rhm

Description: There is a ring homomorphism from a ring to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019)

	Ref	Expression
Hypotheses	mat1rhmval.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	mat1rhmval.a	⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
	mat1rhmval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mat1rhmval.o	⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
	mat1rhmval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } )
Assertion	mat1rhm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑅 RingHom 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		mat1rhmval.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
2		mat1rhmval.a	⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
3		mat1rhmval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mat1rhmval.o	⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
5		mat1rhmval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } )
6		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ∈ Ring )
7		snfi	⊢ { 𝐸 } ∈ Fin
8	2	matring	⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
9	7 6 8	sylancr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐴 ∈ Ring )
10	1 2 3 4 5	mat1ghm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝐴 ) )
11		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
12		eqid	⊢ ( mulGrp ‘ 𝐴 ) = ( mulGrp ‘ 𝐴 )
13	1 2 3 4 5 11 12	mat1mhm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝐴 ) ) )
14	10 13	jca	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝐹 ∈ ( 𝑅 GrpHom 𝐴 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝐴 ) ) ) )
15	11 12	isrhm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝐴 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝐴 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝐴 ) ) ) ) )
16	6 9 14 15	syl21anbrc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑅 RingHom 𝐴 ) )