Metamath Proof Explorer

Theorem chpdmatlem3

Description: Lemma 3 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 chpdmatlem3 
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( K ( ( X .x. .1. ) Z ( T ` M ) ) K ) = ( X .- ( S ` ( K M K ) ) ) )

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 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> 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 14 3 5 2 10 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Q ) )
21 19 20 jca 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( X .x. .1. ) e. ( Base ` Q ) /\ ( T ` M ) e. ( Base ` Q ) ) )
22 21 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( ( X .x. .1. ) e. ( Base ` Q ) /\ ( T ` M ) e. ( Base ` Q ) ) )
23 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> K e. N )
24 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
25 10 24 13 9 matsubgcell 
 |-  ( ( P e. Ring /\ ( ( X .x. .1. ) e. ( Base ` Q ) /\ ( T ` M ) e. ( Base ` Q ) ) /\ ( K e. N /\ K e. N ) ) -> ( K ( ( X .x. .1. ) Z ( T ` M ) ) K ) = ( ( K ( X .x. .1. ) K ) .- ( K ( T ` M ) K ) ) )
26 17 22 23 23 25 syl112anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( K ( ( X .x. .1. ) Z ( T ` M ) ) K ) = ( ( K ( X .x. .1. ) K ) .- ( K ( T ` M ) K ) ) )
27 eqid 
 |-  ( Base ` P ) = ( Base ` P )
28 6 2 27 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
29 28 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> X e. ( Base ` P ) )
30 2 10 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. Ring )
31 24 11 ringidcl 
 |-  ( Q e. Ring -> .1. e. ( Base ` Q ) )
32 30 31 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .1. e. ( Base ` Q ) )
33 29 32 jca 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. ( Base ` P ) /\ .1. e. ( Base ` Q ) ) )
34 33 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( X e. ( Base ` P ) /\ .1. e. ( Base ` Q ) ) )
35 34 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( X e. ( Base ` P ) /\ .1. e. ( Base ` Q ) ) )
36 eqid 
 |-  ( .r ` P ) = ( .r ` P )
37 10 24 27 12 36 matvscacell 
 |-  ( ( P e. Ring /\ ( X e. ( Base ` P ) /\ .1. e. ( Base ` Q ) ) /\ ( K e. N /\ K e. N ) ) -> ( K ( X .x. .1. ) K ) = ( X ( .r ` P ) ( K .1. K ) ) )
38 17 35 23 23 37 syl112anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( K ( X .x. .1. ) K ) = ( X ( .r ` P ) ( K .1. K ) ) )
39 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
40 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
41 simpl1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> N e. Fin )
42 10 39 40 41 17 23 23 11 mat1ov 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( K .1. K ) = if ( K = K , ( 1r ` P ) , ( 0g ` P ) ) )
43 eqid 
 |-  K = K
44 43 iftruei 
 |-  if ( K = K , ( 1r ` P ) , ( 0g ` P ) ) = ( 1r ` P )
45 42 44 eqtrdi 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( K .1. K ) = ( 1r ` P ) )
46 45 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( X ( .r ` P ) ( K .1. K ) ) = ( X ( .r ` P ) ( 1r ` P ) ) )
47 15 28 jca 
 |-  ( R e. Ring -> ( P e. Ring /\ X e. ( Base ` P ) ) )
48 47 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( P e. Ring /\ X e. ( Base ` P ) ) )
49 27 36 39 ringridm 
 |-  ( ( P e. Ring /\ X e. ( Base ` P ) ) -> ( X ( .r ` P ) ( 1r ` P ) ) = X )
50 48 49 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( X ( .r ` P ) ( 1r ` P ) ) = X )
51 50 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( X ( .r ` P ) ( 1r ` P ) ) = X )
52 38 46 51 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( K ( X .x. .1. ) K ) = X )
53 14 3 5 2 4 mat2pmatvalel 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( K e. N /\ K e. N ) ) -> ( K ( T ` M ) K ) = ( S ` ( K M K ) ) )
54 53 anabsan2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( K ( T ` M ) K ) = ( S ` ( K M K ) ) )
55 52 54 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( ( K ( X .x. .1. ) K ) .- ( K ( T ` M ) K ) ) = ( X .- ( S ` ( K M K ) ) ) )
56 26 55 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. N ) -> ( K ( ( X .x. .1. ) Z ( T ` M ) ) K ) = ( X .- ( S ` ( K M K ) ) ) )