Theorem chpdmatlem1

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

	Ref	Expression
Hypotheses	chpdmat.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	chpdmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	chpdmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	chpdmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
	chpdmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	chpdmat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	chpdmat.0	⊢ 0 = ( 0g ‘ 𝑅 )
	chpdmat.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
	chpdmat.m	⊢ − = ( -g ‘ 𝑃 )
	chpdmatlem.q	⊢ 𝑄 = ( 𝑁 Mat 𝑃 )
	chpdmatlem.1	⊢ 1 = ( 1r ‘ 𝑄 )
	chpdmatlem.m	⊢ · = ( ·𝑠 ‘ 𝑄 )
	chpdmatlem.z	⊢ 𝑍 = ( -g ‘ 𝑄 )
	chpdmatlem.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion	chpdmatlem1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑋 · 1 ) 𝑍 ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		chpdmat.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2		chpdmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		chpdmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		chpdmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
5		chpdmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
6		chpdmat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
7		chpdmat.0	⊢ 0 = ( 0g ‘ 𝑅 )
8		chpdmat.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
9		chpdmat.m	⊢ − = ( -g ‘ 𝑃 )
10		chpdmatlem.q	⊢ 𝑄 = ( 𝑁 Mat 𝑃 )
11		chpdmatlem.1	⊢ 1 = ( 1r ‘ 𝑄 )
12		chpdmatlem.m	⊢ · = ( ·𝑠 ‘ 𝑄 )
13		chpdmatlem.z	⊢ 𝑍 = ( -g ‘ 𝑄 )
14		chpdmatlem.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
15	2 10	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )
16	15	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑄 ∈ Ring )
17		ringgrp	⊢ ( 𝑄 ∈ Ring → 𝑄 ∈ Grp )
18	16 17	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑄 ∈ Grp )
19	1 2 3 4 5 6 7 8 9 10 11 12	chpdmatlem0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑄 ) )
20	19	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑄 ) )
21	14 3 5 2 10	mat2pmatbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑄 ) )
22		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
23	22 13	grpsubcl	⊢ ( ( 𝑄 ∈ Grp ∧ ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑄 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑄 ) ) → ( ( 𝑋 · 1 ) 𝑍 ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑄 ) )
24	18 20 21 23	syl3anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑋 · 1 ) 𝑍 ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑄 ) )