Metamath Proof Explorer

Theorem mat2pmat1

Description: The transformation of the identity matrix results in the identity polynomial matrix. (Contributed by AV, 29-Oct-2019)

Ref Expression
Hypotheses mat2pmatbas.t ⊢ T = N matToPolyMat R
mat2pmatbas.a ⊢ A = N Mat R
mat2pmatbas.b ⊢ B = Base A
mat2pmatbas.p ⊢ P = Poly 1 ⁡ R
mat2pmatbas.c ⊢ C = N Mat P
mat2pmatbas0.h ⊢ H = Base C
Assertion mat2pmat1 ⊢ N ∈ Fin ∧ R ∈ Ring → T ⁡ 1 A = 1 C

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t ⊢ T = N matToPolyMat R
2 mat2pmatbas.a ⊢ A = N Mat R
3 mat2pmatbas.b ⊢ B = Base A
4 mat2pmatbas.p ⊢ P = Poly 1 ⁡ R
5 mat2pmatbas.c ⊢ C = N Mat P
6 mat2pmatbas0.h ⊢ H = Base C
7 simpl ⊢ N ∈ Fin ∧ R ∈ Ring → N ∈ Fin
8 simpr ⊢ N ∈ Fin ∧ R ∈ Ring → R ∈ Ring
9 2 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
10 eqid ⊢ 1 A = 1 A
11 3 10 ringidcl ⊢ A ∈ Ring → 1 A ∈ B
12 9 11 syl ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ B
13 7 8 12 3jca ⊢ N ∈ Fin ∧ R ∈ Ring → N ∈ Fin ∧ R ∈ Ring ∧ 1 A ∈ B
14 eqid ⊢ algSc ⁡ P = algSc ⁡ P
15 1 2 3 4 14 mat2pmatvalel ⊢ N ∈ Fin ∧ R ∈ Ring ∧ 1 A ∈ B ∧ i ∈ N ∧ j ∈ N → i T ⁡ 1 A j = algSc ⁡ P ⁡ i 1 A j
16 13 15 sylan ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → i T ⁡ 1 A j = algSc ⁡ P ⁡ i 1 A j
17 fvif ⊢ algSc ⁡ P ⁡ if i = j 1 R 0 R = if i = j algSc ⁡ P ⁡ 1 R algSc ⁡ P ⁡ 0 R
18 eqid ⊢ 1 R = 1 R
19 eqid ⊢ 1 P = 1 P
20 4 14 18 19 ply1scl1 ⊢ R ∈ Ring → algSc ⁡ P ⁡ 1 R = 1 P
21 20 ad2antlr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → algSc ⁡ P ⁡ 1 R = 1 P
22 eqid ⊢ 0 R = 0 R
23 eqid ⊢ 0 P = 0 P
24 4 14 22 23 ply1scl0 ⊢ R ∈ Ring → algSc ⁡ P ⁡ 0 R = 0 P
25 24 ad2antlr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → algSc ⁡ P ⁡ 0 R = 0 P
26 21 25 ifeq12d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → if i = j algSc ⁡ P ⁡ 1 R algSc ⁡ P ⁡ 0 R = if i = j 1 P 0 P
27 17 26 syl5eq ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → algSc ⁡ P ⁡ if i = j 1 R 0 R = if i = j 1 P 0 P
28 7 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → N ∈ Fin
29 8 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → R ∈ Ring
30 simpl ⊢ i ∈ N ∧ j ∈ N → i ∈ N
31 30 adantl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → i ∈ N
32 simpr ⊢ i ∈ N ∧ j ∈ N → j ∈ N
33 32 adantl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → j ∈ N
34 2 18 22 28 29 31 33 10 mat1ov ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → i 1 A j = if i = j 1 R 0 R
35 34 fveq2d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → algSc ⁡ P ⁡ i 1 A j = algSc ⁡ P ⁡ if i = j 1 R 0 R
36 4 ply1ring ⊢ R ∈ Ring → P ∈ Ring
37 36 ad2antlr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → P ∈ Ring
38 eqid ⊢ 1 C = 1 C
39 5 19 23 28 37 31 33 38 mat1ov ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → i 1 C j = if i = j 1 P 0 P
40 27 35 39 3eqtr4d ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → algSc ⁡ P ⁡ i 1 A j = i 1 C j
41 16 40 eqtrd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → i T ⁡ 1 A j = i 1 C j
42 41 ralrimivva ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ i ∈ N ∀ j ∈ N i T ⁡ 1 A j = i 1 C j
43 1 2 3 4 5 6 mat2pmatbas0 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ 1 A ∈ B → T ⁡ 1 A ∈ H
44 13 43 syl ⊢ N ∈ Fin ∧ R ∈ Ring → T ⁡ 1 A ∈ H
45 4 5 pmatring ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ Ring
46 6 38 ringidcl ⊢ C ∈ Ring → 1 C ∈ H
47 45 46 syl ⊢ N ∈ Fin ∧ R ∈ Ring → 1 C ∈ H
48 5 6 eqmat ⊢ T ⁡ 1 A ∈ H ∧ 1 C ∈ H → T ⁡ 1 A = 1 C ↔ ∀ i ∈ N ∀ j ∈ N i T ⁡ 1 A j = i 1 C j
49 44 47 48 syl2anc ⊢ N ∈ Fin ∧ R ∈ Ring → T ⁡ 1 A = 1 C ↔ ∀ i ∈ N ∀ j ∈ N i T ⁡ 1 A j = i 1 C j
50 42 49 mpbird ⊢ N ∈ Fin ∧ R ∈ Ring → T ⁡ 1 A = 1 C