Metamath Proof Explorer

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 ‘ 𝑄 ) )