Metamath Proof Explorer

Theorem chpdmatlem2

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

Ref Expression
Hypotheses chpdmat.c 
|- C = ( N CharPlyMat R )
chpdmat.p 
|- P = ( Poly1 ` R )
chpdmat.a 
|- A = ( N Mat R )
chpdmat.s 
|- S = ( algSc ` P )
chpdmat.b 
|- B = ( Base ` A )
chpdmat.x 
|- X = ( var1 ` R )
chpdmat.0 
|- .0. = ( 0g ` R )
chpdmat.g 
|- G = ( mulGrp ` P )
chpdmat.m 
|- .- = ( -g ` P )
chpdmatlem.q 
|- Q = ( N Mat P )
chpdmatlem.1 
|- .1. = ( 1r ` Q )
chpdmatlem.m 
|- .x. = ( .s ` Q )
chpdmatlem.z 
|- Z = ( -g ` Q )
chpdmatlem.t 
|- T = ( N matToPolyMat R )
Assertion chpdmatlem2 
|- ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( i ( ( X .x. .1. ) Z ( T ` M ) ) j ) = ( 0g ` P ) )

Proof

Step Hyp Ref Expression
1 chpdmat.c 
 |-  C = ( N CharPlyMat R )
2 chpdmat.p 
 |-  P = ( Poly1 ` R )
3 chpdmat.a 
 |-  A = ( N Mat R )
4 chpdmat.s 
 |-  S = ( algSc ` P )
5 chpdmat.b 
 |-  B = ( Base ` A )
6 chpdmat.x 
 |-  X = ( var1 ` R )
7 chpdmat.0 
 |-  .0. = ( 0g ` R )
8 chpdmat.g 
 |-  G = ( mulGrp ` P )
9 chpdmat.m 
 |-  .- = ( -g ` P )
10 chpdmatlem.q 
 |-  Q = ( N Mat P )
11 chpdmatlem.1 
 |-  .1. = ( 1r ` Q )
12 chpdmatlem.m 
 |-  .x. = ( .s ` Q )
13 chpdmatlem.z 
 |-  Z = ( -g ` Q )
14 chpdmatlem.t 
 |-  T = ( N matToPolyMat R )
15 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
16 15 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> P e. Ring )
17 16 ad4antr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> P e. Ring )
18 1 2 3 4 5 6 7 8 9 10 11 12 chpdmatlem0 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X .x. .1. ) e. ( Base ` Q ) )
19 18 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( X .x. .1. ) e. ( Base ` Q ) )
20 19 ad4antr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( X .x. .1. ) e. ( Base ` Q ) )
21 14 3 5 2 10 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Q ) )
22 21 ad4antr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( T ` M ) e. ( Base ` Q ) )
23 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) -> i e. N )
24 23 anim1i 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) -> ( i e. N /\ j e. N ) )
25 24 ad2antrr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( i e. N /\ j e. N ) )
26 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
27 10 26 13 9 matsubgcell 
 |-  ( ( P e. Ring /\ ( ( X .x. .1. ) e. ( Base ` Q ) /\ ( T ` M ) e. ( Base ` Q ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( ( X .x. .1. ) Z ( T ` M ) ) j ) = ( ( i ( X .x. .1. ) j ) .- ( i ( T ` M ) j ) ) )
28 17 20 22 25 27 syl121anc 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( i ( ( X .x. .1. ) Z ( T ` M ) ) j ) = ( ( i ( X .x. .1. ) j ) .- ( i ( T ` M ) j ) ) )
29 16 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) -> P e. Ring )
30 eqid 
 |-  ( Base ` P ) = ( Base ` P )
31 6 2 30 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
32 31 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> X e. ( Base ` P ) )
33 2 10 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. Ring )
34 33 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Q e. Ring )
35 26 11 ringidcl 
 |-  ( Q e. Ring -> .1. e. ( Base ` Q ) )
36 34 35 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> .1. e. ( Base ` Q ) )
37 32 36 jca 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( X e. ( Base ` P ) /\ .1. e. ( Base ` Q ) ) )
38 37 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) -> ( X e. ( Base ` P ) /\ .1. e. ( Base ` Q ) ) )
39 29 38 24 3jca 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) -> ( P e. Ring /\ ( X e. ( Base ` P ) /\ .1. e. ( Base ` Q ) ) /\ ( i e. N /\ j e. N ) ) )
40 39 ad2antrr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( P e. Ring /\ ( X e. ( Base ` P ) /\ .1. e. ( Base ` Q ) ) /\ ( i e. N /\ j e. N ) ) )
41 eqid 
 |-  ( .r ` P ) = ( .r ` P )
42 10 26 30 12 41 matvscacell 
 |-  ( ( P e. Ring /\ ( X e. ( Base ` P ) /\ .1. e. ( Base ` Q ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( X .x. .1. ) j ) = ( X ( .r ` P ) ( i .1. j ) ) )
43 40 42 syl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( i ( X .x. .1. ) j ) = ( X ( .r ` P ) ( i .1. j ) ) )
44 43 oveq1d 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( ( i ( X .x. .1. ) j ) .- ( i ( T ` M ) j ) ) = ( ( X ( .r ` P ) ( i .1. j ) ) .- ( i ( T ` M ) j ) ) )
45 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
46 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
47 simpll1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) -> N e. Fin )
48 23 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) -> i e. N )
49 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) -> j e. N )
50 10 45 46 47 29 48 49 11 mat1ov 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) -> ( i .1. j ) = if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) )
51 ifnefalse 
 |-  ( i =/= j -> if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) = ( 0g ` P ) )
52 50 51 sylan9eq 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) -> ( i .1. j ) = ( 0g ` P ) )
53 52 oveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) -> ( X ( .r ` P ) ( i .1. j ) ) = ( X ( .r ` P ) ( 0g ` P ) ) )
54 15 31 jca 
 |-  ( R e. Ring -> ( P e. Ring /\ X e. ( Base ` P ) ) )
55 54 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( P e. Ring /\ X e. ( Base ` P ) ) )
56 30 41 46 ringrz 
 |-  ( ( P e. Ring /\ X e. ( Base ` P ) ) -> ( X ( .r ` P ) ( 0g ` P ) ) = ( 0g ` P ) )
57 55 56 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( X ( .r ` P ) ( 0g ` P ) ) = ( 0g ` P ) )
58 57 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) -> ( X ( .r ` P ) ( 0g ` P ) ) = ( 0g ` P ) )
59 58 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) -> ( X ( .r ` P ) ( 0g ` P ) ) = ( 0g ` P ) )
60 53 59 eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) -> ( X ( .r ` P ) ( i .1. j ) ) = ( 0g ` P ) )
61 60 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( X ( .r ` P ) ( i .1. j ) ) = ( 0g ` P ) )
62 simpll 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) -> ( N e. Fin /\ R e. Ring /\ M e. B ) )
63 62 24 jca 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) -> ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) )
64 63 ad2antrr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) )
65 14 3 5 2 4 mat2pmatvalel 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` M ) j ) = ( S ` ( i M j ) ) )
66 64 65 syl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( i ( T ` M ) j ) = ( S ` ( i M j ) ) )
67 61 66 oveq12d 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( ( X ( .r ` P ) ( i .1. j ) ) .- ( i ( T ` M ) j ) ) = ( ( 0g ` P ) .- ( S ` ( i M j ) ) ) )
68 fveq2 
 |-  ( ( i M j ) = .0. -> ( S ` ( i M j ) ) = ( S ` .0. ) )
69 68 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( S ` ( i M j ) ) = ( S ` .0. ) )
70 2 4 7 46 ply1scl0 
 |-  ( R e. Ring -> ( S ` .0. ) = ( 0g ` P ) )
71 70 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( S ` .0. ) = ( 0g ` P ) )
72 71 ad4antr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( S ` .0. ) = ( 0g ` P ) )
73 69 72 eqtrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( S ` ( i M j ) ) = ( 0g ` P ) )
74 73 oveq2d 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( ( 0g ` P ) .- ( S ` ( i M j ) ) ) = ( ( 0g ` P ) .- ( 0g ` P ) ) )
75 ringgrp 
 |-  ( P e. Ring -> P e. Grp )
76 15 75 syl 
 |-  ( R e. Ring -> P e. Grp )
77 30 46 grpidcl 
 |-  ( P e. Grp -> ( 0g ` P ) e. ( Base ` P ) )
78 76 77 jccir 
 |-  ( R e. Ring -> ( P e. Grp /\ ( 0g ` P ) e. ( Base ` P ) ) )
79 78 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( P e. Grp /\ ( 0g ` P ) e. ( Base ` P ) ) )
80 30 46 9 grpsubid 
 |-  ( ( P e. Grp /\ ( 0g ` P ) e. ( Base ` P ) ) -> ( ( 0g ` P ) .- ( 0g ` P ) ) = ( 0g ` P ) )
81 79 80 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( 0g ` P ) .- ( 0g ` P ) ) = ( 0g ` P ) )
82 81 ad4antr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( ( 0g ` P ) .- ( 0g ` P ) ) = ( 0g ` P ) )
83 67 74 82 3eqtrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( ( X ( .r ` P ) ( i .1. j ) ) .- ( i ( T ` M ) j ) ) = ( 0g ` P ) )
84 28 44 83 3eqtrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = .0. ) -> ( i ( ( X .x. .1. ) Z ( T ` M ) ) j ) = ( 0g ` P ) )