# Metamath Proof Explorer

## Theorem pm2mpfo

Description: The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 12-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpfo.p 𝑃 = ( Poly1𝑅 )
pm2mpfo.c 𝐶 = ( 𝑁 Mat 𝑃 )
pm2mpfo.b 𝐵 = ( Base ‘ 𝐶 )
pm2mpfo.m = ( ·𝑠𝑄 )
pm2mpfo.e = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
pm2mpfo.x 𝑋 = ( var1𝐴 )
pm2mpfo.a 𝐴 = ( 𝑁 Mat 𝑅 )
pm2mpfo.q 𝑄 = ( Poly1𝐴 )
pm2mpfo.l 𝐿 = ( Base ‘ 𝑄 )
pm2mpfo.t 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion pm2mpfo ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵onto𝐿 )

### Proof

Step Hyp Ref Expression
1 pm2mpfo.p 𝑃 = ( Poly1𝑅 )
2 pm2mpfo.c 𝐶 = ( 𝑁 Mat 𝑃 )
3 pm2mpfo.b 𝐵 = ( Base ‘ 𝐶 )
4 pm2mpfo.m = ( ·𝑠𝑄 )
5 pm2mpfo.e = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6 pm2mpfo.x 𝑋 = ( var1𝐴 )
7 pm2mpfo.a 𝐴 = ( 𝑁 Mat 𝑅 )
8 pm2mpfo.q 𝑄 = ( Poly1𝐴 )
9 pm2mpfo.l 𝐿 = ( Base ‘ 𝑄 )
10 pm2mpfo.t 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
11 1 2 3 4 5 6 7 8 10 9 pm2mpf ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵𝐿 )
12 eqid ( ·𝑠𝑃 ) = ( ·𝑠𝑃 )
13 eqid ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
14 eqid ( var1𝑅 ) = ( var1𝑅 )
15 eqid ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) = ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) )
16 7 8 9 12 13 14 15 1 10 mp2pm2mp ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑝𝐿 ) → ( 𝑇 ‘ ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) = 𝑝 )
17 16 3expa ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝𝐿 ) → ( 𝑇 ‘ ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) = 𝑝 )
18 7 8 9 1 12 13 14 15 2 3 mply1topmatcl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑝𝐿 ) → ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ∈ 𝐵 )
19 18 3expa ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝𝐿 ) → ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ∈ 𝐵 )
20 simpr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝𝐿 ) ∧ 𝑓 = ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) → 𝑓 = ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) )
21 20 fveq2d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝𝐿 ) ∧ 𝑓 = ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) → ( 𝑇𝑓 ) = ( 𝑇 ‘ ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) )
22 21 eqeq2d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝𝐿 ) ∧ 𝑓 = ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) → ( 𝑝 = ( 𝑇𝑓 ) ↔ 𝑝 = ( 𝑇 ‘ ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) ) )
23 19 22 rspcedv ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝𝐿 ) → ( 𝑝 = ( 𝑇 ‘ ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) → ∃ 𝑓𝐵 𝑝 = ( 𝑇𝑓 ) ) )
24 23 com12 ( 𝑝 = ( 𝑇 ‘ ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝𝐿 ) → ∃ 𝑓𝐵 𝑝 = ( 𝑇𝑓 ) ) )
25 24 eqcoms ( ( 𝑇 ‘ ( ( 𝑙𝐿 ↦ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1𝑙 ) ‘ 𝑘 ) 𝑗 ) ( ·𝑠𝑃 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1𝑅 ) ) ) ) ) ) ) ‘ 𝑝 ) ) = 𝑝 → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝𝐿 ) → ∃ 𝑓𝐵 𝑝 = ( 𝑇𝑓 ) ) )
26 17 25 mpcom ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑝𝐿 ) → ∃ 𝑓𝐵 𝑝 = ( 𝑇𝑓 ) )
27 26 ralrimiva ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑝𝐿𝑓𝐵 𝑝 = ( 𝑇𝑓 ) )
28 dffo3 ( 𝑇 : 𝐵onto𝐿 ↔ ( 𝑇 : 𝐵𝐿 ∧ ∀ 𝑝𝐿𝑓𝐵 𝑝 = ( 𝑇𝑓 ) ) )
29 11 27 28 sylanbrc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵onto𝐿 )