mat1mhm

Description: There is a monoid homomorphism from the multiplicative group of a ring to the multiplicative 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⟩\})$
	mat1mhm.m	$⊢ M = {mulGrp}_{R}$
	mat1mhm.n	$⊢ N = {mulGrp}_{A}$
Assertion	mat1mhm	$⊢ (R \in Ring \land E \in V) \to F \in (M MndHom N)$

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		mat1mhm.m	$⊢ M = {mulGrp}_{R}$
7		mat1mhm.n	$⊢ N = {mulGrp}_{A}$
8	6	ringmgp	$⊢ R \in Ring \to M \in Mnd$
9	8	adantr	$⊢ (R \in Ring \land E \in V) \to M \in Mnd$
10		snfi	$⊢ \{E\} \in Fin$
11		simpl	$⊢ (R \in Ring \land E \in V) \to R \in Ring$
12	2	matring	$⊢ (\{E\} \in Fin \land R \in Ring) \to A \in Ring$
13	10 11 12	sylancr	$⊢ (R \in Ring \land E \in V) \to A \in Ring$
14	7	ringmgp	$⊢ A \in Ring \to N \in Mnd$
15	13 14	syl	$⊢ (R \in Ring \land E \in V) \to N \in Mnd$
16	1 2 3 4 5	mat1f	$⊢ (R \in Ring \land E \in V) \to F : K ⟶ B$
17		ringmnd	$⊢ R \in Ring \to R \in Mnd$
18	17	adantr	$⊢ (R \in Ring \land E \in V) \to R \in Mnd$
19	18	adantr	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to R \in Mnd$
20		simpr	$⊢ (R \in Ring \land E \in V) \to E \in V$
21	20	adantr	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E \in V$
22		simpll	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to R \in Ring$
23		eqid	$⊢ {Base}_{A} = {Base}_{A}$
24		snidg	$⊢ E \in V \to E \in \{E\}$
25	24	ad2antlr	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E \in \{E\}$
26		simprl	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to w \in K$
27	1 2 23 4 5	mat1rhmcl	$⊢ (R \in Ring \land E \in V \land w \in K) \to F (w) \in {Base}_{A}$
28	22 21 26 27	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to F (w) \in {Base}_{A}$
29	2 1 23 25 25 28	matecld	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E F (w) E \in K$
30		simprr	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to y \in K$
31	1 2 23 4 5	mat1rhmcl	$⊢ (R \in Ring \land E \in V \land y \in K) \to F (y) \in {Base}_{A}$
32	22 21 30 31	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to F (y) \in {Base}_{A}$
33	2 1 23 25 25 32	matecld	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E F (y) E \in K$
34		eqid	$⊢ \cdot_{R} = \cdot_{R}$
35	1 34	ringcl	$⊢ (R \in Ring \land E F (w) E \in K \land E F (y) E \in K) \to (E F (w) E) \cdot_{R} (E F (y) E) \in K$
36	22 29 33 35	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to (E F (w) E) \cdot_{R} (E F (y) E) \in K$
37		oveq2	$⊢ e = E \to E F (w) e = E F (w) E$
38		oveq1	$⊢ e = E \to e F (y) E = E F (y) E$
39	37 38	oveq12d	$⊢ e = E \to (E F (w) e) \cdot_{R} (e F (y) E) = (E F (w) E) \cdot_{R} (E F (y) E)$
40	39	adantl	$⊢ (((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \land e = E) \to (E F (w) e) \cdot_{R} (e F (y) E) = (E F (w) E) \cdot_{R} (E F (y) E)$
41	1 19 21 36 40	gsumsnd	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to \underset{e \in \{E\}}{\sum_{R}} ((E F (w) e) \cdot_{R} (e F (y) E)) = (E F (w) E) \cdot_{R} (E F (y) E)$
42	1 2 3 4 5	mat1rhmelval	$⊢ (R \in Ring \land E \in V \land w \in K) \to E F (w) E = w$
43	22 21 26 42	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E F (w) E = w$
44	1 2 3 4 5	mat1rhmelval	$⊢ (R \in Ring \land E \in V \land y \in K) \to E F (y) E = y$
45	22 21 30 44	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E F (y) E = y$
46	43 45	oveq12d	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to (E F (w) E) \cdot_{R} (E F (y) E) = w \cdot_{R} y$
47	41 46	eqtrd	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to \underset{e \in \{E\}}{\sum_{R}} ((E F (w) e) \cdot_{R} (e F (y) E)) = w \cdot_{R} y$
48	1 2 3 4 5	mat1rhmcl	$⊢ (R \in Ring \land E \in V \land w \in K) \to F (w) \in B$
49	22 21 26 48	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to F (w) \in B$
50	1 2 3 4 5	mat1rhmcl	$⊢ (R \in Ring \land E \in V \land y \in K) \to F (y) \in B$
51	22 21 30 50	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to F (y) \in B$
52	49 51	jca	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to (F (w) \in B \land F (y) \in B)$
53	24 24	jca	$⊢ E \in V \to (E \in \{E\} \land E \in \{E\})$
54	53	ad2antlr	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to (E \in \{E\} \land E \in \{E\})$
55		eqid	$⊢ \cdot_{A} = \cdot_{A}$
56	2 3 55	matmulcell	$⊢ (R \in Ring \land (F (w) \in B \land F (y) \in B) \land (E \in \{E\} \land E \in \{E\})) \to E (F (w) \cdot_{A} F (y)) E = \underset{e \in \{E\}}{\sum_{R}} ((E F (w) e) \cdot_{R} (e F (y) E))$
57	22 52 54 56	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E (F (w) \cdot_{A} F (y)) E = \underset{e \in \{E\}}{\sum_{R}} ((E F (w) e) \cdot_{R} (e F (y) E))$
58	1 34	ringcl	$⊢ (R \in Ring \land w \in K \land y \in K) \to w \cdot_{R} y \in K$
59	22 26 30 58	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to w \cdot_{R} y \in K$
60	1 2 3 4 5	mat1rhmelval	$⊢ (R \in Ring \land E \in V \land w \cdot_{R} y \in K) \to E F (w \cdot_{R} y) E = w \cdot_{R} y$
61	22 21 59 60	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E F (w \cdot_{R} y) E = w \cdot_{R} y$
62	47 57 61	3eqtr4rd	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to E F (w \cdot_{R} y) E = E (F (w) \cdot_{A} F (y)) E$
63		oveq1	$⊢ i = E \to i F (w \cdot_{R} y) j = E F (w \cdot_{R} y) j$
64		oveq1	$⊢ i = E \to i (F (w) \cdot_{A} F (y)) j = E (F (w) \cdot_{A} F (y)) j$
65	63 64	eqeq12d	$⊢ i = E \to (i F (w \cdot_{R} y) j = i (F (w) \cdot_{A} F (y)) j \leftrightarrow E F (w \cdot_{R} y) j = E (F (w) \cdot_{A} F (y)) j)$
66		oveq2	$⊢ j = E \to E F (w \cdot_{R} y) j = E F (w \cdot_{R} y) E$
67		oveq2	$⊢ j = E \to E (F (w) \cdot_{A} F (y)) j = E (F (w) \cdot_{A} F (y)) E$
68	66 67	eqeq12d	$⊢ j = E \to (E F (w \cdot_{R} y) j = E (F (w) \cdot_{A} F (y)) j \leftrightarrow E F (w \cdot_{R} y) E = E (F (w) \cdot_{A} F (y)) E)$
69	65 68	2ralsng	$⊢ (E \in V \land E \in V) \to (\forall i \in \{E\} \forall j \in \{E\} i F (w \cdot_{R} y) j = i (F (w) \cdot_{A} F (y)) j \leftrightarrow E F (w \cdot_{R} y) E = E (F (w) \cdot_{A} F (y)) E)$
70	20 69	sylancom	$⊢ (R \in Ring \land E \in V) \to (\forall i \in \{E\} \forall j \in \{E\} i F (w \cdot_{R} y) j = i (F (w) \cdot_{A} F (y)) j \leftrightarrow E F (w \cdot_{R} y) E = E (F (w) \cdot_{A} F (y)) E)$
71	70	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 \cdot_{R} y) j = i (F (w) \cdot_{A} F (y)) j \leftrightarrow E F (w \cdot_{R} y) E = E (F (w) \cdot_{A} F (y)) E)$
72	62 71	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 \cdot_{R} y) j = i (F (w) \cdot_{A} F (y)) j$
73	1 2 3 4 5	mat1rhmcl	$⊢ (R \in Ring \land E \in V \land w \cdot_{R} y \in K) \to F (w \cdot_{R} y) \in B$
74	22 21 59 73	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to F (w \cdot_{R} y) \in B$
75	13	adantr	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to A \in Ring$
76	3 55	ringcl	$⊢ (A \in Ring \land F (w) \in B \land F (y) \in B) \to F (w) \cdot_{A} F (y) \in B$
77	75 49 51 76	syl3anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to F (w) \cdot_{A} F (y) \in B$
78	2 3	eqmat	$⊢ (F (w \cdot_{R} y) \in B \land F (w) \cdot_{A} F (y) \in B) \to (F (w \cdot_{R} y) = F (w) \cdot_{A} F (y) \leftrightarrow \forall i \in \{E\} \forall j \in \{E\} i F (w \cdot_{R} y) j = i (F (w) \cdot_{A} F (y)) j)$
79	74 77 78	syl2anc	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to (F (w \cdot_{R} y) = F (w) \cdot_{A} F (y) \leftrightarrow \forall i \in \{E\} \forall j \in \{E\} i F (w \cdot_{R} y) j = i (F (w) \cdot_{A} F (y)) j)$
80	72 79	mpbird	$⊢ ((R \in Ring \land E \in V) \land (w \in K \land y \in K)) \to F (w \cdot_{R} y) = F (w) \cdot_{A} F (y)$
81	80	ralrimivva	$⊢ (R \in Ring \land E \in V) \to \forall w \in K \forall y \in K F (w \cdot_{R} y) = F (w) \cdot_{A} F (y)$
82		eqid	$⊢ 1_{R} = 1_{R}$
83	1 82	ringidcl	$⊢ R \in Ring \to 1_{R} \in K$
84	83	adantr	$⊢ (R \in Ring \land E \in V) \to 1_{R} \in K$
85	1 2 3 4 5	mat1rhmval	$⊢ (R \in Ring \land E \in V \land 1_{R} \in K) \to F (1_{R}) = \{⟨O, 1_{R}⟩\}$
86	84 85	mpd3an3	$⊢ (R \in Ring \land E \in V) \to F (1_{R}) = \{⟨O, 1_{R}⟩\}$
87	2 1 4	mat1dimid	$⊢ (R \in Ring \land E \in V) \to 1_{A} = \{⟨O, 1_{R}⟩\}$
88	86 87	eqtr4d	$⊢ (R \in Ring \land E \in V) \to F (1_{R}) = 1_{A}$
89	16 81 88	3jca	$⊢ (R \in Ring \land E \in V) \to (F : K ⟶ B \land \forall w \in K \forall y \in K F (w \cdot_{R} y) = F (w) \cdot_{A} F (y) \land F (1_{R}) = 1_{A})$
90	6 1	mgpbas	$⊢ K = {Base}_{M}$
91	7 3	mgpbas	$⊢ B = {Base}_{N}$
92	6 34	mgpplusg	$⊢ \cdot_{R} = +_{M}$
93	7 55	mgpplusg	$⊢ \cdot_{A} = +_{N}$
94	6 82	ringidval	$⊢ 1_{R} = 0_{M}$
95		eqid	$⊢ 1_{A} = 1_{A}$
96	7 95	ringidval	$⊢ 1_{A} = 0_{N}$
97	90 91 92 93 94 96	ismhm	$⊢ F \in (M MndHom N) \leftrightarrow ((M \in Mnd \land N \in Mnd) \land (F : K ⟶ B \land \forall w \in K \forall y \in K F (w \cdot_{R} y) = F (w) \cdot_{A} F (y) \land F (1_{R}) = 1_{A}))$
98	9 15 89 97	syl21anbrc	$⊢ (R \in Ring \land E \in V) \to F \in (M MndHom N)$

Metamath Proof Explorer

Theorem mat1mhm

Proof