mat2pmatlin

Description: The transformation of matrices into polynomial matrices is "linear", analogous to lmhmlin . Since A and C have different scalar rings, T cannot be a left module homomorphism as defined in df-lmhm , see lmhmsca . (Contributed by AV, 13-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

	Ref	Expression
Hypotheses	mat2pmatbas.t	$⊢ T = N matToPolyMat R$
	mat2pmatbas.a	$⊢ A = N Mat R$
	mat2pmatbas.b	$⊢ B = {Base}_{A}$
	mat2pmatbas.p	$⊢ P = {Poly}_{1} (R)$
	mat2pmatbas.c	$⊢ C = N Mat P$
	mat2pmatbas0.h	$⊢ H = {Base}_{C}$
	mat2pmatlin.k	$⊢ K = {Base}_{R}$
	mat2pmatlin.s	$⊢ S = algSc (P)$
	mat2pmatlin.m	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
	mat2pmatlin.n	$⊢ \underset{˙}{\times} = \cdot_{C}$
Assertion	mat2pmatlin	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to T (X \underset{˙}{\cdot} Y) = S (X) \underset{˙}{\times} T (Y)$

Proof

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	$⊢ T = N matToPolyMat R$
2		mat2pmatbas.a	$⊢ A = N Mat R$
3		mat2pmatbas.b	$⊢ B = {Base}_{A}$
4		mat2pmatbas.p	$⊢ P = {Poly}_{1} (R)$
5		mat2pmatbas.c	$⊢ C = N Mat P$
6		mat2pmatbas0.h	$⊢ H = {Base}_{C}$
7		mat2pmatlin.k	$⊢ K = {Base}_{R}$
8		mat2pmatlin.s	$⊢ S = algSc (P)$
9		mat2pmatlin.m	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
10		mat2pmatlin.n	$⊢ \underset{˙}{\times} = \cdot_{C}$
11		simpr	$⊢ (N \in Fin \land R \in CRing) \to R \in CRing$
12	4	ply1assa	$⊢ R \in CRing \to P \in AssAlg$
13		eqid	$⊢ Scalar (P) = Scalar (P)$
14	8 13	asclrhm	$⊢ P \in AssAlg \to S \in (Scalar (P) RingHom P)$
15	11 12 14	3syl	$⊢ (N \in Fin \land R \in CRing) \to S \in (Scalar (P) RingHom P)$
16	4	ply1sca	$⊢ R \in CRing \to R = Scalar (P)$
17	16	adantl	$⊢ (N \in Fin \land R \in CRing) \to R = Scalar (P)$
18	17	oveq1d	$⊢ (N \in Fin \land R \in CRing) \to R RingHom P = Scalar (P) RingHom P$
19	15 18	eleqtrrd	$⊢ (N \in Fin \land R \in CRing) \to S \in (R RingHom P)$
20	19	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to S \in (R RingHom P)$
21	20	adantr	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to S \in (R RingHom P)$
22	7	eleq2i	$⊢ X \in K \leftrightarrow X \in {Base}_{R}$
23	22	birani	$⊢ (X \in K \land Y \in B) \to X \in {Base}_{R}$
24	23	ad2antlr	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to X \in {Base}_{R}$
25		eqid	$⊢ {Base}_{R} = {Base}_{R}$
26		simprl	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to i \in N$
27		simpr	$⊢ (i \in N \land j \in N) \to j \in N$
28	27	adantl	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to j \in N$
29		simplrr	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to Y \in B$
30	2 25 3 26 28 29	matecld	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to i Y j \in {Base}_{R}$
31		eqid	$⊢ \cdot_{R} = \cdot_{R}$
32		eqid	$⊢ \cdot_{P} = \cdot_{P}$
33	25 31 32	rhmmul	$⊢ (S \in (R RingHom P) \land X \in {Base}_{R} \land i Y j \in {Base}_{R}) \to S (X \cdot_{R} (i Y j)) = S (X) \cdot_{P} S (i Y j)$
34	21 24 30 33	syl3anc	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to S (X \cdot_{R} (i Y j)) = S (X) \cdot_{P} S (i Y j)$
35		crngring	$⊢ R \in CRing \to R \in Ring$
36	35	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to R \in Ring$
37	36	adantr	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to R \in Ring$
38		simpr	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to (X \in K \land Y \in B)$
39	38	adantr	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to (X \in K \land Y \in B)$
40		simpr	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to (i \in N \land j \in N)$
41	2 3 7 9 31	matvscacell	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land (i \in N \land j \in N)) \to i (X \underset{˙}{\cdot} Y) j = X \cdot_{R} (i Y j)$
42	37 39 40 41	syl3anc	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to i (X \underset{˙}{\cdot} Y) j = X \cdot_{R} (i Y j)$
43	42	fveq2d	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to S (i (X \underset{˙}{\cdot} Y) j) = S (X \cdot_{R} (i Y j))$
44	35	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
45		simpr	$⊢ (X \in K \land Y \in B) \to Y \in B$
46	44 45	anim12i	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to ((N \in Fin \land R \in Ring) \land Y \in B)$
47		df-3an	$⊢ (N \in Fin \land R \in Ring \land Y \in B) \leftrightarrow ((N \in Fin \land R \in Ring) \land Y \in B)$
48	46 47	sylibr	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to (N \in Fin \land R \in Ring \land Y \in B)$
49	1 2 3 4 8	mat2pmatvalel	$⊢ ((N \in Fin \land R \in Ring \land Y \in B) \land (i \in N \land j \in N)) \to i T (Y) j = S (i Y j)$
50	48 49	sylan	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to i T (Y) j = S (i Y j)$
51	50	oveq2d	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to S (X) \cdot_{P} (i T (Y) j) = S (X) \cdot_{P} S (i Y j)$
52	34 43 51	3eqtr4d	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to S (i (X \underset{˙}{\cdot} Y) j) = S (X) \cdot_{P} (i T (Y) j)$
53		simpll	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to N \in Fin$
54	53	adantr	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to N \in Fin$
55	7 2 3 9	matvscl	$⊢ ((N \in Fin \land R \in Ring) \land (X \in K \land Y \in B)) \to X \underset{˙}{\cdot} Y \in B$
56	44 55	sylan	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to X \underset{˙}{\cdot} Y \in B$
57	56	adantr	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to X \underset{˙}{\cdot} Y \in B$
58	1 2 3 4 8	mat2pmatvalel	$⊢ ((N \in Fin \land R \in Ring \land X \underset{˙}{\cdot} Y \in B) \land (i \in N \land j \in N)) \to i T (X \underset{˙}{\cdot} Y) j = S (i (X \underset{˙}{\cdot} Y) j)$
59	54 37 57 40 58	syl31anc	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to i T (X \underset{˙}{\cdot} Y) j = S (i (X \underset{˙}{\cdot} Y) j)$
60	4	ply1ring	$⊢ R \in Ring \to P \in Ring$
61	35 60	syl	$⊢ R \in CRing \to P \in Ring$
62	61	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to P \in Ring$
63	62	adantr	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to P \in Ring$
64	35	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Ring$
65		simpl	$⊢ (X \in K \land Y \in B) \to X \in K$
66		eqid	$⊢ {Base}_{P} = {Base}_{P}$
67	4 8 7 66	ply1sclcl	$⊢ (R \in Ring \land X \in K) \to S (X) \in {Base}_{P}$
68	64 65 67	syl2an	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to S (X) \in {Base}_{P}$
69	1 2 3 4 5 6	mat2pmatbas0	$⊢ (N \in Fin \land R \in Ring \land Y \in B) \to T (Y) \in H$
70	48 69	syl	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to T (Y) \in H$
71	68 70	jca	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to (S (X) \in {Base}_{P} \land T (Y) \in H)$
72	71	adantr	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to (S (X) \in {Base}_{P} \land T (Y) \in H)$
73	5 6 66 10 32	matvscacell	$⊢ (P \in Ring \land (S (X) \in {Base}_{P} \land T (Y) \in H) \land (i \in N \land j \in N)) \to i (S (X) \underset{˙}{\times} T (Y)) j = S (X) \cdot_{P} (i T (Y) j)$
74	63 72 40 73	syl3anc	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to i (S (X) \underset{˙}{\times} T (Y)) j = S (X) \cdot_{P} (i T (Y) j)$
75	52 59 74	3eqtr4d	$⊢ (((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \land (i \in N \land j \in N)) \to i T (X \underset{˙}{\cdot} Y) j = i (S (X) \underset{˙}{\times} T (Y)) j$
76	75	ralrimivva	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to \forall i \in N \forall j \in N i T (X \underset{˙}{\cdot} Y) j = i (S (X) \underset{˙}{\times} T (Y)) j$
77	1 2 3 4 5 6	mat2pmatbas0	$⊢ (N \in Fin \land R \in Ring \land X \underset{˙}{\cdot} Y \in B) \to T (X \underset{˙}{\cdot} Y) \in H$
78	53 36 56 77	syl3anc	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to T (X \underset{˙}{\cdot} Y) \in H$
79	66 5 6 10	matvscl	$⊢ ((N \in Fin \land P \in Ring) \land (S (X) \in {Base}_{P} \land T (Y) \in H)) \to S (X) \underset{˙}{\times} T (Y) \in H$
80	53 62 71 79	syl21anc	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to S (X) \underset{˙}{\times} T (Y) \in H$
81	5 6	eqmat	$⊢ (T (X \underset{˙}{\cdot} Y) \in H \land S (X) \underset{˙}{\times} T (Y) \in H) \to (T (X \underset{˙}{\cdot} Y) = S (X) \underset{˙}{\times} T (Y) \leftrightarrow \forall i \in N \forall j \in N i T (X \underset{˙}{\cdot} Y) j = i (S (X) \underset{˙}{\times} T (Y)) j)$
82	78 80 81	syl2anc	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to (T (X \underset{˙}{\cdot} Y) = S (X) \underset{˙}{\times} T (Y) \leftrightarrow \forall i \in N \forall j \in N i T (X \underset{˙}{\cdot} Y) j = i (S (X) \underset{˙}{\times} T (Y)) j)$
83	76 82	mpbird	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to T (X \underset{˙}{\cdot} Y) = S (X) \underset{˙}{\times} T (Y)$

Metamath Proof Explorer

Theorem mat2pmatlin

Proof