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	$⊢ K = {Base}_{R}$
	mat1rhmval.a	$⊢ A = \{E\} Mat R$
	mat1rhmval.b	$⊢ B = {Base}_{A}$
	mat1rhmval.o	$⊢ O = ⟨E, E⟩$
	mat1rhmval.f	$⊢ F = (x \in K ⟼ \{⟨O, x⟩\})$
Assertion	mat1rhm	$⊢ (R \in Ring \land E \in V) \to F \in (R RingHom A)$

Step	Hyp	Ref	Expression
1		mat1rhmval.k	$⊢ K = {Base}_{R}$
2		mat1rhmval.a	$⊢ A = \{E\} Mat R$
3		mat1rhmval.b	$⊢ B = {Base}_{A}$
4		mat1rhmval.o	$⊢ O = ⟨E, E⟩$
5		mat1rhmval.f	$⊢ F = (x \in K ⟼ \{⟨O, x⟩\})$
6		simpl	$⊢ (R \in Ring \land E \in V) \to R \in Ring$
7		snfi	$⊢ \{E\} \in Fin$
8	2	matring	$⊢ (\{E\} \in Fin \land R \in Ring) \to A \in Ring$
9	7 6 8	sylancr	$⊢ (R \in Ring \land E \in V) \to A \in Ring$
10	1 2 3 4 5	mat1ghm	$⊢ (R \in Ring \land E \in V) \to F \in (R GrpHom A)$
11		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
12		eqid	$⊢ {mulGrp}_{A} = {mulGrp}_{A}$
13	1 2 3 4 5 11 12	mat1mhm	$⊢ (R \in Ring \land E \in V) \to F \in ({mulGrp}_{R} MndHom {mulGrp}_{A})$
14	10 13	jca	$⊢ (R \in Ring \land E \in V) \to (F \in (R GrpHom A) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{A}))$
15	11 12	isrhm	$⊢ F \in (R RingHom A) \leftrightarrow ((R \in Ring \land A \in Ring) \land (F \in (R GrpHom A) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{A})))$
16	6 9 14 15	syl21anbrc	$⊢ (R \in Ring \land E \in V) \to F \in (R RingHom A)$

Metamath Proof Explorer