mat1ghm

Description: There is a group homomorphism from the additive group of a ring to the additive group of 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	mat1ghm	$⊢ (R \in Ring \land E \in V) \to F \in (R GrpHom A)$

Proof

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		eqid	$⊢ +_{R} = +_{R}$
7		eqid	$⊢ +_{A} = +_{A}$
8		ringgrp	$⊢ R \in Ring \to R \in Grp$
9	8	adantr	$⊢ (R \in Ring \land E \in V) \to R \in Grp$
10		snfi	$⊢ \{E\} \in Fin$
11		simpl	$⊢ (R \in Ring \land E \in V) \to R \in Ring$
12	2	matgrp	$⊢ (\{E\} \in Fin \land R \in Ring) \to A \in Grp$
13	10 11 12	sylancr	$⊢ (R \in Ring \land E \in V) \to A \in Grp$
14	1 2 3 4 5	mat1f	$⊢ (R \in Ring \land E \in V) \to F : K ⟶ B$
15	11	adantr	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to R \in Ring$
16		simpr	$⊢ (R \in Ring \land E \in V) \to E \in V$
17	16	adantr	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E \in V$
18		simpl	$⊢ (w \in K \land y \in K) \to w \in K$
19	18	adantl	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to w \in K$
20	1 2 3 4 5	mat1rhmelval	$⊢ (R \in Ring \land E \in V \land w \in K) \to E F (w) E = w$
21	15 17 19 20	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E F (w) E = w$
22		simpr	$⊢ (w \in K \land y \in K) \to y \in K$
23	22	adantl	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to y \in K$
24	1 2 3 4 5	mat1rhmelval	$⊢ (R \in Ring \land E \in V \land y \in K) \to E F (y) E = y$
25	15 17 23 24	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E F (y) E = y$
26	21 25	oveq12d	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to (E F (w) E) +_{R} (E F (y) E) = w +_{R} y$
27	1 2 3 4 5	mat1rhmcl	$⊢ (R \in Ring \land E \in V \land w \in K) \to F (w) \in B$
28	15 17 19 27	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to F (w) \in B$
29	1 2 3 4 5	mat1rhmcl	$⊢ (R \in Ring \land E \in V \land y \in K) \to F (y) \in B$
30	15 17 23 29	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to F (y) \in B$
31		snidg	$⊢ E \in V \to E \in \{E\}$
32	31 31	jca	$⊢ E \in V \to (E \in \{E\} \land E \in \{E\})$
33	32	adantl	$⊢ (R \in Ring \land E \in V) \to (E \in \{E\} \land E \in \{E\})$
34	33	adantr	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to (E \in \{E\} \land E \in \{E\})$
35	2 3 7 6	matplusgcell	$⊢ ((F (w) \in B \land F (y) \in B) \land (E \in \{E\} \land E \in \{E\})) \to E (F (w) +_{A} F (y)) E = (E F (w) E) +_{R} (E F (y) E)$
36	28 30 34 35	syl21anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E (F (w) +_{A} F (y)) E = (E F (w) E) +_{R} (E F (y) E)$
37	1 6	ringacl	$⊢ (R \in Ring \land w \in K \land y \in K) \to w +_{R} y \in K$
38	15 19 23 37	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to w +_{R} y \in K$
39	1 2 3 4 5	mat1rhmelval	$⊢ (R \in Ring \land E \in V \land w +_{R} y \in K) \to E F (w +_{R} y) E = w +_{R} y$
40	15 17 38 39	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E F (w +_{R} y) E = w +_{R} y$
41	26 36 40	3eqtr4rd	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E F (w +_{R} y) E = E (F (w) +_{A} F (y)) E$
42		oveq1	$⊢ i = E \to i F (w +_{R} y) j = E F (w +_{R} y) j$
43		oveq1	$⊢ i = E \to i (F (w) +_{A} F (y)) j = E (F (w) +_{A} F (y)) j$
44	42 43	eqeq12d	$⊢ i = E \to (i F (w +_{R} y) j = i (F (w) +_{A} F (y)) j \leftrightarrow E F (w +_{R} y) j = E (F (w) +_{A} F (y)) j)$
45		oveq2	$⊢ j = E \to E F (w +_{R} y) j = E F (w +_{R} y) E$
46		oveq2	$⊢ j = E \to E (F (w) +_{A} F (y)) j = E (F (w) +_{A} F (y)) E$
47	45 46	eqeq12d	$⊢ j = E \to (E F (w +_{R} y) j = E (F (w) +_{A} F (y)) j \leftrightarrow E F (w +_{R} y) E = E (F (w) +_{A} F (y)) E)$
48	44 47	2ralsng	$⊢ (E \in V \land E \in V) \to (\forall i \in \{E\} \forall j \in \{E\} i F (w +_{R} y) j = i (F (w) +_{A} F (y)) j \leftrightarrow E F (w +_{R} y) E = E (F (w) +_{A} F (y)) E)$
49	16 16 48	syl2anc	$⊢ (R \in Ring \land E \in V) \to (\forall i \in \{E\} \forall j \in \{E\} i F (w +_{R} y) j = i (F (w) +_{A} F (y)) j \leftrightarrow E F (w +_{R} y) E = E (F (w) +_{A} F (y)) E)$
50	49	adantr	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to (\forall i \in \{E\} \forall j \in \{E\} i F (w +_{R} y) j = i (F (w) +_{A} F (y)) j \leftrightarrow E F (w +_{R} y) E = E (F (w) +_{A} F (y)) E)$
51	41 50	mpbird	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to \forall i \in \{E\} \forall j \in \{E\} i F (w +_{R} y) j = i (F (w) +_{A} F (y)) j$
52	1 2 3 4 5	mat1rhmcl	$⊢ (R \in Ring \land E \in V \land w +_{R} y \in K) \to F (w +_{R} y) \in B$
53	15 17 38 52	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to F (w +_{R} y) \in B$
54	2	matring	$⊢ (\{E\} \in Fin \land R \in Ring) \to A \in Ring$
55	10 11 54	sylancr	$⊢ (R \in Ring \land E \in V) \to A \in Ring$
56	55	adantr	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to A \in Ring$
57	3 7	ringacl	$⊢ (A \in Ring \land F (w) \in B \land F (y) \in B) \to F (w) +_{A} F (y) \in B$
58	56 28 30 57	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to F (w) +_{A} F (y) \in B$
59	2 3	eqmat	$⊢ (F (w +_{R} y) \in B \land F (w) +_{A} F (y) \in B) \to (F (w +_{R} y) = F (w) +_{A} F (y) \leftrightarrow \forall i \in \{E\} \forall j \in \{E\} i F (w +_{R} y) j = i (F (w) +_{A} F (y)) j)$
60	53 58 59	syl2anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to (F (w +_{R} y) = F (w) +_{A} F (y) \leftrightarrow \forall i \in \{E\} \forall j \in \{E\} i F (w +_{R} y) j = i (F (w) +_{A} F (y)) j)$
61	51 60	mpbird	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to F (w +_{R} y) = F (w) +_{A} F (y)$
62	1 3 6 7 9 13 14 61	isghmd	$⊢ (R \in Ring \land E \in V) \to F \in (R GrpHom A)$

Metamath Proof Explorer

Theorem mat1ghm

Proof