chpdmatlem2

	Ref	Expression
Hypotheses	chpdmat.c	$⊢ C = N CharPlyMat R$
	chpdmat.p	$⊢ P = {Poly}_{1} (R)$
	chpdmat.a	$⊢ A = N Mat R$
	chpdmat.s	$⊢ S = algSc (P)$
	chpdmat.b	$⊢ B = {Base}_{A}$
	chpdmat.x	$⊢ X = {var}_{1} (R)$
	chpdmat.0	$⊢ \underset{˙}{0} = 0_{R}$
	chpdmat.g	$⊢ G = {mulGrp}_{P}$
	chpdmat.m	$⊢ \underset{˙}{-} = -_{P}$
	chpdmatlem.q	$⊢ Q = N Mat P$
	chpdmatlem.1	$⊢ \underset{˙}{1} = 1_{Q}$
	chpdmatlem.m	$⊢ \underset{˙}{\cdot} = \cdot_{Q}$
	chpdmatlem.z	$⊢ Z = -_{Q}$
	chpdmatlem.t	$⊢ T = N matToPolyMat R$
Assertion	chpdmatlem2	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to i ((X \underset{˙}{\cdot} \underset{˙}{1}) Z T (M)) j = 0_{P}$

Proof

Step	Hyp	Ref	Expression
1		chpdmat.c	$⊢ C = N CharPlyMat R$
2		chpdmat.p	$⊢ P = {Poly}_{1} (R)$
3		chpdmat.a	$⊢ A = N Mat R$
4		chpdmat.s	$⊢ S = algSc (P)$
5		chpdmat.b	$⊢ B = {Base}_{A}$
6		chpdmat.x	$⊢ X = {var}_{1} (R)$
7		chpdmat.0	$⊢ \underset{˙}{0} = 0_{R}$
8		chpdmat.g	$⊢ G = {mulGrp}_{P}$
9		chpdmat.m	$⊢ \underset{˙}{-} = -_{P}$
10		chpdmatlem.q	$⊢ Q = N Mat P$
11		chpdmatlem.1	$⊢ \underset{˙}{1} = 1_{Q}$
12		chpdmatlem.m	$⊢ \underset{˙}{\cdot} = \cdot_{Q}$
13		chpdmatlem.z	$⊢ Z = -_{Q}$
14		chpdmatlem.t	$⊢ T = N matToPolyMat R$
15	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
16	15	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to P \in Ring$
17	16	ad4antr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to P \in Ring$
18	1 2 3 4 5 6 7 8 9 10 11 12	chpdmatlem0	$⊢ (N \in Fin \land R \in Ring) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Q}$
19	18	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Q}$
20	19	ad4antr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Q}$
21	14 3 5 2 10	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Q}$
22	21	ad4antr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to T (M) \in {Base}_{Q}$
23		simpr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \to i \in N$
24	23	anim1i	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \to (i \in N \land j \in N)$
25	24	ad2antrr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to (i \in N \land j \in N)$
26		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
27	10 26 13 9	matsubgcell	$⊢ (P \in Ring \land (X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Q} \land T (M) \in {Base}_{Q}) \land (i \in N \land j \in N)) \to i ((X \underset{˙}{\cdot} \underset{˙}{1}) Z T (M)) j = (i (X \underset{˙}{\cdot} \underset{˙}{1}) j) \underset{˙}{-} (i T (M) j)$
28	17 20 22 25 27	syl121anc	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to i ((X \underset{˙}{\cdot} \underset{˙}{1}) Z T (M)) j = (i (X \underset{˙}{\cdot} \underset{˙}{1}) j) \underset{˙}{-} (i T (M) j)$
29	16	ad2antrr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \to P \in Ring$
30		eqid	$⊢ {Base}_{P} = {Base}_{P}$
31	6 2 30	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
32	31	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to X \in {Base}_{P}$
33	2 10	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Q \in Ring$
34	33	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to Q \in Ring$
35	26 11	ringidcl	$⊢ Q \in Ring \to \underset{˙}{1} \in {Base}_{Q}$
36	34 35	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \underset{˙}{1} \in {Base}_{Q}$
37	32 36	jca	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (X \in {Base}_{P} \land \underset{˙}{1} \in {Base}_{Q})$
38	37	ad2antrr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \to (X \in {Base}_{P} \land \underset{˙}{1} \in {Base}_{Q})$
39	29 38 24	3jca	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \to (P \in Ring \land (X \in {Base}_{P} \land \underset{˙}{1} \in {Base}_{Q}) \land (i \in N \land j \in N))$
40	39	ad2antrr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to (P \in Ring \land (X \in {Base}_{P} \land \underset{˙}{1} \in {Base}_{Q}) \land (i \in N \land j \in N))$
41		eqid	$⊢ \cdot_{P} = \cdot_{P}$
42	10 26 30 12 41	matvscacell	$⊢ (P \in Ring \land (X \in {Base}_{P} \land \underset{˙}{1} \in {Base}_{Q}) \land (i \in N \land j \in N)) \to i (X \underset{˙}{\cdot} \underset{˙}{1}) j = X \cdot_{P} (i \underset{˙}{1} j)$
43	40 42	syl	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to i (X \underset{˙}{\cdot} \underset{˙}{1}) j = X \cdot_{P} (i \underset{˙}{1} j)$
44	43	oveq1d	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to (i (X \underset{˙}{\cdot} \underset{˙}{1}) j) \underset{˙}{-} (i T (M) j) = (X \cdot_{P} (i \underset{˙}{1} j)) \underset{˙}{-} (i T (M) j)$
45		eqid	$⊢ 1_{P} = 1_{P}$
46		eqid	$⊢ 0_{P} = 0_{P}$
47		simpll1	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \to N \in Fin$
48	23	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \to i \in N$
49		simpr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \to j \in N$
50	10 45 46 47 29 48 49 11	mat1ov	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \to i \underset{˙}{1} j = if (i = j, 1_{P}, 0_{P})$
51		ifnefalse	$⊢ i \neq j \to if (i = j, 1_{P}, 0_{P}) = 0_{P}$
52	50 51	sylan9eq	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \to i \underset{˙}{1} j = 0_{P}$
53	52	oveq2d	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \to X \cdot_{P} (i \underset{˙}{1} j) = X \cdot_{P} 0_{P}$
54	15 31	jca	$⊢ R \in Ring \to (P \in Ring \land X \in {Base}_{P})$
55	54	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (P \in Ring \land X \in {Base}_{P})$
56	30 41 46	ringrz	$⊢ (P \in Ring \land X \in {Base}_{P}) \to X \cdot_{P} 0_{P} = 0_{P}$
57	55 56	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to X \cdot_{P} 0_{P} = 0_{P}$
58	57	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \to X \cdot_{P} 0_{P} = 0_{P}$
59	58	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \to X \cdot_{P} 0_{P} = 0_{P}$
60	53 59	eqtrd	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \to X \cdot_{P} (i \underset{˙}{1} j) = 0_{P}$
61	60	adantr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to X \cdot_{P} (i \underset{˙}{1} j) = 0_{P}$
62		simpll	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \to (N \in Fin \land R \in Ring \land M \in B)$
63	62 24	jca	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \to ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N))$
64	63	ad2antrr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N))$
65	14 3 5 2 4	mat2pmatvalel	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (i \in N \land j \in N)) \to i T (M) j = S (i M j)$
66	64 65	syl	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to i T (M) j = S (i M j)$
67	61 66	oveq12d	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to (X \cdot_{P} (i \underset{˙}{1} j)) \underset{˙}{-} (i T (M) j) = 0_{P} \underset{˙}{-} S (i M j)$
68		fveq2	$⊢ i M j = \underset{˙}{0} \to S (i M j) = S (\underset{˙}{0})$
69	68	adantl	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to S (i M j) = S (\underset{˙}{0})$
70	2 4 7 46	ply1scl0	$⊢ R \in Ring \to S (\underset{˙}{0}) = 0_{P}$
71	70	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to S (\underset{˙}{0}) = 0_{P}$
72	71	ad4antr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to S (\underset{˙}{0}) = 0_{P}$
73	69 72	eqtrd	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to S (i M j) = 0_{P}$
74	73	oveq2d	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to 0_{P} \underset{˙}{-} S (i M j) = 0_{P} \underset{˙}{-} 0_{P}$
75		ringgrp	$⊢ P \in Ring \to P \in Grp$
76	15 75	syl	$⊢ R \in Ring \to P \in Grp$
77	30 46	grpidcl	$⊢ P \in Grp \to 0_{P} \in {Base}_{P}$
78	76 77	jccir	$⊢ R \in Ring \to (P \in Grp \land 0_{P} \in {Base}_{P})$
79	78	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (P \in Grp \land 0_{P} \in {Base}_{P})$
80	30 46 9	grpsubid	$⊢ (P \in Grp \land 0_{P} \in {Base}_{P}) \to 0_{P} \underset{˙}{-} 0_{P} = 0_{P}$
81	79 80	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to 0_{P} \underset{˙}{-} 0_{P} = 0_{P}$
82	81	ad4antr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to 0_{P} \underset{˙}{-} 0_{P} = 0_{P}$
83	67 74 82	3eqtrd	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to (X \cdot_{P} (i \underset{˙}{1} j)) \underset{˙}{-} (i T (M) j) = 0_{P}$
84	28 44 83	3eqtrd	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to i ((X \underset{˙}{\cdot} \underset{˙}{1}) Z T (M)) j = 0_{P}$

Metamath Proof Explorer

Theorem chpdmatlem2

Proof