Theorem chpdmatlem0

Description: Lemma 0 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	⊢ · = ( ·𝑠 ‘ 𝑄 )
Assertion	chpdmatlem0	⊢ ( ( 𝑁 ∈ 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	2 10	pmatlmod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ LMod )
14		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
15	6 2 14	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
16	15	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
17	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
18	10	matsca2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝑃 = ( Scalar ‘ 𝑄 ) )
19	17 18	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑃 = ( Scalar ‘ 𝑄 ) )
20	19	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ 𝑄 ) = 𝑃 )
21	20	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ ( Scalar ‘ 𝑄 ) ) = ( Base ‘ 𝑃 ) )
22	16 21	eleqtrrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
23	2 10	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )
24		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
25	24 11	ringidcl	⊢ ( 𝑄 ∈ Ring → 1 ∈ ( Base ‘ 𝑄 ) )
26	23 25	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 1 ∈ ( Base ‘ 𝑄 ) )
27		eqid	⊢ ( Scalar ‘ 𝑄 ) = ( Scalar ‘ 𝑄 )
28		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑄 ) ) = ( Base ‘ ( Scalar ‘ 𝑄 ) )
29	24 27 12 28	lmodvscl	⊢ ( ( 𝑄 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ∧ 1 ∈ ( Base ‘ 𝑄 ) ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑄 ) )
30	13 22 26 29	syl3anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑄 ) )