Metamath Proof Explorer

Theorem mat2pmatf1

Description: The matrix transformation is a 1-1 function from the matrices to the polynomial matrices. (Contributed by AV, 28-Oct-2019) (Proof shortened by AV, 27-Nov-2019)

Ref Expression
Hypotheses mat2pmatbas.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
mat2pmatbas.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mat2pmatbas.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mat2pmatbas.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
mat2pmatbas.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
mat2pmatbas0.h ⊢ 𝐻 = ( Base ‘ 𝐶 )
Assertion mat2pmatf1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –1-1→ 𝐻 )

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 1 2 3 4 5 6 mat2pmatf ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 ⟶ 𝐻 )
8 simpl ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
9 8 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝐵 ) )
10 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝐵 ) )
11 9 10 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) )
12 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
13 1 2 3 4 12 mat2pmatvalel ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) )
14 11 13 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) )
15 simpr ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
16 15 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝐵 ) )
17 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝐵 ) )
18 16 17 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) )
19 1 2 3 4 12 mat2pmatvalel ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ 𝑦 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) )
20 18 19 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ 𝑦 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) )
21 14 20 eqeq12d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑖 ( 𝑇 ‘ 𝑥 ) 𝑗 ) = ( 𝑖 ( 𝑇 ‘ 𝑦 ) 𝑗 ) ↔ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) )
22 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
23 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
24 4 12 22 23 ply1sclf1 ⊢ ( 𝑅 ∈ Ring → ( algSc ‘ 𝑃 ) : ( Base ‘ 𝑅 ) –1-1→ ( Base ‘ 𝑃 ) )
25 24 ad3antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( algSc ‘ 𝑃 ) : ( Base ‘ 𝑅 ) –1-1→ ( Base ‘ 𝑃 ) )
26 simprl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
27 simprr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
28 simplrl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑥 ∈ 𝐵 )
29 2 22 3 26 27 28 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
30 simplrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑦 ∈ 𝐵 )
31 2 22 3 26 27 30 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
32 f1veqaeq ⊢ ( ( ( algSc ‘ 𝑃 ) : ( Base ‘ 𝑅 ) –1-1→ ( Base ‘ 𝑃 ) ∧ ( ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) → ( 𝑖 𝑥 𝑗 ) = ( 𝑖 𝑦 𝑗 ) ) )
33 25 29 31 32 syl12anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) → ( 𝑖 𝑥 𝑗 ) = ( 𝑖 𝑦 𝑗 ) ) )
34 21 33 sylbid ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑖 ( 𝑇 ‘ 𝑥 ) 𝑗 ) = ( 𝑖 ( 𝑇 ‘ 𝑦 ) 𝑗 ) → ( 𝑖 𝑥 𝑗 ) = ( 𝑖 𝑦 𝑗 ) ) )
35 34 ralimdvva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑇 ‘ 𝑥 ) 𝑗 ) = ( 𝑖 ( 𝑇 ‘ 𝑦 ) 𝑗 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑥 𝑗 ) = ( 𝑖 𝑦 𝑗 ) ) )
36 1 2 3 4 5 6 mat2pmatbas0 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑥 ) ∈ 𝐻 )
37 11 36 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑥 ) ∈ 𝐻 )
38 1 2 3 4 5 6 mat2pmatbas0 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑦 ) ∈ 𝐻 )
39 18 38 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑦 ) ∈ 𝐻 )
40 5 6 eqmat ⊢ ( ( ( 𝑇 ‘ 𝑥 ) ∈ 𝐻 ∧ ( 𝑇 ‘ 𝑦 ) ∈ 𝐻 ) → ( ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑦 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑇 ‘ 𝑥 ) 𝑗 ) = ( 𝑖 ( 𝑇 ‘ 𝑦 ) 𝑗 ) ) )
41 37 39 40 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑦 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑇 ‘ 𝑥 ) 𝑗 ) = ( 𝑖 ( 𝑇 ‘ 𝑦 ) 𝑗 ) ) )
42 2 3 eqmat ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑥 𝑗 ) = ( 𝑖 𝑦 𝑗 ) ) )
43 42 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑥 𝑗 ) = ( 𝑖 𝑦 𝑗 ) ) )
44 35 41 43 3imtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
45 44 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
46 dff13 ⊢ ( 𝑇 : 𝐵 –1-1→ 𝐻 ↔ ( 𝑇 : 𝐵 ⟶ 𝐻 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
47 7 45 46 sylanbrc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –1-1→ 𝐻 )