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	biimpi	$⊢ X \in K \to X \in {Base}_{R}$
24	23	adantr	$⊢ (X \in K \land Y \in B) \to X \in {Base}_{R}$
25	24	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}$
26		eqid	$⊢ {Base}_{R} = {Base}_{R}$
27		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$
28		simpr	$⊢ (i \in N \land j \in N) \to j \in N$
29	28	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$
30		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$
31	2 26 3 27 29 30	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}$
32		eqid	$⊢ \cdot_{R} = \cdot_{R}$
33		eqid	$⊢ \cdot_{P} = \cdot_{P}$
34	26 32 33	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)$
35	21 25 31 34	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)$
36		crngring	$⊢ R \in CRing \to R \in Ring$
37	36	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to R \in Ring$
38	37	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$
39		simpr	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to (X \in K \land Y \in B)$
40	39	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)$
41		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)$
42	2 3 7 9 32	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)$
43	38 40 41 42	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)$
44	43	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))$
45	36	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
46		simpr	$⊢ (X \in K \land Y \in B) \to Y \in B$
47	45 46	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)$
48		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)$
49	47 48	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)$
50	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)$
51	49 50	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)$
52	51	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)$
53	35 44 52	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)$
54		simpll	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to N \in Fin$
55	54	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$
56	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$
57	45 56	sylan	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to X \underset{˙}{\cdot} Y \in B$
58	57	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$
59	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)$
60	55 38 58 41 59	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)$
61	4	ply1ring	$⊢ R \in Ring \to P \in Ring$
62	36 61	syl	$⊢ R \in CRing \to P \in Ring$
63	62	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to P \in Ring$
64	63	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$
65	36	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Ring$
66		simpl	$⊢ (X \in K \land Y \in B) \to X \in K$
67		eqid	$⊢ {Base}_{P} = {Base}_{P}$
68	4 8 7 67	ply1sclcl	$⊢ (R \in Ring \land X \in K) \to S (X) \in {Base}_{P}$
69	65 66 68	syl2an	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to S (X) \in {Base}_{P}$
70	1 2 3 4 5 6	mat2pmatbas0	$⊢ (N \in Fin \land R \in Ring \land Y \in B) \to T (Y) \in H$
71	49 70	syl	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to T (Y) \in H$
72	69 71	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)$
73	72	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)$
74	5 6 67 10 33	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)$
75	64 73 41 74	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)$
76	53 60 75	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$
77	76	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$
78	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$
79	54 37 57 78	syl3anc	$⊢ ((N \in Fin \land R \in CRing) \land (X \in K \land Y \in B)) \to T (X \underset{˙}{\cdot} Y) \in H$
80	67 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$
81	54 63 72 80	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$
82	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)$
83	79 81 82	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)$
84	77 83	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