MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pmatcollpw3lem Structured version   Visualization version   GIF version

Theorem pmatcollpw3lem 22672
Description: Lemma for pmatcollpw3 22673 and pmatcollpw3fi 22674: Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 8-Dec-2019.)
Hypotheses
Ref Expression
pmatcollpw.p ๐‘ƒ = (Poly1โ€˜๐‘…)
pmatcollpw.c ๐ถ = (๐‘ Mat ๐‘ƒ)
pmatcollpw.b ๐ต = (Baseโ€˜๐ถ)
pmatcollpw.m โˆ— = ( ยท๐‘  โ€˜๐ถ)
pmatcollpw.e โ†‘ = (.gโ€˜(mulGrpโ€˜๐‘ƒ))
pmatcollpw.x ๐‘‹ = (var1โ€˜๐‘…)
pmatcollpw.t ๐‘‡ = (๐‘ matToPolyMat ๐‘…)
pmatcollpw3.a ๐ด = (๐‘ Mat ๐‘…)
pmatcollpw3.d ๐ท = (Baseโ€˜๐ด)
Assertion
Ref Expression
pmatcollpw3lem (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ (๐‘€ = (๐ถ ฮฃg (๐‘› โˆˆ ๐ผ โ†ฆ ((๐‘› โ†‘ ๐‘‹) โˆ— (๐‘‡โ€˜(๐‘€ decompPMat ๐‘›))))) โ†’ โˆƒ๐‘“ โˆˆ (๐ท โ†‘m ๐ผ)๐‘€ = (๐ถ ฮฃg (๐‘› โˆˆ ๐ผ โ†ฆ ((๐‘› โ†‘ ๐‘‹) โˆ— (๐‘‡โ€˜(๐‘“โ€˜๐‘›)))))))
Distinct variable groups:   ๐ต,๐‘›   ๐‘›,๐‘€   ๐‘›,๐‘   ๐‘ƒ,๐‘›   ๐‘…,๐‘›   ๐‘›,๐‘‹   โ†‘ ,๐‘›   ๐ถ,๐‘›   ๐ต,๐‘“   ๐ถ,๐‘“,๐‘›   ๐ท,๐‘“   ๐‘“,๐ผ,๐‘›   ๐‘“,๐‘€   ๐‘“,๐‘   ๐‘…,๐‘“   ๐‘‡,๐‘“   ๐‘“,๐‘‹   โ†‘ ,๐‘“   โˆ— ,๐‘“
Allowed substitution hints:   ๐ด(๐‘“,๐‘›)   ๐ท(๐‘›)   ๐‘ƒ(๐‘“)   ๐‘‡(๐‘›)   โˆ— (๐‘›)

Proof of Theorem pmatcollpw3lem
Dummy variables ๐‘– ๐‘— ๐‘˜ ๐‘™ ๐‘ฅ ๐‘ฆ ๐‘š are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmeq 5900 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ dom ๐‘ฅ = dom ๐‘ฆ)
21dmeqd 5902 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ dom dom ๐‘ฅ = dom dom ๐‘ฆ)
3 oveq 7420 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘–๐‘ฅ๐‘—) = (๐‘–๐‘ฆ๐‘—))
43fveq2d 6895 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ (coe1โ€˜(๐‘–๐‘ฅ๐‘—)) = (coe1โ€˜(๐‘–๐‘ฆ๐‘—)))
54fveq1d 6893 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜) = ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘˜))
62, 2, 5mpoeq123dv 7489 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘˜)))
7 fveq2 6891 . . . . . . . 8 (๐‘˜ = ๐‘™ โ†’ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘˜) = ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘™))
87mpoeq3dv 7493 . . . . . . 7 (๐‘˜ = ๐‘™ โ†’ (๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘™)))
96, 8cbvmpov 7509 . . . . . 6 (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜))) = (๐‘ฆ โˆˆ ๐ต, ๐‘™ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘™)))
10 dmexg 7903 . . . . . . . . . . 11 (๐‘ฆ โˆˆ ๐ต โ†’ dom ๐‘ฆ โˆˆ V)
1110dmexd 7905 . . . . . . . . . 10 (๐‘ฆ โˆˆ ๐ต โ†’ dom dom ๐‘ฆ โˆˆ V)
1211, 11jca 511 . . . . . . . . 9 (๐‘ฆ โˆˆ ๐ต โ†’ (dom dom ๐‘ฆ โˆˆ V โˆง dom dom ๐‘ฆ โˆˆ V))
1312ad2antrl 727 . . . . . . . 8 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง (๐‘ฆ โˆˆ ๐ต โˆง ๐‘™ โˆˆ ๐ผ)) โ†’ (dom dom ๐‘ฆ โˆˆ V โˆง dom dom ๐‘ฆ โˆˆ V))
14 mpoexga 8076 . . . . . . . 8 ((dom dom ๐‘ฆ โˆˆ V โˆง dom dom ๐‘ฆ โˆˆ V) โ†’ (๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘™)) โˆˆ V)
1513, 14syl 17 . . . . . . 7 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง (๐‘ฆ โˆˆ ๐ต โˆง ๐‘™ โˆˆ ๐ผ)) โ†’ (๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘™)) โˆˆ V)
1615ralrimivva 3195 . . . . . 6 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘™ โˆˆ ๐ผ (๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘™)) โˆˆ V)
17 simprr 772 . . . . . 6 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ ๐ผ โ‰  โˆ…)
18 nn0ex 12500 . . . . . . . 8 โ„•0 โˆˆ V
1918ssex 5315 . . . . . . 7 (๐ผ โІ โ„•0 โ†’ ๐ผ โˆˆ V)
2019ad2antrl 727 . . . . . 6 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ ๐ผ โˆˆ V)
21 simp3 1136 . . . . . . 7 ((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐‘€ โˆˆ ๐ต)
2221adantr 480 . . . . . 6 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ ๐‘€ โˆˆ ๐ต)
239, 16, 17, 20, 22mpocurryvald 8269 . . . . 5 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€) = (๐‘™ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘ฆโฆŒ(๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘™))))
24 fveq2 6891 . . . . . . . . 9 (๐‘™ = ๐‘˜ โ†’ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘™) = ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘˜))
2524mpoeq3dv 7493 . . . . . . . 8 (๐‘™ = ๐‘˜ โ†’ (๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘™)) = (๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘˜)))
2625csbeq2dv 3896 . . . . . . 7 (๐‘™ = ๐‘˜ โ†’ โฆ‹๐‘€ / ๐‘ฆโฆŒ(๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘™)) = โฆ‹๐‘€ / ๐‘ฆโฆŒ(๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘˜)))
27 eqcom 2734 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†” ๐‘ฆ = ๐‘ฅ)
28 eqcom 2734 . . . . . . . . 9 ((๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘˜)) โ†” (๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))
296, 27, 283imtr3i 291 . . . . . . . 8 (๐‘ฆ = ๐‘ฅ โ†’ (๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))
3029cbvcsbv 3901 . . . . . . 7 โฆ‹๐‘€ / ๐‘ฆโฆŒ(๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘˜)) = โฆ‹๐‘€ / ๐‘ฅโฆŒ(๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜))
3126, 30eqtrdi 2783 . . . . . 6 (๐‘™ = ๐‘˜ โ†’ โฆ‹๐‘€ / ๐‘ฆโฆŒ(๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘™)) = โฆ‹๐‘€ / ๐‘ฅโฆŒ(๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))
3231cbvmptv 5255 . . . . 5 (๐‘™ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘ฆโฆŒ(๐‘– โˆˆ dom dom ๐‘ฆ, ๐‘— โˆˆ dom dom ๐‘ฆ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฆ๐‘—))โ€˜๐‘™))) = (๐‘˜ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘ฅโฆŒ(๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))
3323, 32eqtrdi 2783 . . . 4 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€) = (๐‘˜ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘ฅโฆŒ(๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜))))
34 dmeq 5900 . . . . . . . . . . 11 (๐‘ฅ = ๐‘€ โ†’ dom ๐‘ฅ = dom ๐‘€)
3534dmeqd 5902 . . . . . . . . . 10 (๐‘ฅ = ๐‘€ โ†’ dom dom ๐‘ฅ = dom dom ๐‘€)
36 oveq 7420 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘€ โ†’ (๐‘–๐‘ฅ๐‘—) = (๐‘–๐‘€๐‘—))
3736fveq2d 6895 . . . . . . . . . . 11 (๐‘ฅ = ๐‘€ โ†’ (coe1โ€˜(๐‘–๐‘ฅ๐‘—)) = (coe1โ€˜(๐‘–๐‘€๐‘—)))
3837fveq1d 6893 . . . . . . . . . 10 (๐‘ฅ = ๐‘€ โ†’ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜) = ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜))
3935, 35, 38mpoeq123dv 7489 . . . . . . . . 9 (๐‘ฅ = ๐‘€ โ†’ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ dom dom ๐‘€, ๐‘— โˆˆ dom dom ๐‘€ โ†ฆ ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜)))
4039adantl 481 . . . . . . . 8 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ฅ = ๐‘€) โ†’ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ dom dom ๐‘€, ๐‘— โˆˆ dom dom ๐‘€ โ†ฆ ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜)))
4121, 40csbied 3927 . . . . . . 7 ((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ โฆ‹๐‘€ / ๐‘ฅโฆŒ(๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ dom dom ๐‘€, ๐‘— โˆˆ dom dom ๐‘€ โ†ฆ ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜)))
42 pmatcollpw.c . . . . . . . . . . . . 13 ๐ถ = (๐‘ Mat ๐‘ƒ)
43 eqid 2727 . . . . . . . . . . . . 13 (Baseโ€˜๐‘ƒ) = (Baseโ€˜๐‘ƒ)
44 pmatcollpw.b . . . . . . . . . . . . 13 ๐ต = (Baseโ€˜๐ถ)
4542, 43, 44matbas2i 22311 . . . . . . . . . . . 12 (๐‘€ โˆˆ ๐ต โ†’ ๐‘€ โˆˆ ((Baseโ€˜๐‘ƒ) โ†‘m (๐‘ ร— ๐‘)))
46 elmapi 8859 . . . . . . . . . . . 12 (๐‘€ โˆˆ ((Baseโ€˜๐‘ƒ) โ†‘m (๐‘ ร— ๐‘)) โ†’ ๐‘€:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘ƒ))
47 fdm 6725 . . . . . . . . . . . . . 14 (๐‘€:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘ƒ) โ†’ dom ๐‘€ = (๐‘ ร— ๐‘))
4847dmeqd 5902 . . . . . . . . . . . . 13 (๐‘€:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘ƒ) โ†’ dom dom ๐‘€ = dom (๐‘ ร— ๐‘))
49 dmxpid 5926 . . . . . . . . . . . . 13 dom (๐‘ ร— ๐‘) = ๐‘
5048, 49eqtr2di 2784 . . . . . . . . . . . 12 (๐‘€:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘ƒ) โ†’ ๐‘ = dom dom ๐‘€)
5145, 46, 503syl 18 . . . . . . . . . . 11 (๐‘€ โˆˆ ๐ต โ†’ ๐‘ = dom dom ๐‘€)
52513ad2ant3 1133 . . . . . . . . . 10 ((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐‘ = dom dom ๐‘€)
5352adantr 480 . . . . . . . . 9 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘š = ๐‘€) โ†’ ๐‘ = dom dom ๐‘€)
54 simpr 484 . . . . . . . . . . . 12 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘š = ๐‘€) โ†’ ๐‘š = ๐‘€)
5554oveqd 7431 . . . . . . . . . . 11 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘š = ๐‘€) โ†’ (๐‘–๐‘š๐‘—) = (๐‘–๐‘€๐‘—))
5655fveq2d 6895 . . . . . . . . . 10 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘š = ๐‘€) โ†’ (coe1โ€˜(๐‘–๐‘š๐‘—)) = (coe1โ€˜(๐‘–๐‘€๐‘—)))
5756fveq1d 6893 . . . . . . . . 9 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘š = ๐‘€) โ†’ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜) = ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜))
5853, 53, 57mpoeq123dv 7489 . . . . . . . 8 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘š = ๐‘€) โ†’ (๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ dom dom ๐‘€, ๐‘— โˆˆ dom dom ๐‘€ โ†ฆ ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜)))
5921, 58csbied 3927 . . . . . . 7 ((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ dom dom ๐‘€, ๐‘— โˆˆ dom dom ๐‘€ โ†ฆ ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜)))
6041, 59eqtr4d 2770 . . . . . 6 ((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ โฆ‹๐‘€ / ๐‘ฅโฆŒ(๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)) = โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜)))
6160adantr 480 . . . . 5 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ โฆ‹๐‘€ / ๐‘ฅโฆŒ(๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)) = โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜)))
6261mpteq2dv 5244 . . . 4 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ (๐‘˜ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘ฅโฆŒ(๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜))) = (๐‘˜ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜))))
6333, 62eqtrd 2767 . . 3 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€) = (๐‘˜ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜))))
64 oveq 7420 . . . . . . . . . . . 12 (๐‘š = ๐‘€ โ†’ (๐‘–๐‘š๐‘—) = (๐‘–๐‘€๐‘—))
6564adantl 481 . . . . . . . . . . 11 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘š = ๐‘€) โ†’ (๐‘–๐‘š๐‘—) = (๐‘–๐‘€๐‘—))
6665fveq2d 6895 . . . . . . . . . 10 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘š = ๐‘€) โ†’ (coe1โ€˜(๐‘–๐‘š๐‘—)) = (coe1โ€˜(๐‘–๐‘€๐‘—)))
6766fveq1d 6893 . . . . . . . . 9 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘š = ๐‘€) โ†’ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜) = ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜))
6867mpoeq3dv 7493 . . . . . . . 8 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘š = ๐‘€) โ†’ (๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜)))
6921, 68csbied 3927 . . . . . . 7 ((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜)))
7069ad2antrr 725 . . . . . 6 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โ†’ โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜)) = (๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜)))
71 pmatcollpw3.a . . . . . . 7 ๐ด = (๐‘ Mat ๐‘…)
72 eqid 2727 . . . . . . 7 (Baseโ€˜๐‘…) = (Baseโ€˜๐‘…)
73 pmatcollpw3.d . . . . . . 7 ๐ท = (Baseโ€˜๐ด)
74 simpll1 1210 . . . . . . 7 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โ†’ ๐‘ โˆˆ Fin)
75 simpll2 1211 . . . . . . 7 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โ†’ ๐‘… โˆˆ CRing)
76 simp2 1135 . . . . . . . . 9 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โˆง ๐‘– โˆˆ ๐‘ โˆง ๐‘— โˆˆ ๐‘) โ†’ ๐‘– โˆˆ ๐‘)
77 simp3 1136 . . . . . . . . 9 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โˆง ๐‘– โˆˆ ๐‘ โˆง ๐‘— โˆˆ ๐‘) โ†’ ๐‘— โˆˆ ๐‘)
7822adantr 480 . . . . . . . . . 10 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โ†’ ๐‘€ โˆˆ ๐ต)
79783ad2ant1 1131 . . . . . . . . 9 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โˆง ๐‘– โˆˆ ๐‘ โˆง ๐‘— โˆˆ ๐‘) โ†’ ๐‘€ โˆˆ ๐ต)
8042, 43, 44, 76, 77, 79matecld 22315 . . . . . . . 8 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โˆง ๐‘– โˆˆ ๐‘ โˆง ๐‘— โˆˆ ๐‘) โ†’ (๐‘–๐‘€๐‘—) โˆˆ (Baseโ€˜๐‘ƒ))
81 ssel 3971 . . . . . . . . . . 11 (๐ผ โІ โ„•0 โ†’ (๐‘˜ โˆˆ ๐ผ โ†’ ๐‘˜ โˆˆ โ„•0))
8281ad2antrl 727 . . . . . . . . . 10 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ (๐‘˜ โˆˆ ๐ผ โ†’ ๐‘˜ โˆˆ โ„•0))
8382imp 406 . . . . . . . . 9 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โ†’ ๐‘˜ โˆˆ โ„•0)
84833ad2ant1 1131 . . . . . . . 8 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โˆง ๐‘– โˆˆ ๐‘ โˆง ๐‘— โˆˆ ๐‘) โ†’ ๐‘˜ โˆˆ โ„•0)
85 eqid 2727 . . . . . . . . 9 (coe1โ€˜(๐‘–๐‘€๐‘—)) = (coe1โ€˜(๐‘–๐‘€๐‘—))
86 pmatcollpw.p . . . . . . . . 9 ๐‘ƒ = (Poly1โ€˜๐‘…)
8785, 43, 86, 72coe1fvalcl 22118 . . . . . . . 8 (((๐‘–๐‘€๐‘—) โˆˆ (Baseโ€˜๐‘ƒ) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜) โˆˆ (Baseโ€˜๐‘…))
8880, 84, 87syl2anc 583 . . . . . . 7 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โˆง ๐‘– โˆˆ ๐‘ โˆง ๐‘— โˆˆ ๐‘) โ†’ ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜) โˆˆ (Baseโ€˜๐‘…))
8971, 72, 73, 74, 75, 88matbas2d 22312 . . . . . 6 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โ†’ (๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘€๐‘—))โ€˜๐‘˜)) โˆˆ ๐ท)
9070, 89eqeltrd 2828 . . . . 5 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘˜ โˆˆ ๐ผ) โ†’ โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜)) โˆˆ ๐ท)
9190fmpttd 7119 . . . 4 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ (๐‘˜ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜))):๐ผโŸถ๐ท)
9273fvexi 6905 . . . . . 6 ๐ท โˆˆ V
9392a1i 11 . . . . 5 ((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐ท โˆˆ V)
9419adantr 480 . . . . 5 ((๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…) โ†’ ๐ผ โˆˆ V)
95 elmapg 8849 . . . . 5 ((๐ท โˆˆ V โˆง ๐ผ โˆˆ V) โ†’ ((๐‘˜ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜))) โˆˆ (๐ท โ†‘m ๐ผ) โ†” (๐‘˜ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜))):๐ผโŸถ๐ท))
9693, 94, 95syl2an 595 . . . 4 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ ((๐‘˜ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜))) โˆˆ (๐ท โ†‘m ๐ผ) โ†” (๐‘˜ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜))):๐ผโŸถ๐ท))
9791, 96mpbird 257 . . 3 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ (๐‘˜ โˆˆ ๐ผ โ†ฆ โฆ‹๐‘€ / ๐‘šโฆŒ(๐‘– โˆˆ ๐‘, ๐‘— โˆˆ ๐‘ โ†ฆ ((coe1โ€˜(๐‘–๐‘š๐‘—))โ€˜๐‘˜))) โˆˆ (๐ท โ†‘m ๐ผ))
9863, 97eqeltrd 2828 . 2 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€) โˆˆ (๐ท โ†‘m ๐ผ))
99 fveq1 6890 . . . . . . . . . . 11 (๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€) โ†’ (๐‘“โ€˜๐‘›) = ((curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)โ€˜๐‘›))
10099adantl 481 . . . . . . . . . 10 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โ†’ (๐‘“โ€˜๐‘›) = ((curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)โ€˜๐‘›))
101100adantr 480 . . . . . . . . 9 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘“โ€˜๐‘›) = ((curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)โ€˜๐‘›))
102 eqid 2727 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜))) = (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))
103 dmexg 7903 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ ๐ต โ†’ dom ๐‘ฅ โˆˆ V)
104103dmexd 7905 . . . . . . . . . . . . . . . 16 (๐‘ฅ โˆˆ ๐ต โ†’ dom dom ๐‘ฅ โˆˆ V)
105104, 104jca 511 . . . . . . . . . . . . . . 15 (๐‘ฅ โˆˆ ๐ต โ†’ (dom dom ๐‘ฅ โˆˆ V โˆง dom dom ๐‘ฅ โˆˆ V))
106105ad2antrl 727 . . . . . . . . . . . . . 14 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘› โˆˆ ๐ผ) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘˜ โˆˆ ๐ผ)) โ†’ (dom dom ๐‘ฅ โˆˆ V โˆง dom dom ๐‘ฅ โˆˆ V))
107 mpoexga 8076 . . . . . . . . . . . . . 14 ((dom dom ๐‘ฅ โˆˆ V โˆง dom dom ๐‘ฅ โˆˆ V) โ†’ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)) โˆˆ V)
108106, 107syl 17 . . . . . . . . . . . . 13 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘› โˆˆ ๐ผ) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘˜ โˆˆ ๐ผ)) โ†’ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)) โˆˆ V)
109108ralrimivva 3195 . . . . . . . . . . . 12 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘˜ โˆˆ ๐ผ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)) โˆˆ V)
11020adantr 480 . . . . . . . . . . . 12 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐ผ โˆˆ V)
11122adantr 480 . . . . . . . . . . . 12 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘€ โˆˆ ๐ต)
112 simpr 484 . . . . . . . . . . . 12 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ ๐ผ)
113102, 109, 110, 111, 112fvmpocurryd 8270 . . . . . . . . . . 11 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)โ€˜๐‘›) = (๐‘€(๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))๐‘›))
114 df-decpmat 22652 . . . . . . . . . . . . . 14 decompPMat = (๐‘ฅ โˆˆ V, ๐‘˜ โˆˆ โ„•0 โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))
115114reseq1i 5975 . . . . . . . . . . . . 13 ( decompPMat โ†พ (๐ต ร— ๐ผ)) = ((๐‘ฅ โˆˆ V, ๐‘˜ โˆˆ โ„•0 โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜))) โ†พ (๐ต ร— ๐ผ))
116 ssv 4002 . . . . . . . . . . . . . . . . 17 ๐ต โІ V
117116a1i 11 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐ต โІ V)
118 simpl 482 . . . . . . . . . . . . . . . 16 ((๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…) โ†’ ๐ผ โІ โ„•0)
119117, 118anim12i 612 . . . . . . . . . . . . . . 15 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ (๐ต โІ V โˆง ๐ผ โІ โ„•0))
120119adantr 480 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐ต โІ V โˆง ๐ผ โІ โ„•0))
121 resmpo 7534 . . . . . . . . . . . . . 14 ((๐ต โІ V โˆง ๐ผ โІ โ„•0) โ†’ ((๐‘ฅ โˆˆ V, ๐‘˜ โˆˆ โ„•0 โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜))) โ†พ (๐ต ร— ๐ผ)) = (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜))))
122120, 121syl 17 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ฅ โˆˆ V, ๐‘˜ โˆˆ โ„•0 โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜))) โ†พ (๐ต ร— ๐ผ)) = (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜))))
123115, 122eqtr2id 2780 . . . . . . . . . . . 12 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜))) = ( decompPMat โ†พ (๐ต ร— ๐ผ)))
124123oveqd 7431 . . . . . . . . . . 11 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘€(๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))๐‘›) = (๐‘€( decompPMat โ†พ (๐ต ร— ๐ผ))๐‘›))
125113, 124eqtrd 2767 . . . . . . . . . 10 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)โ€˜๐‘›) = (๐‘€( decompPMat โ†พ (๐ต ร— ๐ผ))๐‘›))
126125adantlr 714 . . . . . . . . 9 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)โ€˜๐‘›) = (๐‘€( decompPMat โ†พ (๐ต ร— ๐ผ))๐‘›))
127101, 126eqtrd 2767 . . . . . . . 8 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘“โ€˜๐‘›) = (๐‘€( decompPMat โ†พ (๐ต ร— ๐ผ))๐‘›))
128127fveq2d 6895 . . . . . . 7 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘‡โ€˜(๐‘“โ€˜๐‘›)) = (๐‘‡โ€˜(๐‘€( decompPMat โ†พ (๐ต ร— ๐ผ))๐‘›)))
12921ad2antrr 725 . . . . . . . . 9 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โ†’ ๐‘€ โˆˆ ๐ต)
130 ovres 7581 . . . . . . . . 9 ((๐‘€ โˆˆ ๐ต โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘€( decompPMat โ†พ (๐ต ร— ๐ผ))๐‘›) = (๐‘€ decompPMat ๐‘›))
131129, 130sylan 579 . . . . . . . 8 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘€( decompPMat โ†พ (๐ต ร— ๐ผ))๐‘›) = (๐‘€ decompPMat ๐‘›))
132131fveq2d 6895 . . . . . . 7 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘‡โ€˜(๐‘€( decompPMat โ†พ (๐ต ร— ๐ผ))๐‘›)) = (๐‘‡โ€˜(๐‘€ decompPMat ๐‘›)))
133128, 132eqtrd 2767 . . . . . 6 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘‡โ€˜(๐‘“โ€˜๐‘›)) = (๐‘‡โ€˜(๐‘€ decompPMat ๐‘›)))
134133oveq2d 7430 . . . . 5 (((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘› โ†‘ ๐‘‹) โˆ— (๐‘‡โ€˜(๐‘“โ€˜๐‘›))) = ((๐‘› โ†‘ ๐‘‹) โˆ— (๐‘‡โ€˜(๐‘€ decompPMat ๐‘›))))
135134mpteq2dva 5242 . . . 4 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โ†’ (๐‘› โˆˆ ๐ผ โ†ฆ ((๐‘› โ†‘ ๐‘‹) โˆ— (๐‘‡โ€˜(๐‘“โ€˜๐‘›)))) = (๐‘› โˆˆ ๐ผ โ†ฆ ((๐‘› โ†‘ ๐‘‹) โˆ— (๐‘‡โ€˜(๐‘€ decompPMat ๐‘›)))))
136135oveq2d 7430 . . 3 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โ†’ (๐ถ ฮฃg (๐‘› โˆˆ ๐ผ โ†ฆ ((๐‘› โ†‘ ๐‘‹) โˆ— (๐‘‡โ€˜(๐‘“โ€˜๐‘›))))) = (๐ถ ฮฃg (๐‘› โˆˆ ๐ผ โ†ฆ ((๐‘› โ†‘ ๐‘‹) โˆ— (๐‘‡โ€˜(๐‘€ decompPMat ๐‘›))))))
137136eqeq2d 2738 . 2 ((((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โˆง ๐‘“ = (curry (๐‘ฅ โˆˆ ๐ต, ๐‘˜ โˆˆ ๐ผ โ†ฆ (๐‘– โˆˆ dom dom ๐‘ฅ, ๐‘— โˆˆ dom dom ๐‘ฅ โ†ฆ ((coe1โ€˜(๐‘–๐‘ฅ๐‘—))โ€˜๐‘˜)))โ€˜๐‘€)) โ†’ (๐‘€ = (๐ถ ฮฃg (๐‘› โˆˆ ๐ผ โ†ฆ ((๐‘› โ†‘ ๐‘‹) โˆ— (๐‘‡โ€˜(๐‘“โ€˜๐‘›))))) โ†” ๐‘€ = (๐ถ ฮฃg (๐‘› โˆˆ ๐ผ โ†ฆ ((๐‘› โ†‘ ๐‘‹) โˆ— (๐‘‡โ€˜(๐‘€ decompPMat ๐‘›)))))))
13898, 137rspcedv 3600 1 (((๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง (๐ผ โІ โ„•0 โˆง ๐ผ โ‰  โˆ…)) โ†’ (๐‘€ = (๐ถ ฮฃg (๐‘› โˆˆ ๐ผ โ†ฆ ((๐‘› โ†‘ ๐‘‹) โˆ— (๐‘‡โ€˜(๐‘€ decompPMat ๐‘›))))) โ†’ โˆƒ๐‘“ โˆˆ (๐ท โ†‘m ๐ผ)๐‘€ = (๐ถ ฮฃg (๐‘› โˆˆ ๐ผ โ†ฆ ((๐‘› โ†‘ ๐‘‹) โˆ— (๐‘‡โ€˜(๐‘“โ€˜๐‘›)))))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆง w3a 1085   = wceq 1534   โˆˆ wcel 2099   โ‰  wne 2935  โˆƒwrex 3065  Vcvv 3469  โฆ‹csb 3889   โІ wss 3944  โˆ…c0 4318   โ†ฆ cmpt 5225   ร— cxp 5670  dom cdm 5672   โ†พ cres 5674  โŸถwf 6538  โ€˜cfv 6542  (class class class)co 7414   โˆˆ cmpo 7416  curry ccur 8264   โ†‘m cmap 8836  Fincfn 8955  โ„•0cn0 12494  Basecbs 17171   ยท๐‘  cvsca 17228   ฮฃg cgsu 17413  .gcmg 19014  mulGrpcmgp 20065  CRingccrg 20165  var1cv1 22082  Poly1cpl1 22083  coe1cco1 22084   Mat cmat 22294   matToPolyMat cmat2pmat 22593   decompPMat cdecpmat 22651
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-ot 4633  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-cur 8266  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-map 8838  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-sup 9457  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-z 12581  df-dec 12700  df-uz 12845  df-fz 13509  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-hom 17248  df-cco 17249  df-0g 17414  df-prds 17420  df-pws 17422  df-sra 21047  df-rgmod 21048  df-dsmm 21653  df-frlm 21668  df-psr 21829  df-opsr 21833  df-psr1 22086  df-ply1 22088  df-coe1 22089  df-mat 22295  df-decpmat 22652
This theorem is referenced by:  pmatcollpw3  22673  pmatcollpw3fi  22674
  Copyright terms: Public domain W3C validator