Metamath Proof Explorer

Theorem chpmat1dlem

Description: Lemma for chpmat1d . (Contributed by AV, 7-Aug-2019)

Ref Expression
Hypotheses chpmat1d.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
chpmat1d.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
chpmat1d.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
chpmat1d.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
chpmat1d.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
chpmat1d.z ⊢ − = ( -g ‘ 𝑃 )
chpmat1d.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
chpmat1dlem.g ⊢ 𝐺 = ( 𝑁 Mat 𝑃 )
chpmat1dlem.x ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion chpmat1dlem ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ( ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) ( -g ‘ 𝐺 ) ( 𝑇 ‘ 𝑀 ) ) 𝐼 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ) )

Proof

Step Hyp Ref Expression
1 chpmat1d.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2 chpmat1d.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 chpmat1d.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4 chpmat1d.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
5 chpmat1d.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
6 chpmat1d.z ⊢ − = ( -g ‘ 𝑃 )
7 chpmat1d.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
8 chpmat1dlem.g ⊢ 𝐺 = ( 𝑁 Mat 𝑃 )
9 chpmat1dlem.x ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
10 2 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
11 10 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
12 snfi ⊢ { 𝐼 } ∈ Fin
13 eleq1 ⊢ ( 𝑁 = { 𝐼 } → ( 𝑁 ∈ Fin ↔ { 𝐼 } ∈ Fin ) )
14 12 13 mpbiri ⊢ ( 𝑁 = { 𝐼 } → 𝑁 ∈ Fin )
15 14 adantr ⊢ ( ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) → 𝑁 ∈ Fin )
16 10 15 anim12i ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ) → ( 𝑃 ∈ Ring ∧ 𝑁 ∈ Fin ) )
17 16 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑃 ∈ Ring ∧ 𝑁 ∈ Fin ) )
18 17 ancomd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
19 8 matlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝐺 ∈ LMod )
20 18 19 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝐺 ∈ LMod )
21 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
22 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
23 5 21 22 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
24 23 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
25 15 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
26 fvex ⊢ ( Poly1 ‘ 𝑅 ) ∈ V
27 2 oveq2i ⊢ ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) )
28 8 27 eqtri ⊢ 𝐺 = ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) )
29 28 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ ( Poly1 ‘ 𝑅 ) ∈ V ) → ( Poly1 ‘ 𝑅 ) = ( Scalar ‘ 𝐺 ) )
30 25 26 29 sylancl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( Poly1 ‘ 𝑅 ) = ( Scalar ‘ 𝐺 ) )
31 30 eqcomd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝐺 ) = ( Poly1 ‘ 𝑅 ) )
32 31 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( Scalar ‘ 𝐺 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
33 24 32 eleqtrrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) )
34 8 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝐺 ∈ Ring )
35 18 34 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝐺 ∈ Ring )
36 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
37 eqid ⊢ ( 1r ‘ 𝐺 ) = ( 1r ‘ 𝐺 )
38 36 37 ringidcl ⊢ ( 𝐺 ∈ Ring → ( 1r ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
39 35 38 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 1r ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
40 20 33 39 3jca ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐺 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ ( 1r ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) ) )
41 eqid ⊢ ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝐺 )
42 eqid ⊢ ( ·𝑠 ‘ 𝐺 ) = ( ·𝑠 ‘ 𝐺 )
43 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐺 ) ) = ( Base ‘ ( Scalar ‘ 𝐺 ) )
44 36 41 42 43 lmodvscl ⊢ ( ( 𝐺 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ ( 1r ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐺 ) )
45 40 44 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐺 ) )
46 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
47 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
48 25 46 47 3jca ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) )
49 9 3 4 2 8 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝐺 ) )
50 48 49 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝐺 ) )
51 snidg ⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ { 𝐼 } )
52 51 adantl ⊢ ( ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) → 𝐼 ∈ { 𝐼 } )
53 eleq2 ⊢ ( 𝑁 = { 𝐼 } → ( 𝐼 ∈ 𝑁 ↔ 𝐼 ∈ { 𝐼 } ) )
54 53 adantr ⊢ ( ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 ∈ 𝑁 ↔ 𝐼 ∈ { 𝐼 } ) )
55 52 54 mpbird ⊢ ( ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) → 𝐼 ∈ 𝑁 )
56 id ⊢ ( 𝐼 ∈ 𝑁 → 𝐼 ∈ 𝑁 )
57 55 56 jccir ⊢ ( ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ) )
58 57 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ) )
59 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
60 8 36 59 6 matsubgcell ⊢ ( ( 𝑃 ∈ Ring ∧ ( ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ) ) → ( 𝐼 ( ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) ( -g ‘ 𝐺 ) ( 𝑇 ‘ 𝑀 ) ) 𝐼 ) = ( ( 𝐼 ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) 𝐼 ) − ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐼 ) ) )
61 11 45 50 58 60 syl121anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ( ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) ( -g ‘ 𝐺 ) ( 𝑇 ‘ 𝑀 ) ) 𝐼 ) = ( ( 𝐼 ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) 𝐼 ) − ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐼 ) ) )
62 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
63 5 2 62 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
64 63 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
65 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
66 8 36 62 42 65 matvscacell ⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 1r ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) 𝐼 ) = ( 𝑋 ( .r ‘ 𝑃 ) ( 𝐼 ( 1r ‘ 𝐺 ) 𝐼 ) ) )
67 11 64 39 58 66 syl121anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) 𝐼 ) = ( 𝑋 ( .r ‘ 𝑃 ) ( 𝐼 ( 1r ‘ 𝐺 ) 𝐼 ) ) )
68 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
69 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
70 55 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝐼 ∈ 𝑁 )
71 8 68 69 25 11 70 70 37 mat1ov ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ( 1r ‘ 𝐺 ) 𝐼 ) = if ( 𝐼 = 𝐼 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) )
72 eqidd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝐼 = 𝐼 )
73 72 iftrued ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → if ( 𝐼 = 𝐼 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) = ( 1r ‘ 𝑃 ) )
74 71 73 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ( 1r ‘ 𝐺 ) 𝐼 ) = ( 1r ‘ 𝑃 ) )
75 74 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 𝐼 ( 1r ‘ 𝐺 ) 𝐼 ) ) = ( 𝑋 ( .r ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
76 62 65 68 ringridm ⊢ ( ( 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) = 𝑋 )
77 11 64 76 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 ( .r ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) = 𝑋 )
78 67 75 77 3eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) 𝐼 ) = 𝑋 )
79 9 3 4 2 7 mat2pmatvalel ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐼 ) = ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) )
80 48 58 79 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐼 ) = ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) )
81 78 80 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝐼 ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) 𝐼 ) − ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐼 ) ) = ( 𝑋 − ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ) )
82 61 81 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ( ( 𝑋 ( ·𝑠 ‘ 𝐺 ) ( 1r ‘ 𝐺 ) ) ( -g ‘ 𝐺 ) ( 𝑇 ‘ 𝑀 ) ) 𝐼 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ) )