chpmat1dlem

	Ref	Expression
Hypotheses	chpmat1d.c	$⊢ C = N CharPlyMat R$
	chpmat1d.p	$⊢ P = {Poly}_{1} (R)$
	chpmat1d.a	$⊢ A = N Mat R$
	chpmat1d.b	$⊢ B = {Base}_{A}$
	chpmat1d.x	$⊢ X = {var}_{1} (R)$
	chpmat1d.z	$⊢ \underset{˙}{-} = -_{P}$
	chpmat1d.s	$⊢ S = algSc (P)$
	chpmat1dlem.g	$⊢ G = N Mat P$
	chpmat1dlem.x	$⊢ T = N matToPolyMat R$
Assertion	chpmat1dlem	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to I ((X \cdot_{G} 1_{G}) -_{G} T (M)) I = X \underset{˙}{-} S (I M I)$

Proof

Step	Hyp	Ref	Expression
1		chpmat1d.c	$⊢ C = N CharPlyMat R$
2		chpmat1d.p	$⊢ P = {Poly}_{1} (R)$
3		chpmat1d.a	$⊢ A = N Mat R$
4		chpmat1d.b	$⊢ B = {Base}_{A}$
5		chpmat1d.x	$⊢ X = {var}_{1} (R)$
6		chpmat1d.z	$⊢ \underset{˙}{-} = -_{P}$
7		chpmat1d.s	$⊢ S = algSc (P)$
8		chpmat1dlem.g	$⊢ G = N Mat P$
9		chpmat1dlem.x	$⊢ T = N matToPolyMat R$
10	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
11	10	3ad2ant1	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to P \in Ring$
12		snfi	$⊢ \{I\} \in Fin$
13		eleq1	$⊢ N = \{I\} \to (N \in Fin \leftrightarrow \{I\} \in Fin)$
14	12 13	mpbiri	$⊢ N = \{I\} \to N \in Fin$
15	14	adantr	$⊢ (N = \{I\} \land I \in V) \to N \in Fin$
16	10 15	anim12i	$⊢ (R \in Ring \land (N = \{I\} \land I \in V)) \to (P \in Ring \land N \in Fin)$
17	16	3adant3	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to (P \in Ring \land N \in Fin)$
18	17	ancomd	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to (N \in Fin \land P \in Ring)$
19	8	matlmod	$⊢ (N \in Fin \land P \in Ring) \to G \in LMod$
20	18 19	syl	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to G \in LMod$
21		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
22		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
23	5 21 22	vr1cl	$⊢ R \in Ring \to X \in {Base}_{{Poly}_{1} (R)}$
24	23	3ad2ant1	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to X \in {Base}_{{Poly}_{1} (R)}$
25	15	3ad2ant2	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to N \in Fin$
26		fvex	$⊢ {Poly}_{1} (R) \in V$
27	2	oveq2i	$⊢ N Mat P = N Mat {Poly}_{1} (R)$
28	8 27	eqtri	$⊢ G = N Mat {Poly}_{1} (R)$
29	28	matsca2	$⊢ (N \in Fin \land {Poly}_{1} (R) \in V) \to {Poly}_{1} (R) = Scalar (G)$
30	25 26 29	sylancl	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to {Poly}_{1} (R) = Scalar (G)$
31	30	eqcomd	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to Scalar (G) = {Poly}_{1} (R)$
32	31	fveq2d	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to {Base}_{Scalar (G)} = {Base}_{{Poly}_{1} (R)}$
33	24 32	eleqtrrd	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to X \in {Base}_{Scalar (G)}$
34	8	matring	$⊢ (N \in Fin \land P \in Ring) \to G \in Ring$
35	18 34	syl	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to G \in Ring$
36		eqid	$⊢ {Base}_{G} = {Base}_{G}$
37		eqid	$⊢ 1_{G} = 1_{G}$
38	36 37	ringidcl	$⊢ G \in Ring \to 1_{G} \in {Base}_{G}$
39	35 38	syl	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to 1_{G} \in {Base}_{G}$
40	20 33 39	3jca	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to (G \in LMod \land X \in {Base}_{Scalar (G)} \land 1_{G} \in {Base}_{G})$
41		eqid	$⊢ Scalar (G) = Scalar (G)$
42		eqid	$⊢ \cdot_{G} = \cdot_{G}$
43		eqid	$⊢ {Base}_{Scalar (G)} = {Base}_{Scalar (G)}$
44	36 41 42 43	lmodvscl	$⊢ (G \in LMod \land X \in {Base}_{Scalar (G)} \land 1_{G} \in {Base}_{G}) \to X \cdot_{G} 1_{G} \in {Base}_{G}$
45	40 44	syl	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to X \cdot_{G} 1_{G} \in {Base}_{G}$
46		simp1	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to R \in Ring$
47		simp3	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to M \in B$
48	25 46 47	3jca	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to (N \in Fin \land R \in Ring \land M \in B)$
49	9 3 4 2 8	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{G}$
50	48 49	syl	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to T (M) \in {Base}_{G}$
51		snidg	$⊢ I \in V \to I \in \{I\}$
52	51	adantl	$⊢ (N = \{I\} \land I \in V) \to I \in \{I\}$
53		eleq2	$⊢ N = \{I\} \to (I \in N \leftrightarrow I \in \{I\})$
54	53	adantr	$⊢ (N = \{I\} \land I \in V) \to (I \in N \leftrightarrow I \in \{I\})$
55	52 54	mpbird	$⊢ (N = \{I\} \land I \in V) \to I \in N$
56		id	$⊢ I \in N \to I \in N$
57	55 56	jccir	$⊢ (N = \{I\} \land I \in V) \to (I \in N \land I \in N)$
58	57	3ad2ant2	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to (I \in N \land I \in N)$
59		eqid	$⊢ -_{G} = -_{G}$
60	8 36 59 6	matsubgcell	$⊢ (P \in Ring \land (X \cdot_{G} 1_{G} \in {Base}_{G} \land T (M) \in {Base}_{G}) \land (I \in N \land I \in N)) \to I ((X \cdot_{G} 1_{G}) -_{G} T (M)) I = (I (X \cdot_{G} 1_{G}) I) \underset{˙}{-} (I T (M) I)$
61	11 45 50 58 60	syl121anc	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to I ((X \cdot_{G} 1_{G}) -_{G} T (M)) I = (I (X \cdot_{G} 1_{G}) I) \underset{˙}{-} (I T (M) I)$
62		eqid	$⊢ {Base}_{P} = {Base}_{P}$
63	5 2 62	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
64	63	3ad2ant1	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to X \in {Base}_{P}$
65		eqid	$⊢ \cdot_{P} = \cdot_{P}$
66	8 36 62 42 65	matvscacell	$⊢ (P \in Ring \land (X \in {Base}_{P} \land 1_{G} \in {Base}_{G}) \land (I \in N \land I \in N)) \to I (X \cdot_{G} 1_{G}) I = X \cdot_{P} (I 1_{G} I)$
67	11 64 39 58 66	syl121anc	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to I (X \cdot_{G} 1_{G}) I = X \cdot_{P} (I 1_{G} I)$
68		eqid	$⊢ 1_{P} = 1_{P}$
69		eqid	$⊢ 0_{P} = 0_{P}$
70	55	3ad2ant2	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to I \in N$
71	8 68 69 25 11 70 70 37	mat1ov	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to I 1_{G} I = if (I = I, 1_{P}, 0_{P})$
72		eqidd	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to I = I$
73	72	iftrued	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to if (I = I, 1_{P}, 0_{P}) = 1_{P}$
74	71 73	eqtrd	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to I 1_{G} I = 1_{P}$
75	74	oveq2d	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to X \cdot_{P} (I 1_{G} I) = X \cdot_{P} 1_{P}$
76	62 65 68	ringridm	$⊢ (P \in Ring \land X \in {Base}_{P}) \to X \cdot_{P} 1_{P} = X$
77	11 64 76	syl2anc	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to X \cdot_{P} 1_{P} = X$
78	67 75 77	3eqtrd	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to I (X \cdot_{G} 1_{G}) I = X$
79	9 3 4 2 7	mat2pmatvalel	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land I \in N)) \to I T (M) I = S (I M I)$
80	48 58 79	syl2anc	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to I T (M) I = S (I M I)$
81	78 80	oveq12d	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to (I (X \cdot_{G} 1_{G}) I) \underset{˙}{-} (I T (M) I) = X \underset{˙}{-} S (I M I)$
82	61 81	eqtrd	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to I ((X \cdot_{G} 1_{G}) -_{G} T (M)) I = X \underset{˙}{-} S (I M I)$

Metamath Proof Explorer

Theorem chpmat1dlem

Proof