Theorem pm2mpghmlem1

Description: Lemma 1 for pm2mpghm . (Contributed by AV, 15-Oct-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	pm2mpfo.p	|- P = ( Poly1 ` R )
	pm2mpfo.c	|- C = ( N Mat P )
	pm2mpfo.b	|- B = ( Base ` C )
	pm2mpfo.m	|- .* = ( .s ` Q )
	pm2mpfo.e	|- .^ = ( .g ` ( mulGrp ` Q ) )
	pm2mpfo.x	|- X = ( var1 ` A )
	pm2mpfo.a	|- A = ( N Mat R )
	pm2mpfo.q	|- Q = ( Poly1 ` A )
	pm2mpfo.l	|- L = ( Base ` Q )
Assertion	pm2mpghmlem1	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. NN0 ) -> ( ( M decompPMat K ) .* ( K .^ X ) ) e. L )

Proof

Step	Hyp	Ref	Expression
1		pm2mpfo.p	|- P = ( Poly1 ` R )
2		pm2mpfo.c	|- C = ( N Mat P )
3		pm2mpfo.b	|- B = ( Base ` C )
4		pm2mpfo.m	|- .* = ( .s ` Q )
5		pm2mpfo.e	|- .^ = ( .g ` ( mulGrp ` Q ) )
6		pm2mpfo.x	|- X = ( var1 ` A )
7		pm2mpfo.a	|- A = ( N Mat R )
8		pm2mpfo.q	|- Q = ( Poly1 ` A )
9		pm2mpfo.l	|- L = ( Base ` Q )
10	7	matring	|- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
11	10	3adant3	|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> A e. Ring )
12	11	adantr	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. NN0 ) -> A e. Ring )
13		simpl2	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. NN0 ) -> R e. Ring )
14		simpl3	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. NN0 ) -> M e. B )
15		simpr	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. NN0 ) -> K e. NN0 )
16		eqid	|- ( Base ` A ) = ( Base ` A )
17	1 2 3 7 16	decpmatcl	|- ( ( R e. Ring /\ M e. B /\ K e. NN0 ) -> ( M decompPMat K ) e. ( Base ` A ) )
18	13 14 15 17	syl3anc	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. NN0 ) -> ( M decompPMat K ) e. ( Base ` A ) )
19		eqid	|- ( mulGrp ` Q ) = ( mulGrp ` Q )
20	16 8 6 4 19 5 9	ply1tmcl	|- ( ( A e. Ring /\ ( M decompPMat K ) e. ( Base ` A ) /\ K e. NN0 ) -> ( ( M decompPMat K ) .* ( K .^ X ) ) e. L )
21	12 18 15 20	syl3anc	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ K e. NN0 ) -> ( ( M decompPMat K ) .* ( K .^ X ) ) e. L )