scmatghm

Description: There is a group homomorphism from the additive group of a ring to the additive group of the ring of scalar matrices over this ring. (Contributed by AV, 22-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$
Assertion	scmatghm	$⊢ (N \in Fin \land R \in Ring) \to F \in (R GrpHom S)$

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		eqid	$⊢ {Base}_{S} = {Base}_{S}$
9		eqid	$⊢ +_{R} = +_{R}$
10		eqid	$⊢ +_{S} = +_{S}$
11		ringgrp	$⊢ R \in Ring \to R \in Grp$
12	11	adantl	$⊢ (N \in Fin \land R \in Ring) \to R \in Grp$
13		eqid	$⊢ {Base}_{A} = {Base}_{A}$
14		eqid	$⊢ 0_{R} = 0_{R}$
15	2 13 1 14 6	scmatsgrp	$⊢ (N \in Fin \land R \in Ring) \to C \in SubGrp (A)$
16	7	subggrp	$⊢ C \in SubGrp (A) \to S \in Grp$
17	15 16	syl	$⊢ (N \in Fin \land R \in Ring) \to S \in Grp$
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	2	matsca2	$⊢ (N \in Fin \land R \in Ring) \to R = Scalar (A)$
23	6	ovexi	$⊢ C \in V$
24		eqid	$⊢ Scalar (A) = Scalar (A)$
25	7 24	resssca	$⊢ C \in V \to Scalar (A) = Scalar (S)$
26	23 25	mp1i	$⊢ (N \in Fin \land R \in Ring) \to Scalar (A) = Scalar (S)$
27	22 26	eqtrd	$⊢ (N \in Fin \land R \in Ring) \to R = Scalar (S)$
28	27	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to +_{R} = +_{Scalar (S)}$
29	28	oveqd	$⊢ (N \in Fin \land R \in Ring) \to y +_{R} z = y +_{Scalar (S)} z$
30	29	oveq1d	$⊢ (N \in Fin \land R \in Ring) \to (y +_{R} z) \underset{˙}{} \underset{˙}{1} = (y +_{Scalar (S)} z) \underset{˙}{} \underset{˙}{1}$
31	30	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (y +_{R} z) \underset{˙}{} \underset{˙}{1} = (y +_{Scalar (S)} z) \underset{˙}{} \underset{˙}{1}$
32	2	matlmod	$⊢ (N \in Fin \land R \in Ring) \to A \in LMod$
33	2 6	scmatlss	$⊢ (N \in Fin \land R \in Ring) \to C \in LSubSp (A)$
34		eqid	$⊢ LSubSp (A) = LSubSp (A)$
35	7 34	lsslmod	$⊢ (A \in LMod \land C \in LSubSp (A)) \to S \in LMod$
36	32 33 35	syl2anc	$⊢ (N \in Fin \land R \in Ring) \to S \in LMod$
37	36	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to S \in LMod$
38	27	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{R} = {Base}_{Scalar (S)}$
39	1 38	syl5eq	$⊢ (N \in Fin \land R \in Ring) \to K = {Base}_{Scalar (S)}$
40	39	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (y \in K \leftrightarrow y \in {Base}_{Scalar (S)})$
41	40	biimpd	$⊢ (N \in Fin \land R \in Ring) \to (y \in K \to y \in {Base}_{Scalar (S)})$
42	41	adantrd	$⊢ (N \in Fin \land R \in Ring) \to ((y \in K \land z \in K) \to y \in {Base}_{Scalar (S)})$
43	42	imp	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to y \in {Base}_{Scalar (S)}$
44	39	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (z \in K \leftrightarrow z \in {Base}_{Scalar (S)})$
45	44	biimpd	$⊢ (N \in Fin \land R \in Ring) \to (z \in K \to z \in {Base}_{Scalar (S)})$
46	45	adantld	$⊢ (N \in Fin \land R \in Ring) \to ((y \in K \land z \in K) \to z \in {Base}_{Scalar (S)})$
47	46	imp	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to z \in {Base}_{Scalar (S)}$
48	2 13 1 14 6	scmatid	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in C$
49	3	a1i	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{1} = 1_{A}$
50	48 49 19	3eltr4d	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{1} \in {Base}_{S}$
51	50	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to \underset{˙}{1} \in {Base}_{S}$
52		eqid	$⊢ Scalar (S) = Scalar (S)$
53	7 4	ressvsca	$⊢ C \in V \to \underset{˙}{*} = \cdot_{S}$
54	23 53	ax-mp	$⊢ \underset{˙}{*} = \cdot_{S}$
55		eqid	$⊢ {Base}_{Scalar (S)} = {Base}_{Scalar (S)}$
56		eqid	$⊢ +_{Scalar (S)} = +_{Scalar (S)}$
57	8 10 52 54 55 56	lmodvsdir	$⊢ (S \in LMod \land (y \in {Base}_{Scalar (S)} \land z \in {Base}_{Scalar (S)} \land \underset{˙}{1} \in {Base}_{S})) \to (y +_{Scalar (S)} z) \underset{˙}{} \underset{˙}{1} = (y \underset{˙}{} \underset{˙}{1}) +_{S} (z \underset{˙}{*} \underset{˙}{1})$
58	37 43 47 51 57	syl13anc	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (y +_{Scalar (S)} z) \underset{˙}{} \underset{˙}{1} = (y \underset{˙}{} \underset{˙}{1}) +_{S} (z \underset{˙}{*} \underset{˙}{1})$
59	31 58	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (y +_{R} z) \underset{˙}{} \underset{˙}{1} = (y \underset{˙}{} \underset{˙}{1}) +_{S} (z \underset{˙}{*} \underset{˙}{1})$
60		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
61	60	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to R \in Ring$
62	60	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))$
63		3anass	$⊢ (R \in Ring \land y \in K \land z \in K) \leftrightarrow (R \in Ring \land (y \in K \land z \in K))$
64	62 63	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)$
65	1 9	ringacl	$⊢ (R \in Ring \land y \in K \land z \in K) \to y +_{R} z \in K$
66	64 65	syl	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to y +_{R} z \in K$
67	1 2 3 4 5	scmatrhmval	$⊢ (R \in Ring \land y +_{R} z \in K) \to F (y +_{R} z) = (y +_{R} z) \underset{˙}{*} \underset{˙}{1}$
68	61 66 67	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to F (y +_{R} z) = (y +_{R} z) \underset{˙}{*} \underset{˙}{1}$
69	1 2 3 4 5	scmatrhmval	$⊢ (R \in Ring \land y \in K) \to F (y) = y \underset{˙}{*} \underset{˙}{1}$
70	69	ad2ant2lr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to F (y) = y \underset{˙}{*} \underset{˙}{1}$
71	1 2 3 4 5	scmatrhmval	$⊢ (R \in Ring \land z \in K) \to F (z) = z \underset{˙}{*} \underset{˙}{1}$
72	71	ad2ant2l	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to F (z) = z \underset{˙}{*} \underset{˙}{1}$
73	70 72	oveq12d	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to F (y) +_{S} F (z) = (y \underset{˙}{} \underset{˙}{1}) +_{S} (z \underset{˙}{} \underset{˙}{1})$
74	59 68 73	3eqtr4d	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to F (y +_{R} z) = F (y) +_{S} F (z)$
75	1 8 9 10 12 17 21 74	isghmd	$⊢ (N \in Fin \land R \in Ring) \to F \in (R GrpHom S)$

Metamath Proof Explorer

Theorem scmatghm

Proof