Theorem chpdmatlem0

Description: Lemma 0 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 )
Assertion	chpdmatlem0	|- ( ( N e. Fin /\ R e. Ring ) -> ( X .x. .1. ) 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	2 10	pmatlmod	|- ( ( N e. Fin /\ R e. Ring ) -> Q e. LMod )
14		eqid	|- ( Base ` P ) = ( Base ` P )
15	6 2 14	vr1cl	|- ( R e. Ring -> X e. ( Base ` P ) )
16	15	adantl	|- ( ( N e. Fin /\ R e. Ring ) -> X e. ( Base ` P ) )
17	2	ply1ring	|- ( R e. Ring -> P e. Ring )
18	10	matsca2	|- ( ( N e. Fin /\ P e. Ring ) -> P = ( Scalar ` Q ) )
19	17 18	sylan2	|- ( ( N e. Fin /\ R e. Ring ) -> P = ( Scalar ` Q ) )
20	19	eqcomd	|- ( ( N e. Fin /\ R e. Ring ) -> ( Scalar ` Q ) = P )
21	20	fveq2d	|- ( ( N e. Fin /\ R e. Ring ) -> ( Base ` ( Scalar ` Q ) ) = ( Base ` P ) )
22	16 21	eleqtrrd	|- ( ( N e. Fin /\ R e. Ring ) -> X e. ( Base ` ( Scalar ` Q ) ) )
23	2 10	pmatring	|- ( ( N e. Fin /\ R e. Ring ) -> Q e. Ring )
24		eqid	|- ( Base ` Q ) = ( Base ` Q )
25	24 11	ringidcl	|- ( Q e. Ring -> .1. e. ( Base ` Q ) )
26	23 25	syl	|- ( ( N e. Fin /\ R e. Ring ) -> .1. e. ( Base ` Q ) )
27		eqid	|- ( Scalar ` Q ) = ( Scalar ` Q )
28		eqid	|- ( Base ` ( Scalar ` Q ) ) = ( Base ` ( Scalar ` Q ) )
29	24 27 12 28	lmodvscl	|- ( ( Q e. LMod /\ X e. ( Base ` ( Scalar ` Q ) ) /\ .1. e. ( Base ` Q ) ) -> ( X .x. .1. ) e. ( Base ` Q ) )
30	13 22 26 29	syl3anc	|- ( ( N e. Fin /\ R e. Ring ) -> ( X .x. .1. ) e. ( Base ` Q ) )