Metamath Proof Explorer

Theorem chpdmatlem1

Description: Lemma 1 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 chpdmatlem1 
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( X .x. .1. ) Z ( T ` M ) ) e. ( Base ` Q ) )

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 10 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. Ring )
16 15 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Q e. Ring )
17 ringgrp 
 |-  ( Q e. Ring -> Q e. Grp )
18 16 17 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Q e. Grp )
19 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 ) )
20 19 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( 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 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
23 22 13 grpsubcl 
 |-  ( ( Q e. Grp /\ ( X .x. .1. ) e. ( Base ` Q ) /\ ( T ` M ) e. ( Base ` Q ) ) -> ( ( X .x. .1. ) Z ( T ` M ) ) e. ( Base ` Q ) )
24 18 20 21 23 syl3anc 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( X .x. .1. ) Z ( T ` M ) ) e. ( Base ` Q ) )