Metamath Proof Explorer

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 ‘ 𝑃 ) )