Theorem chpdmatlem1

Description: Lemma 1 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$$
	chpdmatlem.z	$$⊢Z={-}_Q$$
	chpdmatlem.t	$$⊢T=N\mathrm{matToPolyMat}R$$
Assertion	chpdmatlem1	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to \left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)ZT\left(M\right)\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		chpdmatlem.z	$$⊢Z={-}_Q$$
14		chpdmatlem.t	$$⊢T=N\mathrm{matToPolyMat}R$$
15	2 10	pmatring	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to Q\in \mathrm{Ring}$$
16	15	3adant3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to Q\in \mathrm{Ring}$$
17		ringgrp	$$⊢Q\in \mathrm{Ring}\to Q\in \mathrm{Grp}$$
18	16 17	syl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to Q\in \mathrm{Grp}$$
19	1 2 3 4 5 6 7 8 9 10 11 12	chpdmatlem0	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{1}\in {\mathrm{Base}}_Q$$
20	19	3adant3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{1}\in {\mathrm{Base}}_Q$$
21	14 3 5 2 10	mat2pmatbas	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to T\left(M\right)\in {\mathrm{Base}}_Q$$
22		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
23	22 13	grpsubcl	$$⊢\left(Q\in \mathrm{Grp}\wedge X\underset{\dot{}}{·}\underset{\dot{}}{1}\in {\mathrm{Base}}_Q\wedge T\left(M\right)\in {\mathrm{Base}}_Q\right)\to \left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)ZT\left(M\right)\in {\mathrm{Base}}_Q$$
24	18 20 21 23	syl3anc	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to \left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)ZT\left(M\right)\in {\mathrm{Base}}_Q$$