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

Theorem pmatcollpw3lem 21527
Description: Lemma for pmatcollpw3 21528 and pmatcollpw3fi 21529: 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 5740 . . . . . . . . 9 (𝑥 = 𝑦 → dom 𝑥 = dom 𝑦)
21dmeqd 5742 . . . . . . . 8 (𝑥 = 𝑦 → dom dom 𝑥 = dom dom 𝑦)
3 oveq 7170 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑖𝑥𝑗) = (𝑖𝑦𝑗))
43fveq2d 6672 . . . . . . . . 9 (𝑥 = 𝑦 → (coe1‘(𝑖𝑥𝑗)) = (coe1‘(𝑖𝑦𝑗)))
54fveq1d 6670 . . . . . . . 8 (𝑥 = 𝑦 → ((coe1‘(𝑖𝑥𝑗))‘𝑘) = ((coe1‘(𝑖𝑦𝑗))‘𝑘))
62, 2, 5mpoeq123dv 7237 . . . . . . 7 (𝑥 = 𝑦 → (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)) = (𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑘)))
7 fveq2 6668 . . . . . . . 8 (𝑘 = 𝑙 → ((coe1‘(𝑖𝑦𝑗))‘𝑘) = ((coe1‘(𝑖𝑦𝑗))‘𝑙))
87mpoeq3dv 7241 . . . . . . 7 (𝑘 = 𝑙 → (𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑘)) = (𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑙)))
96, 8cbvmpov 7257 . . . . . 6 (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘))) = (𝑦𝐵, 𝑙𝐼 ↦ (𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑙)))
10 dmexg 7627 . . . . . . . . . . 11 (𝑦𝐵 → dom 𝑦 ∈ V)
1110dmexd 7629 . . . . . . . . . 10 (𝑦𝐵 → dom dom 𝑦 ∈ V)
1211, 11jca 515 . . . . . . . . 9 (𝑦𝐵 → (dom dom 𝑦 ∈ V ∧ dom dom 𝑦 ∈ V))
1312ad2antrl 728 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ (𝑦𝐵𝑙𝐼)) → (dom dom 𝑦 ∈ V ∧ dom dom 𝑦 ∈ V))
14 mpoexga 7794 . . . . . . . 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 3103 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → ∀𝑦𝐵𝑙𝐼 (𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑙)) ∈ V)
17 simprr 773 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → 𝐼 ≠ ∅)
18 nn0ex 11975 . . . . . . . 8 0 ∈ V
1918ssex 5186 . . . . . . 7 (𝐼 ⊆ ℕ0𝐼 ∈ V)
2019ad2antrl 728 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → 𝐼 ∈ V)
21 simp3 1139 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑀𝐵)
2221adantr 484 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → 𝑀𝐵)
239, 16, 17, 20, 22mpocurryvald 7958 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀) = (𝑙𝐼𝑀 / 𝑦(𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑙))))
24 fveq2 6668 . . . . . . . . 9 (𝑙 = 𝑘 → ((coe1‘(𝑖𝑦𝑗))‘𝑙) = ((coe1‘(𝑖𝑦𝑗))‘𝑘))
2524mpoeq3dv 7241 . . . . . . . 8 (𝑙 = 𝑘 → (𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑙)) = (𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑘)))
2625csbeq2dv 3795 . . . . . . 7 (𝑙 = 𝑘𝑀 / 𝑦(𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑙)) = 𝑀 / 𝑦(𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑘)))
27 eqcom 2745 . . . . . . . . 9 (𝑥 = 𝑦𝑦 = 𝑥)
28 eqcom 2745 . . . . . . . . 9 ((𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)) = (𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑘)) ↔ (𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑘)) = (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))
296, 27, 283imtr3i 294 . . . . . . . 8 (𝑦 = 𝑥 → (𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑘)) = (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))
3029cbvcsbv 3800 . . . . . . 7 𝑀 / 𝑦(𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑘)) = 𝑀 / 𝑥(𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘))
3126, 30eqtrdi 2789 . . . . . 6 (𝑙 = 𝑘𝑀 / 𝑦(𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑙)) = 𝑀 / 𝑥(𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))
3231cbvmptv 5130 . . . . 5 (𝑙𝐼𝑀 / 𝑦(𝑖 ∈ dom dom 𝑦, 𝑗 ∈ dom dom 𝑦 ↦ ((coe1‘(𝑖𝑦𝑗))‘𝑙))) = (𝑘𝐼𝑀 / 𝑥(𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))
3323, 32eqtrdi 2789 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀) = (𝑘𝐼𝑀 / 𝑥(𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘))))
34 dmeq 5740 . . . . . . . . . . 11 (𝑥 = 𝑀 → dom 𝑥 = dom 𝑀)
3534dmeqd 5742 . . . . . . . . . 10 (𝑥 = 𝑀 → dom dom 𝑥 = dom dom 𝑀)
36 oveq 7170 . . . . . . . . . . . 12 (𝑥 = 𝑀 → (𝑖𝑥𝑗) = (𝑖𝑀𝑗))
3736fveq2d 6672 . . . . . . . . . . 11 (𝑥 = 𝑀 → (coe1‘(𝑖𝑥𝑗)) = (coe1‘(𝑖𝑀𝑗)))
3837fveq1d 6670 . . . . . . . . . 10 (𝑥 = 𝑀 → ((coe1‘(𝑖𝑥𝑗))‘𝑘) = ((coe1‘(𝑖𝑀𝑗))‘𝑘))
3935, 35, 38mpoeq123dv 7237 . . . . . . . . 9 (𝑥 = 𝑀 → (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)) = (𝑖 ∈ dom dom 𝑀, 𝑗 ∈ dom dom 𝑀 ↦ ((coe1‘(𝑖𝑀𝑗))‘𝑘)))
4039adantl 485 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑥 = 𝑀) → (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)) = (𝑖 ∈ dom dom 𝑀, 𝑗 ∈ dom dom 𝑀 ↦ ((coe1‘(𝑖𝑀𝑗))‘𝑘)))
4121, 40csbied 3824 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑀 / 𝑥(𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)) = (𝑖 ∈ dom dom 𝑀, 𝑗 ∈ dom dom 𝑀 ↦ ((coe1‘(𝑖𝑀𝑗))‘𝑘)))
42 pmatcollpw.c . . . . . . . . . . . . 13 𝐶 = (𝑁 Mat 𝑃)
43 eqid 2738 . . . . . . . . . . . . 13 (Base‘𝑃) = (Base‘𝑃)
44 pmatcollpw.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝐶)
4542, 43, 44matbas2i 21166 . . . . . . . . . . . 12 (𝑀𝐵𝑀 ∈ ((Base‘𝑃) ↑m (𝑁 × 𝑁)))
46 elmapi 8452 . . . . . . . . . . . 12 (𝑀 ∈ ((Base‘𝑃) ↑m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑃))
47 fdm 6507 . . . . . . . . . . . . . 14 (𝑀:(𝑁 × 𝑁)⟶(Base‘𝑃) → dom 𝑀 = (𝑁 × 𝑁))
4847dmeqd 5742 . . . . . . . . . . . . 13 (𝑀:(𝑁 × 𝑁)⟶(Base‘𝑃) → dom dom 𝑀 = dom (𝑁 × 𝑁))
49 dmxpid 5767 . . . . . . . . . . . . 13 dom (𝑁 × 𝑁) = 𝑁
5048, 49eqtr2di 2790 . . . . . . . . . . . 12 (𝑀:(𝑁 × 𝑁)⟶(Base‘𝑃) → 𝑁 = dom dom 𝑀)
5145, 46, 503syl 18 . . . . . . . . . . 11 (𝑀𝐵𝑁 = dom dom 𝑀)
52513ad2ant3 1136 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑁 = dom dom 𝑀)
5352adantr 484 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑚 = 𝑀) → 𝑁 = dom dom 𝑀)
54 simpr 488 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑚 = 𝑀) → 𝑚 = 𝑀)
5554oveqd 7181 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑚 = 𝑀) → (𝑖𝑚𝑗) = (𝑖𝑀𝑗))
5655fveq2d 6672 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑚 = 𝑀) → (coe1‘(𝑖𝑚𝑗)) = (coe1‘(𝑖𝑀𝑗)))
5756fveq1d 6670 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑚 = 𝑀) → ((coe1‘(𝑖𝑚𝑗))‘𝑘) = ((coe1‘(𝑖𝑀𝑗))‘𝑘))
5853, 53, 57mpoeq123dv 7237 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑚 = 𝑀) → (𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)) = (𝑖 ∈ dom dom 𝑀, 𝑗 ∈ dom dom 𝑀 ↦ ((coe1‘(𝑖𝑀𝑗))‘𝑘)))
5921, 58csbied 3824 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)) = (𝑖 ∈ dom dom 𝑀, 𝑗 ∈ dom dom 𝑀 ↦ ((coe1‘(𝑖𝑀𝑗))‘𝑘)))
6041, 59eqtr4d 2776 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑀 / 𝑥(𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)) = 𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)))
6160adantr 484 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → 𝑀 / 𝑥(𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)) = 𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)))
6261mpteq2dv 5123 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → (𝑘𝐼𝑀 / 𝑥(𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘))) = (𝑘𝐼𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘))))
6333, 62eqtrd 2773 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀) = (𝑘𝐼𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘))))
64 oveq 7170 . . . . . . . . . . . 12 (𝑚 = 𝑀 → (𝑖𝑚𝑗) = (𝑖𝑀𝑗))
6564adantl 485 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑚 = 𝑀) → (𝑖𝑚𝑗) = (𝑖𝑀𝑗))
6665fveq2d 6672 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑚 = 𝑀) → (coe1‘(𝑖𝑚𝑗)) = (coe1‘(𝑖𝑀𝑗)))
6766fveq1d 6670 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑚 = 𝑀) → ((coe1‘(𝑖𝑚𝑗))‘𝑘) = ((coe1‘(𝑖𝑀𝑗))‘𝑘))
6867mpoeq3dv 7241 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑚 = 𝑀) → (𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)) = (𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑀𝑗))‘𝑘)))
6921, 68csbied 3824 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)) = (𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑀𝑗))‘𝑘)))
7069ad2antrr 726 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) → 𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)) = (𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑀𝑗))‘𝑘)))
71 pmatcollpw3.a . . . . . . 7 𝐴 = (𝑁 Mat 𝑅)
72 eqid 2738 . . . . . . 7 (Base‘𝑅) = (Base‘𝑅)
73 pmatcollpw3.d . . . . . . 7 𝐷 = (Base‘𝐴)
74 simpll1 1213 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) → 𝑁 ∈ Fin)
75 simpll2 1214 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) → 𝑅 ∈ CRing)
76 simp2 1138 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) ∧ 𝑖𝑁𝑗𝑁) → 𝑖𝑁)
77 simp3 1139 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) ∧ 𝑖𝑁𝑗𝑁) → 𝑗𝑁)
7822adantr 484 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) → 𝑀𝐵)
79783ad2ant1 1134 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) ∧ 𝑖𝑁𝑗𝑁) → 𝑀𝐵)
8042, 43, 44, 76, 77, 79matecld 21170 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) ∧ 𝑖𝑁𝑗𝑁) → (𝑖𝑀𝑗) ∈ (Base‘𝑃))
81 ssel 3868 . . . . . . . . . . 11 (𝐼 ⊆ ℕ0 → (𝑘𝐼𝑘 ∈ ℕ0))
8281ad2antrl 728 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → (𝑘𝐼𝑘 ∈ ℕ0))
8382imp 410 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) → 𝑘 ∈ ℕ0)
84833ad2ant1 1134 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) ∧ 𝑖𝑁𝑗𝑁) → 𝑘 ∈ ℕ0)
85 eqid 2738 . . . . . . . . 9 (coe1‘(𝑖𝑀𝑗)) = (coe1‘(𝑖𝑀𝑗))
86 pmatcollpw.p . . . . . . . . 9 𝑃 = (Poly1𝑅)
8785, 43, 86, 72coe1fvalcl 20980 . . . . . . . 8 (((𝑖𝑀𝑗) ∈ (Base‘𝑃) ∧ 𝑘 ∈ ℕ0) → ((coe1‘(𝑖𝑀𝑗))‘𝑘) ∈ (Base‘𝑅))
8880, 84, 87syl2anc 587 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) ∧ 𝑖𝑁𝑗𝑁) → ((coe1‘(𝑖𝑀𝑗))‘𝑘) ∈ (Base‘𝑅))
8971, 72, 73, 74, 75, 88matbas2d 21167 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) → (𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑀𝑗))‘𝑘)) ∈ 𝐷)
9070, 89eqeltrd 2833 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑘𝐼) → 𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)) ∈ 𝐷)
9190fmpttd 6883 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → (𝑘𝐼𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘))):𝐼𝐷)
9273fvexi 6682 . . . . . 6 𝐷 ∈ V
9392a1i 11 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝐷 ∈ V)
9419adantr 484 . . . . 5 ((𝐼 ⊆ ℕ0𝐼 ≠ ∅) → 𝐼 ∈ V)
95 elmapg 8443 . . . . 5 ((𝐷 ∈ V ∧ 𝐼 ∈ V) → ((𝑘𝐼𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘))) ∈ (𝐷m 𝐼) ↔ (𝑘𝐼𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘))):𝐼𝐷))
9693, 94, 95syl2an 599 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → ((𝑘𝐼𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘))) ∈ (𝐷m 𝐼) ↔ (𝑘𝐼𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘))):𝐼𝐷))
9791, 96mpbird 260 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → (𝑘𝐼𝑀 / 𝑚(𝑖𝑁, 𝑗𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘))) ∈ (𝐷m 𝐼))
9863, 97eqeltrd 2833 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀) ∈ (𝐷m 𝐼))
99 fveq1 6667 . . . . . . . . . . 11 (𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀) → (𝑓𝑛) = ((curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)‘𝑛))
10099adantl 485 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) → (𝑓𝑛) = ((curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)‘𝑛))
101100adantr 484 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) ∧ 𝑛𝐼) → (𝑓𝑛) = ((curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)‘𝑛))
102 eqid 2738 . . . . . . . . . . . 12 (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘))) = (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))
103 dmexg 7627 . . . . . . . . . . . . . . . . 17 (𝑥𝐵 → dom 𝑥 ∈ V)
104103dmexd 7629 . . . . . . . . . . . . . . . 16 (𝑥𝐵 → dom dom 𝑥 ∈ V)
105104, 104jca 515 . . . . . . . . . . . . . . 15 (𝑥𝐵 → (dom dom 𝑥 ∈ V ∧ dom dom 𝑥 ∈ V))
106105ad2antrl 728 . . . . . . . . . . . . . 14 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑛𝐼) ∧ (𝑥𝐵𝑘𝐼)) → (dom dom 𝑥 ∈ V ∧ dom dom 𝑥 ∈ V))
107 mpoexga 7794 . . . . . . . . . . . . . 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 3103 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑛𝐼) → ∀𝑥𝐵𝑘𝐼 (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)) ∈ V)
11020adantr 484 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑛𝐼) → 𝐼 ∈ V)
11122adantr 484 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑛𝐼) → 𝑀𝐵)
112 simpr 488 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑛𝐼) → 𝑛𝐼)
113102, 109, 110, 111, 112fvmpocurryd 7959 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑛𝐼) → ((curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)‘𝑛) = (𝑀(𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))𝑛))
114 df-decpmat 21507 . . . . . . . . . . . . . 14 decompPMat = (𝑥 ∈ V, 𝑘 ∈ ℕ0 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))
115114reseq1i 5815 . . . . . . . . . . . . 13 ( decompPMat ↾ (𝐵 × 𝐼)) = ((𝑥 ∈ V, 𝑘 ∈ ℕ0 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘))) ↾ (𝐵 × 𝐼))
116 ssv 3899 . . . . . . . . . . . . . . . . 17 𝐵 ⊆ V
117116a1i 11 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝐵 ⊆ V)
118 simpl 486 . . . . . . . . . . . . . . . 16 ((𝐼 ⊆ ℕ0𝐼 ≠ ∅) → 𝐼 ⊆ ℕ0)
119117, 118anim12i 616 . . . . . . . . . . . . . . 15 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → (𝐵 ⊆ V ∧ 𝐼 ⊆ ℕ0))
120119adantr 484 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑛𝐼) → (𝐵 ⊆ V ∧ 𝐼 ⊆ ℕ0))
121 resmpo 7280 . . . . . . . . . . . . . 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 2786 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑛𝐼) → (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘))) = ( decompPMat ↾ (𝐵 × 𝐼)))
124123oveqd 7181 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑛𝐼) → (𝑀(𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))𝑛) = (𝑀( decompPMat ↾ (𝐵 × 𝐼))𝑛))
125113, 124eqtrd 2773 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑛𝐼) → ((curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)‘𝑛) = (𝑀( decompPMat ↾ (𝐵 × 𝐼))𝑛))
126125adantlr 715 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) ∧ 𝑛𝐼) → ((curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)‘𝑛) = (𝑀( decompPMat ↾ (𝐵 × 𝐼))𝑛))
127101, 126eqtrd 2773 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) ∧ 𝑛𝐼) → (𝑓𝑛) = (𝑀( decompPMat ↾ (𝐵 × 𝐼))𝑛))
128127fveq2d 6672 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) ∧ 𝑛𝐼) → (𝑇‘(𝑓𝑛)) = (𝑇‘(𝑀( decompPMat ↾ (𝐵 × 𝐼))𝑛)))
12921ad2antrr 726 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) → 𝑀𝐵)
130 ovres 7324 . . . . . . . . 9 ((𝑀𝐵𝑛𝐼) → (𝑀( decompPMat ↾ (𝐵 × 𝐼))𝑛) = (𝑀 decompPMat 𝑛))
131129, 130sylan 583 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) ∧ 𝑛𝐼) → (𝑀( decompPMat ↾ (𝐵 × 𝐼))𝑛) = (𝑀 decompPMat 𝑛))
132131fveq2d 6672 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) ∧ 𝑛𝐼) → (𝑇‘(𝑀( decompPMat ↾ (𝐵 × 𝐼))𝑛)) = (𝑇‘(𝑀 decompPMat 𝑛)))
133128, 132eqtrd 2773 . . . . . 6 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) ∧ 𝑛𝐼) → (𝑇‘(𝑓𝑛)) = (𝑇‘(𝑀 decompPMat 𝑛)))
134133oveq2d 7180 . . . . 5 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) ∧ 𝑛𝐼) → ((𝑛 𝑋) (𝑇‘(𝑓𝑛))) = ((𝑛 𝑋) (𝑇‘(𝑀 decompPMat 𝑛))))
135134mpteq2dva 5122 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) → (𝑛𝐼 ↦ ((𝑛 𝑋) (𝑇‘(𝑓𝑛)))) = (𝑛𝐼 ↦ ((𝑛 𝑋) (𝑇‘(𝑀 decompPMat 𝑛)))))
136135oveq2d 7180 . . 3 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) → (𝐶 Σg (𝑛𝐼 ↦ ((𝑛 𝑋) (𝑇‘(𝑓𝑛))))) = (𝐶 Σg (𝑛𝐼 ↦ ((𝑛 𝑋) (𝑇‘(𝑀 decompPMat 𝑛))))))
137136eqeq2d 2749 . 2 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) ∧ 𝑓 = (curry (𝑥𝐵, 𝑘𝐼 ↦ (𝑖 ∈ dom dom 𝑥, 𝑗 ∈ dom dom 𝑥 ↦ ((coe1‘(𝑖𝑥𝑗))‘𝑘)))‘𝑀)) → (𝑀 = (𝐶 Σg (𝑛𝐼 ↦ ((𝑛 𝑋) (𝑇‘(𝑓𝑛))))) ↔ 𝑀 = (𝐶 Σg (𝑛𝐼 ↦ ((𝑛 𝑋) (𝑇‘(𝑀 decompPMat 𝑛)))))))
13898, 137rspcedv 3517 1 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝐼 ⊆ ℕ0𝐼 ≠ ∅)) → (𝑀 = (𝐶 Σg (𝑛𝐼 ↦ ((𝑛 𝑋) (𝑇‘(𝑀 decompPMat 𝑛))))) → ∃𝑓 ∈ (𝐷m 𝐼)𝑀 = (𝐶 Σg (𝑛𝐼 ↦ ((𝑛 𝑋) (𝑇‘(𝑓𝑛)))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1088   = wceq 1542  wcel 2113  wne 2934  wrex 3054  Vcvv 3397  csb 3788  wss 3841  c0 4209  cmpt 5107   × cxp 5517  dom cdm 5519  cres 5521  wf 6329  cfv 6333  (class class class)co 7164  cmpo 7166  curry ccur 7953  m cmap 8430  Fincfn 8548  0cn0 11969  Basecbs 16579   ·𝑠 cvsca 16665   Σg cgsu 16810  .gcmg 18335  mulGrpcmgp 19351  CRingccrg 19410  var1cv1 20944  Poly1cpl1 20945  coe1cco1 20946   Mat cmat 21151   matToPolyMat cmat2pmat 21448   decompPMat cdecpmat 21506
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-cnex 10664  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684  ax-pre-mulgt0 10685
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-ot 4522  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-of 7419  df-om 7594  df-1st 7707  df-2nd 7708  df-supp 7850  df-cur 7955  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-1o 8124  df-er 8313  df-map 8432  df-ixp 8501  df-en 8549  df-dom 8550  df-sdom 8551  df-fin 8552  df-fsupp 8900  df-sup 8972  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752  df-sub 10943  df-neg 10944  df-nn 11710  df-2 11772  df-3 11773  df-4 11774  df-5 11775  df-6 11776  df-7 11777  df-8 11778  df-9 11779  df-n0 11970  df-z 12056  df-dec 12173  df-uz 12318  df-fz 12975  df-struct 16581  df-ndx 16582  df-slot 16583  df-base 16585  df-sets 16586  df-ress 16587  df-plusg 16674  df-mulr 16675  df-sca 16677  df-vsca 16678  df-ip 16679  df-tset 16680  df-ple 16681  df-ds 16683  df-hom 16685  df-cco 16686  df-0g 16811  df-prds 16817  df-pws 16819  df-sra 20056  df-rgmod 20057  df-dsmm 20541  df-frlm 20556  df-psr 20715  df-opsr 20719  df-psr1 20948  df-ply1 20950  df-coe1 20951  df-mat 21152  df-decpmat 21507
This theorem is referenced by:  pmatcollpw3  21528  pmatcollpw3fi  21529
  Copyright terms: Public domain W3C validator