Theorem chpdmatlem0

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

	Ref	Expression
Hypotheses	chpdmat.c	$$⊢C=N\mathrm{CharPlyMat}R$$
	chpdmat.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	chpdmat.a	$$⊢A=N\mathrm{Mat}R$$
	chpdmat.s	$$⊢S=\mathrm{algSc}\left(P\right)$$
	chpdmat.b	$$⊢B={\mathrm{Base}}_A$$
	chpdmat.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	chpdmat.0	$$⊢\underset{\dot{}}{0}=0_R$$
	chpdmat.g	$$⊢G={\mathrm{mulGrp}}_P$$
	chpdmat.m	$$⊢\underset{\dot{}}{-}={-}_P$$
	chpdmatlem.q	$$⊢Q=N\mathrm{Mat}P$$
	chpdmatlem.1	$$⊢\underset{\dot{}}{1}=1_Q$$
	chpdmatlem.m	$$⊢\underset{\dot{}}{·}={\cdot }_Q$$
Assertion	chpdmatlem0	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{1}\in {\mathrm{Base}}_Q$$

Proof

Step	Hyp	Ref	Expression
1		chpdmat.c	$$⊢C=N\mathrm{CharPlyMat}R$$
2		chpdmat.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		chpdmat.a	$$⊢A=N\mathrm{Mat}R$$
4		chpdmat.s	$$⊢S=\mathrm{algSc}\left(P\right)$$
5		chpdmat.b	$$⊢B={\mathrm{Base}}_A$$
6		chpdmat.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
7		chpdmat.0	$$⊢\underset{\dot{}}{0}=0_R$$
8		chpdmat.g	$$⊢G={\mathrm{mulGrp}}_P$$
9		chpdmat.m	$$⊢\underset{\dot{}}{-}={-}_P$$
10		chpdmatlem.q	$$⊢Q=N\mathrm{Mat}P$$
11		chpdmatlem.1	$$⊢\underset{\dot{}}{1}=1_Q$$
12		chpdmatlem.m	$$⊢\underset{\dot{}}{·}={\cdot }_Q$$
13	2 10	pmatlmod	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to Q\in \mathrm{LMod}$$
14		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
15	6 2 14	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in {\mathrm{Base}}_P$$
16	15	adantl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to X\in {\mathrm{Base}}_P$$
17	2	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
18	10	matsca2	$$⊢\left(N\in \mathrm{Fin}\wedge P\in \mathrm{Ring}\right)\to P=\mathrm{Scalar}\left(Q\right)$$
19	17 18	sylan2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to P=\mathrm{Scalar}\left(Q\right)$$
20	19	eqcomd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to \mathrm{Scalar}\left(Q\right)=P$$
21	20	fveq2d	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(Q\right)}={\mathrm{Base}}_P$$
22	16 21	eleqtrrd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(Q\right)}$$
23	2 10	pmatring	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to Q\in \mathrm{Ring}$$
24		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
25	24 11	ringidcl	$$⊢Q\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_Q$$
26	23 25	syl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to \underset{\dot{}}{1}\in {\mathrm{Base}}_Q$$
27		eqid	$$⊢\mathrm{Scalar}\left(Q\right)=\mathrm{Scalar}\left(Q\right)$$
28		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(Q\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(Q\right)}$$
29	24 27 12 28	lmodvscl	$$⊢\left(Q\in \mathrm{LMod}\wedge X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(Q\right)}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_Q\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{1}\in {\mathrm{Base}}_Q$$
30	13 22 26 29	syl3anc	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{1}\in {\mathrm{Base}}_Q$$