Metamath Proof Explorer

Theorem chfacfpmmulcl

Description: Closure of the value of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019)

Ref Expression
Hypotheses cayhamlem1.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
cayhamlem1.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
cayhamlem1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cayhamlem1.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
cayhamlem1.r ⊢ × = ( .r ‘ 𝑌 )
cayhamlem1.s ⊢ − = ( -g ‘ 𝑌 )
cayhamlem1.0 ⊢ 0 = ( 0g ‘ 𝑌 )
cayhamlem1.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
cayhamlem1.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
cayhamlem1.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑌 ) )
Assertion chfacfpmmulcl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝐾 ) ) ∈ ( Base ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 cayhamlem1.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 cayhamlem1.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 cayhamlem1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 cayhamlem1.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5 cayhamlem1.r ⊢ × = ( .r ‘ 𝑌 )
6 cayhamlem1.s ⊢ − = ( -g ‘ 𝑌 )
7 cayhamlem1.0 ⊢ 0 = ( 0g ‘ 𝑌 )
8 cayhamlem1.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
9 cayhamlem1.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
10 cayhamlem1.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑌 ) )
11 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
12 3 4 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
13 11 12 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ Ring )
14 13 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Ring )
15 14 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝑌 ∈ Ring )
16 eqid ⊢ ( mulGrp ‘ 𝑌 ) = ( mulGrp ‘ 𝑌 )
17 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
18 16 17 mgpbas ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ ( mulGrp ‘ 𝑌 ) )
19 16 ringmgp ⊢ ( 𝑌 ∈ Ring → ( mulGrp ‘ 𝑌 ) ∈ Mnd )
20 14 19 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝑌 ) ∈ Mnd )
21 20 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( mulGrp ‘ 𝑌 ) ∈ Mnd )
22 simp3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
23 8 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
24 11 23 syl3an2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
25 24 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
26 18 10 21 22 25 mulgnn0cld ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
27 1 2 3 4 5 6 7 8 9 chfacfisf ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )
28 11 27 syl3anl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )
29 28 3adant3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )
30 29 22 ffvelcdmd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑌 ) )
31 17 5 ringcl ⊢ ( ( 𝑌 ∈ Ring ∧ ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝐾 ) ) ∈ ( Base ‘ 𝑌 ) )
32 15 26 30 31 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝐾 ) ) ∈ ( Base ‘ 𝑌 ) )