Theorem pm2mpghmlem1

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

	Ref	Expression
Hypotheses	pm2mpfo.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pm2mpfo.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pm2mpfo.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pm2mpfo.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
	pm2mpfo.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
	pm2mpfo.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
	pm2mpfo.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	pm2mpfo.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	pm2mpfo.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
Assertion	pm2mpghmlem1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑀 decompPMat 𝐾 ) ∗ ( 𝐾 ↑ 𝑋 ) ) ∈ 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		pm2mpfo.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pm2mpfo.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pm2mpfo.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pm2mpfo.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
5		pm2mpfo.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6		pm2mpfo.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
7		pm2mpfo.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
8		pm2mpfo.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
9		pm2mpfo.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
10	7	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
11	10	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝐴 ∈ Ring )
12	11	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝐴 ∈ Ring )
13		simpl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑅 ∈ Ring )
14		simpl3	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
15		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
16		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
17	1 2 3 7 16	decpmatcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) ∈ ( Base ‘ 𝐴 ) )
18	13 14 15 17	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) ∈ ( Base ‘ 𝐴 ) )
19		eqid	⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
20	16 8 6 4 19 5 9	ply1tmcl	⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝑀 decompPMat 𝐾 ) ∈ ( Base ‘ 𝐴 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑀 decompPMat 𝐾 ) ∗ ( 𝐾 ↑ 𝑋 ) ) ∈ 𝐿 )
21	12 18 15 20	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑀 decompPMat 𝐾 ) ∗ ( 𝐾 ↑ 𝑋 ) ) ∈ 𝐿 )