chpdmatlem3

	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	chpdmatlem3	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to K ((X \underset{˙}{\cdot} \underset{˙}{1}) Z T (M)) K = X \underset{˙}{-} S (K M K)$

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	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \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	14 3 5 2 10	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Q}$
21	19 20	jca	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Q} \land T (M) \in {Base}_{Q})$
22	21	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to (X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Q} \land T (M) \in {Base}_{Q})$
23		simpr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to K \in N$
24		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
25	10 24 13 9	matsubgcell	$⊢ (P \in Ring \land (X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Q} \land T (M) \in {Base}_{Q}) \land (K \in N \land K \in N)) \to K ((X \underset{˙}{\cdot} \underset{˙}{1}) Z T (M)) K = (K (X \underset{˙}{\cdot} \underset{˙}{1}) K) \underset{˙}{-} (K T (M) K)$
26	17 22 23 23 25	syl112anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to K ((X \underset{˙}{\cdot} \underset{˙}{1}) Z T (M)) K = (K (X \underset{˙}{\cdot} \underset{˙}{1}) K) \underset{˙}{-} (K T (M) K)$
27		eqid	$⊢ {Base}_{P} = {Base}_{P}$
28	6 2 27	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
29	28	adantl	$⊢ (N \in Fin \land R \in Ring) \to X \in {Base}_{P}$
30	2 10	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Q \in Ring$
31	24 11	ringidcl	$⊢ Q \in Ring \to \underset{˙}{1} \in {Base}_{Q}$
32	30 31	syl	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{1} \in {Base}_{Q}$
33	29 32	jca	$⊢ (N \in Fin \land R \in Ring) \to (X \in {Base}_{P} \land \underset{˙}{1} \in {Base}_{Q})$
34	33	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (X \in {Base}_{P} \land \underset{˙}{1} \in {Base}_{Q})$
35	34	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to (X \in {Base}_{P} \land \underset{˙}{1} \in {Base}_{Q})$
36		eqid	$⊢ \cdot_{P} = \cdot_{P}$
37	10 24 27 12 36	matvscacell	$⊢ (P \in Ring \land (X \in {Base}_{P} \land \underset{˙}{1} \in {Base}_{Q}) \land (K \in N \land K \in N)) \to K (X \underset{˙}{\cdot} \underset{˙}{1}) K = X \cdot_{P} (K \underset{˙}{1} K)$
38	17 35 23 23 37	syl112anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to K (X \underset{˙}{\cdot} \underset{˙}{1}) K = X \cdot_{P} (K \underset{˙}{1} K)$
39		eqid	$⊢ 1_{P} = 1_{P}$
40		eqid	$⊢ 0_{P} = 0_{P}$
41		simpl1	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to N \in Fin$
42	10 39 40 41 17 23 23 11	mat1ov	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to K \underset{˙}{1} K = if (K = K, 1_{P}, 0_{P})$
43		eqid	$⊢ K = K$
44	43	iftruei	$⊢ if (K = K, 1_{P}, 0_{P}) = 1_{P}$
45	42 44	eqtrdi	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to K \underset{˙}{1} K = 1_{P}$
46	45	oveq2d	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to X \cdot_{P} (K \underset{˙}{1} K) = X \cdot_{P} 1_{P}$
47	15 28	jca	$⊢ R \in Ring \to (P \in Ring \land X \in {Base}_{P})$
48	47	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (P \in Ring \land X \in {Base}_{P})$
49	27 36 39	ringridm	$⊢ (P \in Ring \land X \in {Base}_{P}) \to X \cdot_{P} 1_{P} = X$
50	48 49	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to X \cdot_{P} 1_{P} = X$
51	50	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to X \cdot_{P} 1_{P} = X$
52	38 46 51	3eqtrd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to K (X \underset{˙}{\cdot} \underset{˙}{1}) K = X$
53	14 3 5 2 4	mat2pmatvalel	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (K \in N \land K \in N)) \to K T (M) K = S (K M K)$
54	53	anabsan2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to K T (M) K = S (K M K)$
55	52 54	oveq12d	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to (K (X \underset{˙}{\cdot} \underset{˙}{1}) K) \underset{˙}{-} (K T (M) K) = X \underset{˙}{-} S (K M K)$
56	26 55	eqtrd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land K \in N) \to K ((X \underset{˙}{\cdot} \underset{˙}{1}) Z T (M)) K = X \underset{˙}{-} S (K M K)$

Metamath Proof Explorer

Theorem chpdmatlem3

Proof