scmatmhm

Description: There is a monoid homomorphism from the multiplicative group of a ring to the multiplicative group of the ring of scalar matrices over this ring. (Contributed by AV, 29-Dec-2019)

	Ref	Expression
Hypotheses	scmatrhmval.k	$⊢ K = {Base}_{R}$
	scmatrhmval.a	$⊢ A = N Mat R$
	scmatrhmval.o	$⊢ \underset{˙}{1} = 1_{A}$
	scmatrhmval.t	$⊢ \underset{˙}{*} = \cdot_{A}$
	scmatrhmval.f	$⊢ F = (x \in K ⟼ x \underset{˙}{*} \underset{˙}{1})$
	scmatrhmval.c	$⊢ C = N ScMat R$
	scmatghm.s	$⊢ S = A ↾_{𝑠} C$
	scmatmhm.m	$⊢ M = {mulGrp}_{R}$
	scmatmhm.t	$⊢ T = {mulGrp}_{S}$
Assertion	scmatmhm	$⊢ (N \in Fin \land R \in Ring) \to F \in (M MndHom T)$

Proof

Step	Hyp	Ref	Expression
1		scmatrhmval.k	$⊢ K = {Base}_{R}$
2		scmatrhmval.a	$⊢ A = N Mat R$
3		scmatrhmval.o	$⊢ \underset{˙}{1} = 1_{A}$
4		scmatrhmval.t	$⊢ \underset{˙}{*} = \cdot_{A}$
5		scmatrhmval.f	$⊢ F = (x \in K ⟼ x \underset{˙}{*} \underset{˙}{1})$
6		scmatrhmval.c	$⊢ C = N ScMat R$
7		scmatghm.s	$⊢ S = A ↾_{𝑠} C$
8		scmatmhm.m	$⊢ M = {mulGrp}_{R}$
9		scmatmhm.t	$⊢ T = {mulGrp}_{S}$
10	8	ringmgp	$⊢ R \in Ring \to M \in Mnd$
11	10	adantl	$⊢ (N \in Fin \land R \in Ring) \to M \in Mnd$
12		eqid	$⊢ {Base}_{A} = {Base}_{A}$
13		eqid	$⊢ 0_{R} = 0_{R}$
14	2 12 1 13 6	scmatsrng	$⊢ (N \in Fin \land R \in Ring) \to C \in SubRing (A)$
15	7	subrgring	$⊢ C \in SubRing (A) \to S \in Ring$
16	9	ringmgp	$⊢ S \in Ring \to T \in Mnd$
17	14 15 16	3syl	$⊢ (N \in Fin \land R \in Ring) \to T \in Mnd$
18	1 2 3 4 5 6	scmatf	$⊢ (N \in Fin \land R \in Ring) \to F : K ⟶ C$
19	2 6 7	scmatstrbas	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{S} = C$
20	19	feq3d	$⊢ (N \in Fin \land R \in Ring) \to (F : K ⟶ {Base}_{S} \leftrightarrow F : K ⟶ C)$
21	18 20	mpbird	$⊢ (N \in Fin \land R \in Ring) \to F : K ⟶ {Base}_{S}$
22		eqid	$⊢ \cdot_{R} = \cdot_{R}$
23		eqid	$⊢ \cdot_{A} = \cdot_{A}$
24	2 1 13 3 4 22 23	scmatscmiddistr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (y \underset{˙}{} \underset{˙}{1}) \cdot_{A} (z \underset{˙}{} \underset{˙}{1}) = (y \cdot_{R} z) \underset{˙}{*} \underset{˙}{1}$
25	7 23	ressmulr	$⊢ C \in SubRing (A) \to \cdot_{A} = \cdot_{S}$
26	14 25	syl	$⊢ (N \in Fin \land R \in Ring) \to \cdot_{A} = \cdot_{S}$
27	26	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to \cdot_{A} = \cdot_{S}$
28	27	oveqd	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (y \underset{˙}{} \underset{˙}{1}) \cdot_{A} (z \underset{˙}{} \underset{˙}{1}) = (y \underset{˙}{} \underset{˙}{1}) \cdot_{S} (z \underset{˙}{} \underset{˙}{1})$
29	24 28	eqtr3d	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (y \cdot_{R} z) \underset{˙}{} \underset{˙}{1} = (y \underset{˙}{} \underset{˙}{1}) \cdot_{S} (z \underset{˙}{*} \underset{˙}{1})$
30		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
31	30	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to R \in Ring$
32	30	anim1i	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (R \in Ring \land (y \in K \land z \in K))$
33		3anass	$⊢ (R \in Ring \land y \in K \land z \in K) \leftrightarrow (R \in Ring \land (y \in K \land z \in K))$
34	32 33	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (R \in Ring \land y \in K \land z \in K)$
35	1 22	ringcl	$⊢ (R \in Ring \land y \in K \land z \in K) \to y \cdot_{R} z \in K$
36	34 35	syl	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to y \cdot_{R} z \in K$
37	1 2 3 4 5	scmatrhmval	$⊢ (R \in Ring \land y \cdot_{R} z \in K) \to F (y \cdot_{R} z) = (y \cdot_{R} z) \underset{˙}{*} \underset{˙}{1}$
38	31 36 37	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to F (y \cdot_{R} z) = (y \cdot_{R} z) \underset{˙}{*} \underset{˙}{1}$
39	1 2 3 4 5	scmatrhmval	$⊢ (R \in Ring \land y \in K) \to F (y) = y \underset{˙}{*} \underset{˙}{1}$
40	39	ad2ant2lr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to F (y) = y \underset{˙}{*} \underset{˙}{1}$
41	1 2 3 4 5	scmatrhmval	$⊢ (R \in Ring \land z \in K) \to F (z) = z \underset{˙}{*} \underset{˙}{1}$
42	41	ad2ant2l	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to F (z) = z \underset{˙}{*} \underset{˙}{1}$
43	40 42	oveq12d	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to F (y) \cdot_{S} F (z) = (y \underset{˙}{} \underset{˙}{1}) \cdot_{S} (z \underset{˙}{} \underset{˙}{1})$
44	29 38 43	3eqtr4d	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to F (y \cdot_{R} z) = F (y) \cdot_{S} F (z)$
45	44	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall y \in K \forall z \in K F (y \cdot_{R} z) = F (y) \cdot_{S} F (z)$
46		eqid	$⊢ 1_{R} = 1_{R}$
47	1 46	ringidcl	$⊢ R \in Ring \to 1_{R} \in K$
48	1 2 3 4 5	scmatrhmval	$⊢ (R \in Ring \land 1_{R} \in K) \to F (1_{R}) = 1_{R} \underset{˙}{*} \underset{˙}{1}$
49	30 47 48	syl2anc2	$⊢ (N \in Fin \land R \in Ring) \to F (1_{R}) = 1_{R} \underset{˙}{*} \underset{˙}{1}$
50	2	matsca2	$⊢ (N \in Fin \land R \in Ring) \to R = Scalar (A)$
51	50	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to 1_{R} = 1_{Scalar (A)}$
52	51	oveq1d	$⊢ (N \in Fin \land R \in Ring) \to 1_{R} \underset{˙}{} \underset{˙}{1} = 1_{Scalar (A)} \underset{˙}{} \underset{˙}{1}$
53	2	matlmod	$⊢ (N \in Fin \land R \in Ring) \to A \in LMod$
54	2	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
55	12 3	ringidcl	$⊢ A \in Ring \to \underset{˙}{1} \in {Base}_{A}$
56	54 55	syl	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{1} \in {Base}_{A}$
57		eqid	$⊢ Scalar (A) = Scalar (A)$
58		eqid	$⊢ 1_{Scalar (A)} = 1_{Scalar (A)}$
59	12 57 4 58	lmodvs1	$⊢ (A \in LMod \land \underset{˙}{1} \in {Base}_{A}) \to 1_{Scalar (A)} \underset{˙}{*} \underset{˙}{1} = \underset{˙}{1}$
60	53 56 59	syl2anc	$⊢ (N \in Fin \land R \in Ring) \to 1_{Scalar (A)} \underset{˙}{*} \underset{˙}{1} = \underset{˙}{1}$
61	52 60	eqtrd	$⊢ (N \in Fin \land R \in Ring) \to 1_{R} \underset{˙}{*} \underset{˙}{1} = \underset{˙}{1}$
62	49 61	eqtrd	$⊢ (N \in Fin \land R \in Ring) \to F (1_{R}) = \underset{˙}{1}$
63	7 3	subrg1	$⊢ C \in SubRing (A) \to \underset{˙}{1} = 1_{S}$
64	14 63	syl	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{1} = 1_{S}$
65	62 64	eqtrd	$⊢ (N \in Fin \land R \in Ring) \to F (1_{R}) = 1_{S}$
66	21 45 65	3jca	$⊢ (N \in Fin \land R \in Ring) \to (F : K ⟶ {Base}_{S} \land \forall y \in K \forall z \in K F (y \cdot_{R} z) = F (y) \cdot_{S} F (z) \land F (1_{R}) = 1_{S})$
67	8 1	mgpbas	$⊢ K = {Base}_{M}$
68		eqid	$⊢ {Base}_{S} = {Base}_{S}$
69	9 68	mgpbas	$⊢ {Base}_{S} = {Base}_{T}$
70	8 22	mgpplusg	$⊢ \cdot_{R} = +_{M}$
71		eqid	$⊢ \cdot_{S} = \cdot_{S}$
72	9 71	mgpplusg	$⊢ \cdot_{S} = +_{T}$
73	8 46	ringidval	$⊢ 1_{R} = 0_{M}$
74		eqid	$⊢ 1_{S} = 1_{S}$
75	9 74	ringidval	$⊢ 1_{S} = 0_{T}$
76	67 69 70 72 73 75	ismhm	$⊢ F \in (M MndHom T) \leftrightarrow ((M \in Mnd \land T \in Mnd) \land (F : K ⟶ {Base}_{S} \land \forall y \in K \forall z \in K F (y \cdot_{R} z) = F (y) \cdot_{S} F (z) \land F (1_{R}) = 1_{S}))$
77	11 17 66 76	syl21anbrc	$⊢ (N \in Fin \land R \in Ring) \to F \in (M MndHom T)$

Metamath Proof Explorer

Theorem scmatmhm

Proof