Metamath Proof Explorer

Theorem chmatcl

Description: Closure of the characteristic matrix of a matrix. (Contributed by AV, 25-Oct-2019) (Proof shortened by AV, 29-Nov-2019)

Ref Expression
Hypotheses chmatcl.a ⊢ A = N Mat R
chmatcl.b ⊢ B = Base A
chmatcl.p ⊢ P = Poly 1 ⁡ R
chmatcl.y ⊢ Y = N Mat P
chmatcl.x ⊢ X = var 1 ⁡ R
chmatcl.t ⊢ T = N matToPolyMat R
chmatcl.s ⊢ - ˙ = - Y
chmatcl.m ⊢ · ˙ = ⋅ Y
chmatcl.1 ⊢ 1 ˙ = 1 Y
chmatcl.h ⊢ H = X · ˙ 1 ˙ - ˙ T ⁡ M
Assertion chmatcl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → H ∈ Base Y

Proof

Step Hyp Ref Expression
1 chmatcl.a ⊢ A = N Mat R
2 chmatcl.b ⊢ B = Base A
3 chmatcl.p ⊢ P = Poly 1 ⁡ R
4 chmatcl.y ⊢ Y = N Mat P
5 chmatcl.x ⊢ X = var 1 ⁡ R
6 chmatcl.t ⊢ T = N matToPolyMat R
7 chmatcl.s ⊢ - ˙ = - Y
8 chmatcl.m ⊢ · ˙ = ⋅ Y
9 chmatcl.1 ⊢ 1 ˙ = 1 Y
10 chmatcl.h ⊢ H = X · ˙ 1 ˙ - ˙ T ⁡ M
11 3 4 pmatring ⊢ N ∈ Fin ∧ R ∈ Ring → Y ∈ Ring
12 ringgrp ⊢ Y ∈ Ring → Y ∈ Grp
13 11 12 syl ⊢ N ∈ Fin ∧ R ∈ Ring → Y ∈ Grp
14 13 3adant3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → Y ∈ Grp
15 3 ply1ring ⊢ R ∈ Ring → P ∈ Ring
16 15 anim2i ⊢ N ∈ Fin ∧ R ∈ Ring → N ∈ Fin ∧ P ∈ Ring
17 16 3adant3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → N ∈ Fin ∧ P ∈ Ring
18 eqid ⊢ Base P = Base P
19 5 3 18 vr1cl ⊢ R ∈ Ring → X ∈ Base P
20 19 3ad2ant2 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → X ∈ Base P
21 11 3adant3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → Y ∈ Ring
22 eqid ⊢ Base Y = Base Y
23 22 9 ringidcl ⊢ Y ∈ Ring → 1 ˙ ∈ Base Y
24 21 23 syl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → 1 ˙ ∈ Base Y
25 18 4 22 8 matvscl ⊢ N ∈ Fin ∧ P ∈ Ring ∧ X ∈ Base P ∧ 1 ˙ ∈ Base Y → X · ˙ 1 ˙ ∈ Base Y
26 17 20 24 25 syl12anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → X · ˙ 1 ˙ ∈ Base Y
27 6 1 2 3 4 mat2pmatbas ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → T ⁡ M ∈ Base Y
28 22 7 grpsubcl ⊢ Y ∈ Grp ∧ X · ˙ 1 ˙ ∈ Base Y ∧ T ⁡ M ∈ Base Y → X · ˙ 1 ˙ - ˙ T ⁡ M ∈ Base Y
29 14 26 27 28 syl3anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → X · ˙ 1 ˙ - ˙ T ⁡ M ∈ Base Y
30 10 29 eqeltrid ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → H ∈ Base Y