Metamath Proof Explorer

Theorem chpdmatlem3

Description: Lemma 3 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 chpdmatlem3 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 ( ( 𝑋 · 1 ) 𝑍 ( 𝑇 ‘ 𝑀 ) ) 𝐾 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝐾 𝑀 𝐾 ) ) ) )

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 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → 𝑃 ∈ 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 14 3 5 2 10 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑄 ) )
21 19 20 jca ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑄 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑄 ) ) )
22 21 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑄 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑄 ) ) )
23 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → 𝐾 ∈ 𝑁 )
24 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
25 10 24 13 9 matsubgcell ⊢ ( ( 𝑃 ∈ Ring ∧ ( ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑄 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) → ( 𝐾 ( ( 𝑋 · 1 ) 𝑍 ( 𝑇 ‘ 𝑀 ) ) 𝐾 ) = ( ( 𝐾 ( 𝑋 · 1 ) 𝐾 ) − ( 𝐾 ( 𝑇 ‘ 𝑀 ) 𝐾 ) ) )
26 17 22 23 23 25 syl112anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 ( ( 𝑋 · 1 ) 𝑍 ( 𝑇 ‘ 𝑀 ) ) 𝐾 ) = ( ( 𝐾 ( 𝑋 · 1 ) 𝐾 ) − ( 𝐾 ( 𝑇 ‘ 𝑀 ) 𝐾 ) ) )
27 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
28 6 2 27 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
29 28 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
30 2 10 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )
31 24 11 ringidcl ⊢ ( 𝑄 ∈ Ring → 1 ∈ ( Base ‘ 𝑄 ) )
32 30 31 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 1 ∈ ( Base ‘ 𝑄 ) )
33 29 32 jca ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 1 ∈ ( Base ‘ 𝑄 ) ) )
34 33 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 1 ∈ ( Base ‘ 𝑄 ) ) )
35 34 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 1 ∈ ( Base ‘ 𝑄 ) ) )
36 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
37 10 24 27 12 36 matvscacell ⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 1 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑋 · 1 ) 𝐾 ) = ( 𝑋 ( .r ‘ 𝑃 ) ( 𝐾 1 𝐾 ) ) )
38 17 35 23 23 37 syl112anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 ( 𝑋 · 1 ) 𝐾 ) = ( 𝑋 ( .r ‘ 𝑃 ) ( 𝐾 1 𝐾 ) ) )
39 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
40 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
41 simpl1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → 𝑁 ∈ Fin )
42 10 39 40 41 17 23 23 11 mat1ov ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 1 𝐾 ) = if ( 𝐾 = 𝐾 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) )
43 eqid ⊢ 𝐾 = 𝐾
44 43 iftruei ⊢ if ( 𝐾 = 𝐾 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) = ( 1r ‘ 𝑃 )
45 42 44 eqtrdi ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 1 𝐾 ) = ( 1r ‘ 𝑃 ) )
46 45 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 𝐾 1 𝐾 ) ) = ( 𝑋 ( .r ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
47 15 28 jca ⊢ ( 𝑅 ∈ Ring → ( 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) )
48 47 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) )
49 27 36 39 ringridm ⊢ ( ( 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) = 𝑋 )
50 48 49 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) = 𝑋 )
51 50 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) = 𝑋 )
52 38 46 51 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 ( 𝑋 · 1 ) 𝐾 ) = 𝑋 )
53 14 3 5 2 4 mat2pmatvalel ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑇 ‘ 𝑀 ) 𝐾 ) = ( 𝑆 ‘ ( 𝐾 𝑀 𝐾 ) ) )
54 53 anabsan2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 ( 𝑇 ‘ 𝑀 ) 𝐾 ) = ( 𝑆 ‘ ( 𝐾 𝑀 𝐾 ) ) )
55 52 54 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( ( 𝐾 ( 𝑋 · 1 ) 𝐾 ) − ( 𝐾 ( 𝑇 ‘ 𝑀 ) 𝐾 ) ) = ( 𝑋 − ( 𝑆 ‘ ( 𝐾 𝑀 𝐾 ) ) ) )
56 26 55 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 ( ( 𝑋 · 1 ) 𝑍 ( 𝑇 ‘ 𝑀 ) ) 𝐾 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝐾 𝑀 𝐾 ) ) ) )