Theorem chpdmatlem2

Description: Lemma 2 for chpdmat . (Contributed by AV, 18-Aug-2019)

	Ref	Expression
Hypotheses	chpdmat.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	chpdmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	chpdmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	chpdmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
	chpdmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	chpdmat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	chpdmat.0	⊢ 0 = ( 0g ‘ 𝑅 )
	chpdmat.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
	chpdmat.m	⊢ − = ( -g ‘ 𝑃 )
	chpdmatlem.q	⊢ 𝑄 = ( 𝑁 Mat 𝑃 )
	chpdmatlem.1	⊢ 1 = ( 1r ‘ 𝑄 )
	chpdmatlem.m	⊢ · = ( ·𝑠 ‘ 𝑄 )
	chpdmatlem.z	⊢ 𝑍 = ( -g ‘ 𝑄 )
	chpdmatlem.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion	chpdmatlem2	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑖 ( ( 𝑋 · 1 ) 𝑍 ( 𝑇 ‘ 𝑀 ) ) 𝑗 ) = ( 0g ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		chpdmat.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2		chpdmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		chpdmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		chpdmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
5		chpdmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
6		chpdmat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
7		chpdmat.0	⊢ 0 = ( 0g ‘ 𝑅 )
8		chpdmat.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
9		chpdmat.m	⊢ − = ( -g ‘ 𝑃 )
10		chpdmatlem.q	⊢ 𝑄 = ( 𝑁 Mat 𝑃 )
11		chpdmatlem.1	⊢ 1 = ( 1r ‘ 𝑄 )
12		chpdmatlem.m	⊢ · = ( ·𝑠 ‘ 𝑄 )
13		chpdmatlem.z	⊢ 𝑍 = ( -g ‘ 𝑄 )
14		chpdmatlem.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
15	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
16	15	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
17	16	ad4antr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → 𝑃 ∈ Ring )
18	1 2 3 4 5 6 7 8 9 10 11 12	chpdmatlem0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑄 ) )
19	18	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑄 ) )
20	19	ad4antr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑄 ) )
21	14 3 5 2 10	mat2pmatbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑄 ) )
22	21	ad4antr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑄 ) )
23		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
24	23	anim1i	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
25	24	ad2antrr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
26		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
27	10 26 13 9	matsubgcell	⊢ ( ( 𝑃 ∈ Ring ∧ ( ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑄 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( 𝑋 · 1 ) 𝑍 ( 𝑇 ‘ 𝑀 ) ) 𝑗 ) = ( ( 𝑖 ( 𝑋 · 1 ) 𝑗 ) − ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) )
28	17 20 22 25 27	syl121anc	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑖 ( ( 𝑋 · 1 ) 𝑍 ( 𝑇 ‘ 𝑀 ) ) 𝑗 ) = ( ( 𝑖 ( 𝑋 · 1 ) 𝑗 ) − ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) )
29	16	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ Ring )
30		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
31	6 2 30	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
32	31	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
33	2 10	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )
34	33	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑄 ∈ Ring )
35	26 11	ringidcl	⊢ ( 𝑄 ∈ Ring → 1 ∈ ( Base ‘ 𝑄 ) )
36	34 35	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 1 ∈ ( Base ‘ 𝑄 ) )
37	32 36	jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 1 ∈ ( Base ‘ 𝑄 ) ) )
38	37	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 1 ∈ ( Base ‘ 𝑄 ) ) )
39	29 38 24	3jca	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑃 ∈ Ring ∧ ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 1 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) )
40	39	ad2antrr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑃 ∈ Ring ∧ ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 1 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) )
41		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
42	10 26 30 12 41	matvscacell	⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 1 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑋 · 1 ) 𝑗 ) = ( 𝑋 ( .r ‘ 𝑃 ) ( 𝑖 1 𝑗 ) ) )
43	40 42	syl	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑖 ( 𝑋 · 1 ) 𝑗 ) = ( 𝑋 ( .r ‘ 𝑃 ) ( 𝑖 1 𝑗 ) ) )
44	43	oveq1d	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( ( 𝑖 ( 𝑋 · 1 ) 𝑗 ) − ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) = ( ( 𝑋 ( .r ‘ 𝑃 ) ( 𝑖 1 𝑗 ) ) − ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) )
45		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
46		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
47		simpll1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑁 ∈ Fin )
48	23	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
49		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
50	10 45 46 47 29 48 49 11	mat1ov	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 1 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) )
51		ifnefalse	⊢ ( 𝑖 ≠ 𝑗 → if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) = ( 0g ‘ 𝑃 ) )
52	50 51	sylan9eq	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝑖 1 𝑗 ) = ( 0g ‘ 𝑃 ) )
53	52	oveq2d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 𝑖 1 𝑗 ) ) = ( 𝑋 ( .r ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) )
54	15 31	jca	⊢ ( 𝑅 ∈ Ring → ( 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) )
55	54	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) )
56	30 41 46	ringrz	⊢ ( ( 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) = ( 0g ‘ 𝑃 ) )
57	55 56	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) = ( 0g ‘ 𝑃 ) )
58	57	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) = ( 0g ‘ 𝑃 ) )
59	58	ad2antrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) = ( 0g ‘ 𝑃 ) )
60	53 59	eqtrd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 𝑖 1 𝑗 ) ) = ( 0g ‘ 𝑃 ) )
61	60	adantr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 𝑖 1 𝑗 ) ) = ( 0g ‘ 𝑃 ) )
62		simpll	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) )
63	62 24	jca	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) )
64	63	ad2antrr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) )
65	14 3 5 2 4	mat2pmatvalel	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) )
66	64 65	syl	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) )
67	61 66	oveq12d	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( ( 𝑋 ( .r ‘ 𝑃 ) ( 𝑖 1 𝑗 ) ) − ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) = ( ( 0g ‘ 𝑃 ) − ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) )
68		fveq2	⊢ ( ( 𝑖 𝑀 𝑗 ) = 0 → ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) = ( 𝑆 ‘ 0 ) )
69	68	adantl	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) = ( 𝑆 ‘ 0 ) )
70	2 4 7 46	ply1scl0	⊢ ( 𝑅 ∈ Ring → ( 𝑆 ‘ 0 ) = ( 0g ‘ 𝑃 ) )
71	70	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑆 ‘ 0 ) = ( 0g ‘ 𝑃 ) )
72	71	ad4antr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑆 ‘ 0 ) = ( 0g ‘ 𝑃 ) )
73	69 72	eqtrd	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) = ( 0g ‘ 𝑃 ) )
74	73	oveq2d	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( ( 0g ‘ 𝑃 ) − ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = ( ( 0g ‘ 𝑃 ) − ( 0g ‘ 𝑃 ) ) )
75		ringgrp	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
76	15 75	syl	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Grp )
77	30 46	grpidcl	⊢ ( 𝑃 ∈ Grp → ( 0g ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
78	76 77	jccir	⊢ ( 𝑅 ∈ Ring → ( 𝑃 ∈ Grp ∧ ( 0g ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) ) )
79	78	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑃 ∈ Grp ∧ ( 0g ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) ) )
80	30 46 9	grpsubid	⊢ ( ( 𝑃 ∈ Grp ∧ ( 0g ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 0g ‘ 𝑃 ) − ( 0g ‘ 𝑃 ) ) = ( 0g ‘ 𝑃 ) )
81	79 80	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 0g ‘ 𝑃 ) − ( 0g ‘ 𝑃 ) ) = ( 0g ‘ 𝑃 ) )
82	81	ad4antr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( ( 0g ‘ 𝑃 ) − ( 0g ‘ 𝑃 ) ) = ( 0g ‘ 𝑃 ) )
83	67 74 82	3eqtrd	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( ( 𝑋 ( .r ‘ 𝑃 ) ( 𝑖 1 𝑗 ) ) − ( 𝑖 ( 𝑇 ‘ 𝑀 ) 𝑗 ) ) = ( 0g ‘ 𝑃 ) )
84	28 44 83	3eqtrd	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝑖 ( ( 𝑋 · 1 ) 𝑍 ( 𝑇 ‘ 𝑀 ) ) 𝑗 ) = ( 0g ‘ 𝑃 ) )