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 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
mat2pmatbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
mat2pmatbas.b 𝐵 = ( Base ‘ 𝐴 )
mat2pmatbas.p 𝑃 = ( Poly1𝑅 )
mat2pmatbas.c 𝐶 = ( 𝑁 Mat 𝑃 )
mat2pmatbas0.h 𝐻 = ( Base ‘ 𝐶 )
Assertion mat2pmat1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ‘ ( 1r𝐴 ) ) = ( 1r𝐶 ) )

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2 mat2pmatbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
3 mat2pmatbas.b 𝐵 = ( Base ‘ 𝐴 )
4 mat2pmatbas.p 𝑃 = ( Poly1𝑅 )
5 mat2pmatbas.c 𝐶 = ( 𝑁 Mat 𝑃 )
6 mat2pmatbas0.h 𝐻 = ( Base ‘ 𝐶 )
7 simpl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin )
8 simpr ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
9 2 matring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
10 eqid ( 1r𝐴 ) = ( 1r𝐴 )
11 3 10 ringidcl ( 𝐴 ∈ Ring → ( 1r𝐴 ) ∈ 𝐵 )
12 9 11 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r𝐴 ) ∈ 𝐵 )
13 7 8 12 3jca ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 1r𝐴 ) ∈ 𝐵 ) )
14 eqid ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
15 1 2 3 4 14 mat2pmatvalel ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 1r𝐴 ) ∈ 𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 1r𝐴 ) ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 1r𝐴 ) 𝑗 ) ) )
16 13 15 sylan ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 1r𝐴 ) ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 1r𝐴 ) 𝑗 ) ) )
17 fvif ( ( algSc ‘ 𝑃 ) ‘ if ( 𝑖 = 𝑗 , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) = if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1r𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) )
18 eqid ( 1r𝑅 ) = ( 1r𝑅 )
19 eqid ( 1r𝑃 ) = ( 1r𝑃 )
20 4 14 18 19 ply1scl1 ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 1r𝑅 ) ) = ( 1r𝑃 ) )
21 20 ad2antlr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 1r𝑅 ) ) = ( 1r𝑃 ) )
22 eqid ( 0g𝑅 ) = ( 0g𝑅 )
23 eqid ( 0g𝑃 ) = ( 0g𝑃 )
24 4 14 22 23 ply1scl0 ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) = ( 0g𝑃 ) )
25 24 ad2antlr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) = ( 0g𝑃 ) )
26 21 25 ifeq12d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → if ( 𝑖 = 𝑗 , ( ( algSc ‘ 𝑃 ) ‘ ( 1r𝑅 ) ) , ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) ) = if ( 𝑖 = 𝑗 , ( 1r𝑃 ) , ( 0g𝑃 ) ) )
27 17 26 syl5eq ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( ( algSc ‘ 𝑃 ) ‘ if ( 𝑖 = 𝑗 , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) = if ( 𝑖 = 𝑗 , ( 1r𝑃 ) , ( 0g𝑃 ) ) )
28 7 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑁 ∈ Fin )
29 8 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑅 ∈ Ring )
30 simpl ( ( 𝑖𝑁𝑗𝑁 ) → 𝑖𝑁 )
31 30 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑖𝑁 )
32 simpr ( ( 𝑖𝑁𝑗𝑁 ) → 𝑗𝑁 )
33 32 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑗𝑁 )
34 2 18 22 28 29 31 33 10 mat1ov ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 1r𝐴 ) 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r𝑅 ) , ( 0g𝑅 ) ) )
35 34 fveq2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 1r𝐴 ) 𝑗 ) ) = ( ( algSc ‘ 𝑃 ) ‘ if ( 𝑖 = 𝑗 , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) )
36 4 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
37 36 ad2antlr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑃 ∈ Ring )
38 eqid ( 1r𝐶 ) = ( 1r𝐶 )
39 5 19 23 28 37 31 33 38 mat1ov ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 1r𝐶 ) 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r𝑃 ) , ( 0g𝑃 ) ) )
40 27 35 39 3eqtr4d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 1r𝐴 ) 𝑗 ) ) = ( 𝑖 ( 1r𝐶 ) 𝑗 ) )
41 16 40 eqtrd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 1r𝐴 ) ) 𝑗 ) = ( 𝑖 ( 1r𝐶 ) 𝑗 ) )
42 41 ralrimivva ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 ( 𝑇 ‘ ( 1r𝐴 ) ) 𝑗 ) = ( 𝑖 ( 1r𝐶 ) 𝑗 ) )
43 1 2 3 4 5 6 mat2pmatbas0 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 1r𝐴 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 1r𝐴 ) ) ∈ 𝐻 )
44 13 43 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ‘ ( 1r𝐴 ) ) ∈ 𝐻 )
45 4 5 pmatring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
46 6 38 ringidcl ( 𝐶 ∈ Ring → ( 1r𝐶 ) ∈ 𝐻 )
47 45 46 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r𝐶 ) ∈ 𝐻 )
48 5 6 eqmat ( ( ( 𝑇 ‘ ( 1r𝐴 ) ) ∈ 𝐻 ∧ ( 1r𝐶 ) ∈ 𝐻 ) → ( ( 𝑇 ‘ ( 1r𝐴 ) ) = ( 1r𝐶 ) ↔ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 ( 𝑇 ‘ ( 1r𝐴 ) ) 𝑗 ) = ( 𝑖 ( 1r𝐶 ) 𝑗 ) ) )
49 44 47 48 syl2anc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑇 ‘ ( 1r𝐴 ) ) = ( 1r𝐶 ) ↔ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 ( 𝑇 ‘ ( 1r𝐴 ) ) 𝑗 ) = ( 𝑖 ( 1r𝐶 ) 𝑗 ) ) )
50 42 49 mpbird ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ‘ ( 1r𝐴 ) ) = ( 1r𝐶 ) )