Metamath Proof Explorer

Theorem chpmat1dlem

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

Ref Expression
Hypotheses chpmat1d.c 
|- C = ( N CharPlyMat R )
chpmat1d.p 
|- P = ( Poly1 ` R )
chpmat1d.a 
|- A = ( N Mat R )
chpmat1d.b 
|- B = ( Base ` A )
chpmat1d.x 
|- X = ( var1 ` R )
chpmat1d.z 
|- .- = ( -g ` P )
chpmat1d.s 
|- S = ( algSc ` P )
chpmat1dlem.g 
|- G = ( N Mat P )
chpmat1dlem.x 
|- T = ( N matToPolyMat R )
Assertion chpmat1dlem 
|- ( ( R e. Ring /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( I ( ( X ( .s ` G ) ( 1r ` G ) ) ( -g ` G ) ( T ` M ) ) I ) = ( X .- ( S ` ( I M I ) ) ) )

Proof

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