scmatf1

Description: There is a 1-1 function from a ring to any ring of scalar matrices with positive dimension over this ring. (Contributed by AV, 25-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$
Assertion	scmatf1	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to F : K \underset{1-1}{⟶} C$

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	1 2 3 4 5 6	scmatf	$⊢ (N \in Fin \land R \in Ring) \to F : K ⟶ C$
8	7	3adant2	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to F : K ⟶ C$
9		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
10		simpl	$⊢ (y \in K \land z \in K) \to y \in K$
11	1 2 3 4 5	scmatrhmval	$⊢ (R \in Ring \land y \in K) \to F (y) = y \underset{˙}{*} \underset{˙}{1}$
12	9 10 11	syl2an	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to F (y) = y \underset{˙}{*} \underset{˙}{1}$
13		simpr	$⊢ (y \in K \land z \in K) \to z \in K$
14	1 2 3 4 5	scmatrhmval	$⊢ (R \in Ring \land z \in K) \to F (z) = z \underset{˙}{*} \underset{˙}{1}$
15	9 13 14	syl2an	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to F (z) = z \underset{˙}{*} \underset{˙}{1}$
16	12 15	eqeq12d	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (F (y) = F (z) \leftrightarrow y \underset{˙}{} \underset{˙}{1} = z \underset{˙}{} \underset{˙}{1})$
17	16	3adantl2	$⊢ ((N \in Fin \land N \neq \emptyset \land R \in Ring) \land (y \in K \land z \in K)) \to (F (y) = F (z) \leftrightarrow y \underset{˙}{} \underset{˙}{1} = z \underset{˙}{} \underset{˙}{1})$
18	2	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
19		eqid	$⊢ {Base}_{A} = {Base}_{A}$
20	19 3	ringidcl	$⊢ A \in Ring \to \underset{˙}{1} \in {Base}_{A}$
21	18 20	syl	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{1} \in {Base}_{A}$
22	21 10	anim12ci	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (y \in K \land \underset{˙}{1} \in {Base}_{A})$
23	1 2 19 4	matvscl	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land \underset{˙}{1} \in {Base}_{A})) \to y \underset{˙}{*} \underset{˙}{1} \in {Base}_{A}$
24	22 23	syldan	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to y \underset{˙}{*} \underset{˙}{1} \in {Base}_{A}$
25	21 13	anim12ci	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (z \in K \land \underset{˙}{1} \in {Base}_{A})$
26	1 2 19 4	matvscl	$⊢ ((N \in Fin \land R \in Ring) \land (z \in K \land \underset{˙}{1} \in {Base}_{A})) \to z \underset{˙}{*} \underset{˙}{1} \in {Base}_{A}$
27	25 26	syldan	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to z \underset{˙}{*} \underset{˙}{1} \in {Base}_{A}$
28	24 27	jca	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (y \underset{˙}{} \underset{˙}{1} \in {Base}_{A} \land z \underset{˙}{} \underset{˙}{1} \in {Base}_{A})$
29	28	3adantl2	$⊢ ((N \in Fin \land N \neq \emptyset \land R \in Ring) \land (y \in K \land z \in K)) \to (y \underset{˙}{} \underset{˙}{1} \in {Base}_{A} \land z \underset{˙}{} \underset{˙}{1} \in {Base}_{A})$
30	2 19	eqmat	$⊢ (y \underset{˙}{} \underset{˙}{1} \in {Base}_{A} \land z \underset{˙}{} \underset{˙}{1} \in {Base}_{A}) \to (y \underset{˙}{} \underset{˙}{1} = z \underset{˙}{} \underset{˙}{1} \leftrightarrow \forall i \in N \forall j \in N i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j)$
31	29 30	syl	$⊢ ((N \in Fin \land N \neq \emptyset \land R \in Ring) \land (y \in K \land z \in K)) \to (y \underset{˙}{} \underset{˙}{1} = z \underset{˙}{} \underset{˙}{1} \leftrightarrow \forall i \in N \forall j \in N i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j)$
32		difsnid	$⊢ i \in N \to (N ∖ \{i\}) \cup \{i\} = N$
33	32	eqcomd	$⊢ i \in N \to N = (N ∖ \{i\}) \cup \{i\}$
34	33	adantl	$⊢ (((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \land i \in N) \to N = (N ∖ \{i\}) \cup \{i\}$
35	34	raleqdv	$⊢ (((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \land i \in N) \to (\forall j \in N i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \leftrightarrow \forall j \in ((N ∖ \{i\}) \cup \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j)$
36		oveq2	$⊢ j = i \to i (y \underset{˙}{} \underset{˙}{1}) j = i (y \underset{˙}{} \underset{˙}{1}) i$
37		oveq2	$⊢ j = i \to i (z \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) i$
38	36 37	eqeq12d	$⊢ j = i \to (i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \leftrightarrow i (y \underset{˙}{} \underset{˙}{1}) i = i (z \underset{˙}{} \underset{˙}{1}) i)$
39	38	ralunsn	$⊢ i \in N \to (\forall j \in ((N ∖ \{i\}) \cup \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \leftrightarrow (\forall j \in (N ∖ \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \land i (y \underset{˙}{} \underset{˙}{1}) i = i (z \underset{˙}{} \underset{˙}{1}) i))$
40	39	adantl	$⊢ (((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \land i \in N) \to (\forall j \in ((N ∖ \{i\}) \cup \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \leftrightarrow (\forall j \in (N ∖ \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \land i (y \underset{˙}{} \underset{˙}{1}) i = i (z \underset{˙}{} \underset{˙}{1}) i))$
41	10	anim2i	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to ((N \in Fin \land R \in Ring) \land y \in K)$
42		df-3an	$⊢ (N \in Fin \land R \in Ring \land y \in K) \leftrightarrow ((N \in Fin \land R \in Ring) \land y \in K)$
43	41 42	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (N \in Fin \land R \in Ring \land y \in K)$
44		id	$⊢ i \in N \to i \in N$
45	44 44	jca	$⊢ i \in N \to (i \in N \land i \in N)$
46		eqid	$⊢ 0_{R} = 0_{R}$
47	2 1 46 3 4	scmatscmide	$⊢ ((N \in Fin \land R \in Ring \land y \in K) \land (i \in N \land i \in N)) \to i (y \underset{˙}{*} \underset{˙}{1}) i = if (i = i, y, 0_{R})$
48	43 45 47	syl2an	$⊢ (((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \land i \in N) \to i (y \underset{˙}{*} \underset{˙}{1}) i = if (i = i, y, 0_{R})$
49		eqid	$⊢ i = i$
50	49	iftruei	$⊢ if (i = i, y, 0_{R}) = y$
51	48 50	eqtrdi	$⊢ (((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \land i \in N) \to i (y \underset{˙}{*} \underset{˙}{1}) i = y$
52	13	anim2i	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to ((N \in Fin \land R \in Ring) \land z \in K)$
53		df-3an	$⊢ (N \in Fin \land R \in Ring \land z \in K) \leftrightarrow ((N \in Fin \land R \in Ring) \land z \in K)$
54	52 53	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (N \in Fin \land R \in Ring \land z \in K)$
55	2 1 46 3 4	scmatscmide	$⊢ ((N \in Fin \land R \in Ring \land z \in K) \land (i \in N \land i \in N)) \to i (z \underset{˙}{*} \underset{˙}{1}) i = if (i = i, z, 0_{R})$
56	54 45 55	syl2an	$⊢ (((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \land i \in N) \to i (z \underset{˙}{*} \underset{˙}{1}) i = if (i = i, z, 0_{R})$
57	49	iftruei	$⊢ if (i = i, z, 0_{R}) = z$
58	56 57	eqtrdi	$⊢ (((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \land i \in N) \to i (z \underset{˙}{*} \underset{˙}{1}) i = z$
59	51 58	eqeq12d	$⊢ (((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \land i \in N) \to (i (y \underset{˙}{} \underset{˙}{1}) i = i (z \underset{˙}{} \underset{˙}{1}) i \leftrightarrow y = z)$
60	59	anbi2d	$⊢ (((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \land i \in N) \to ((\forall j \in (N ∖ \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \land i (y \underset{˙}{} \underset{˙}{1}) i = i (z \underset{˙}{} \underset{˙}{1}) i) \leftrightarrow (\forall j \in (N ∖ \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \land y = z))$
61	35 40 60	3bitrd	$⊢ (((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \land i \in N) \to (\forall j \in N i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \leftrightarrow (\forall j \in (N ∖ \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \land y = z))$
62	61	ralbidva	$⊢ ((N \in Fin \land R \in Ring) \land (y \in K \land z \in K)) \to (\forall i \in N \forall j \in N i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \leftrightarrow \forall i \in N (\forall j \in (N ∖ \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \land y = z))$
63	62	3adantl2	$⊢ ((N \in Fin \land N \neq \emptyset \land R \in Ring) \land (y \in K \land z \in K)) \to (\forall i \in N \forall j \in N i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \leftrightarrow \forall i \in N (\forall j \in (N ∖ \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \land y = z))$
64		r19.26	$⊢ \forall i \in N (\forall j \in (N ∖ \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \land y = z) \leftrightarrow (\forall i \in N \forall j \in (N ∖ \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \land \forall i \in N y = z)$
65		rspn0	$⊢ N \neq \emptyset \to (\forall i \in N y = z \to y = z)$
66	65	3ad2ant2	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to (\forall i \in N y = z \to y = z)$
67	66	adantr	$⊢ ((N \in Fin \land N \neq \emptyset \land R \in Ring) \land (y \in K \land z \in K)) \to (\forall i \in N y = z \to y = z)$
68	67	com12	$⊢ \forall i \in N y = z \to (((N \in Fin \land N \neq \emptyset \land R \in Ring) \land (y \in K \land z \in K)) \to y = z)$
69	64 68	simplbiim	$⊢ \forall i \in N (\forall j \in (N ∖ \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \land y = z) \to (((N \in Fin \land N \neq \emptyset \land R \in Ring) \land (y \in K \land z \in K)) \to y = z)$
70	69	com12	$⊢ ((N \in Fin \land N \neq \emptyset \land R \in Ring) \land (y \in K \land z \in K)) \to (\forall i \in N (\forall j \in (N ∖ \{i\}) i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \land y = z) \to y = z)$
71	63 70	sylbid	$⊢ ((N \in Fin \land N \neq \emptyset \land R \in Ring) \land (y \in K \land z \in K)) \to (\forall i \in N \forall j \in N i (y \underset{˙}{} \underset{˙}{1}) j = i (z \underset{˙}{} \underset{˙}{1}) j \to y = z)$
72	31 71	sylbid	$⊢ ((N \in Fin \land N \neq \emptyset \land R \in Ring) \land (y \in K \land z \in K)) \to (y \underset{˙}{} \underset{˙}{1} = z \underset{˙}{} \underset{˙}{1} \to y = z)$
73	17 72	sylbid	$⊢ ((N \in Fin \land N \neq \emptyset \land R \in Ring) \land (y \in K \land z \in K)) \to (F (y) = F (z) \to y = z)$
74	73	ralrimivva	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to \forall y \in K \forall z \in K (F (y) = F (z) \to y = z)$
75		dff13	$⊢ F : K \underset{1-1}{⟶} C \leftrightarrow (F : K ⟶ C \land \forall y \in K \forall z \in K (F (y) = F (z) \to y = z))$
76	8 74 75	sylanbrc	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to F : K \underset{1-1}{⟶} C$

Metamath Proof Explorer

Theorem scmatf1

Proof