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

Theorem m2cpminvid2lem 22010
Description: Lemma for m2cpminvid2 22011. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.)
Hypotheses
Ref Expression
m2cpminvid2lem.s 𝑆 = (𝑁 ConstPolyMat 𝑅)
m2cpminvid2lem.p 𝑃 = (Poly1𝑅)
Assertion
Ref Expression
m2cpminvid2lem (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → ∀𝑛 ∈ ℕ0 ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))
Distinct variable groups:   𝑛,𝑀   𝑛,𝑁   𝑃,𝑛   𝑅,𝑛   𝑆,𝑛   𝑥,𝑛   𝑦,𝑛
Allowed substitution hints:   𝑃(𝑥,𝑦)   𝑅(𝑥,𝑦)   𝑆(𝑥,𝑦)   𝑀(𝑥,𝑦)   𝑁(𝑥,𝑦)

Proof of Theorem m2cpminvid2lem
Dummy variables 𝑖 𝑗 𝑘 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 m2cpminvid2lem.s . . . . . . . 8 𝑆 = (𝑁 ConstPolyMat 𝑅)
2 m2cpminvid2lem.p . . . . . . . 8 𝑃 = (Poly1𝑅)
3 eqid 2736 . . . . . . . 8 (𝑁 Mat 𝑃) = (𝑁 Mat 𝑃)
4 eqid 2736 . . . . . . . 8 (Base‘(𝑁 Mat 𝑃)) = (Base‘(𝑁 Mat 𝑃))
51, 2, 3, 4cpmatelimp 21968 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀𝑆 → (𝑀 ∈ (Base‘(𝑁 Mat 𝑃)) ∧ ∀𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g𝑅))))
653impia 1116 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) → (𝑀 ∈ (Base‘(𝑁 Mat 𝑃)) ∧ ∀𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g𝑅)))
76simprd 496 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) → ∀𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g𝑅))
87adantr 481 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → ∀𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g𝑅))
9 fvoveq1 7361 . . . . . . . . . 10 (𝑖 = 𝑥 → (coe1‘(𝑖𝑀𝑗)) = (coe1‘(𝑥𝑀𝑗)))
109fveq1d 6828 . . . . . . . . 9 (𝑖 = 𝑥 → ((coe1‘(𝑖𝑀𝑗))‘𝑘) = ((coe1‘(𝑥𝑀𝑗))‘𝑘))
1110eqeq1d 2738 . . . . . . . 8 (𝑖 = 𝑥 → (((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g𝑅) ↔ ((coe1‘(𝑥𝑀𝑗))‘𝑘) = (0g𝑅)))
1211ralbidv 3170 . . . . . . 7 (𝑖 = 𝑥 → (∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g𝑅) ↔ ∀𝑘 ∈ ℕ ((coe1‘(𝑥𝑀𝑗))‘𝑘) = (0g𝑅)))
13 oveq2 7346 . . . . . . . . . . 11 (𝑗 = 𝑦 → (𝑥𝑀𝑗) = (𝑥𝑀𝑦))
1413fveq2d 6830 . . . . . . . . . 10 (𝑗 = 𝑦 → (coe1‘(𝑥𝑀𝑗)) = (coe1‘(𝑥𝑀𝑦)))
1514fveq1d 6828 . . . . . . . . 9 (𝑗 = 𝑦 → ((coe1‘(𝑥𝑀𝑗))‘𝑘) = ((coe1‘(𝑥𝑀𝑦))‘𝑘))
1615eqeq1d 2738 . . . . . . . 8 (𝑗 = 𝑦 → (((coe1‘(𝑥𝑀𝑗))‘𝑘) = (0g𝑅) ↔ ((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g𝑅)))
1716ralbidv 3170 . . . . . . 7 (𝑗 = 𝑦 → (∀𝑘 ∈ ℕ ((coe1‘(𝑥𝑀𝑗))‘𝑘) = (0g𝑅) ↔ ∀𝑘 ∈ ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g𝑅)))
1812, 17rspc2v 3579 . . . . . 6 ((𝑥𝑁𝑦𝑁) → (∀𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g𝑅) → ∀𝑘 ∈ ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g𝑅)))
1918adantl 482 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → (∀𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g𝑅) → ∀𝑘 ∈ ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g𝑅)))
20 fveqeq2 6835 . . . . . . 7 (𝑘 = 𝑛 → (((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g𝑅) ↔ ((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g𝑅)))
2120cbvralvw 3221 . . . . . 6 (∀𝑘 ∈ ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g𝑅) ↔ ∀𝑛 ∈ ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g𝑅))
22 simpl2 1191 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → 𝑅 ∈ Ring)
23 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (Base‘𝑃) = (Base‘𝑃)
24 simprl 768 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → 𝑥𝑁)
25 simprr 770 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → 𝑦𝑁)
261, 2, 3, 4cpmatpmat 21966 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) → 𝑀 ∈ (Base‘(𝑁 Mat 𝑃)))
2726adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → 𝑀 ∈ (Base‘(𝑁 Mat 𝑃)))
283, 23, 4, 24, 25, 27matecld 21682 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → (𝑥𝑀𝑦) ∈ (Base‘𝑃))
29 0nn0 12350 . . . . . . . . . . . . . . . . . 18 0 ∈ ℕ0
30 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (coe1‘(𝑥𝑀𝑦)) = (coe1‘(𝑥𝑀𝑦))
31 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (Base‘𝑅) = (Base‘𝑅)
3230, 23, 2, 31coe1fvalcl 21490 . . . . . . . . . . . . . . . . . 18 (((𝑥𝑀𝑦) ∈ (Base‘𝑃) ∧ 0 ∈ ℕ0) → ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅))
3328, 29, 32sylancl 586 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅))
3422, 33jca 512 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → (𝑅 ∈ Ring ∧ ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)))
3534adantr 481 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) → (𝑅 ∈ Ring ∧ ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)))
36 eqid 2736 . . . . . . . . . . . . . . . 16 (algSc‘𝑃) = (algSc‘𝑃)
37 eqid 2736 . . . . . . . . . . . . . . . 16 (0g𝑅) = (0g𝑅)
382, 36, 31, 37coe1scl 21565 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) → (coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅))))
3935, 38syl 17 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) → (coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅))))
4039fveq1d 6828 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) → ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅)))‘𝑛))
41 eqidd 2737 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) → (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅))))
42 eqeq1 2740 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑛 → (𝑙 = 0 ↔ 𝑛 = 0))
4342ifbid 4497 . . . . . . . . . . . . . . 15 (𝑙 = 𝑛 → if(𝑙 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅)) = if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅)))
4443adantl 482 . . . . . . . . . . . . . 14 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅)) = if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅)))
45 nnnn0 12342 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
4645adantl 482 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
47 fvex 6839 . . . . . . . . . . . . . . . 16 ((coe1‘(𝑥𝑀𝑦))‘0) ∈ V
48 fvex 6839 . . . . . . . . . . . . . . . 16 (0g𝑅) ∈ V
4947, 48ifex 4524 . . . . . . . . . . . . . . 15 if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅)) ∈ V
5049a1i 11 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅)) ∈ V)
5141, 44, 46, 50fvmptd 6939 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) → ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅)))‘𝑛) = if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅)))
52 nnne0 12109 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
5352neneqd 2945 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ¬ 𝑛 = 0)
5453adantl 482 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0)
5554iffalsed 4485 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g𝑅)) = (0g𝑅))
5640, 51, 553eqtrd 2780 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) → ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = (0g𝑅))
57 eqcom 2743 . . . . . . . . . . . . 13 (((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g𝑅) ↔ (0g𝑅) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))
5857biimpi 215 . . . . . . . . . . . 12 (((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g𝑅) → (0g𝑅) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))
5956, 58sylan9eq 2796 . . . . . . . . . . 11 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) ∧ ((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g𝑅)) → ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))
6059ex 413 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ 𝑛 ∈ ℕ) → (((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g𝑅) → ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)))
6160ralimdva 3160 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → (∀𝑛 ∈ ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g𝑅) → ∀𝑛 ∈ ℕ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)))
6261imp 407 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ ∀𝑛 ∈ ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g𝑅)) → ∀𝑛 ∈ ℕ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))
6334adantr 481 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ ∀𝑛 ∈ ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g𝑅)) → (𝑅 ∈ Ring ∧ ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)))
642, 36, 31ply1sclid 21566 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) → ((coe1‘(𝑥𝑀𝑦))‘0) = ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0))
6564eqcomd 2742 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) → ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) = ((coe1‘(𝑥𝑀𝑦))‘0))
6663, 65syl 17 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ ∀𝑛 ∈ ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g𝑅)) → ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) = ((coe1‘(𝑥𝑀𝑦))‘0))
6762, 66jca 512 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) ∧ ∀𝑛 ∈ ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g𝑅)) → (∀𝑛 ∈ ℕ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) = ((coe1‘(𝑥𝑀𝑦))‘0)))
6867ex 413 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → (∀𝑛 ∈ ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g𝑅) → (∀𝑛 ∈ ℕ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) = ((coe1‘(𝑥𝑀𝑦))‘0))))
6921, 68biimtrid 241 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → (∀𝑘 ∈ ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g𝑅) → (∀𝑛 ∈ ℕ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) = ((coe1‘(𝑥𝑀𝑦))‘0))))
7019, 69syld 47 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → (∀𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g𝑅) → (∀𝑛 ∈ ℕ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) = ((coe1‘(𝑥𝑀𝑦))‘0))))
718, 70mpd 15 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → (∀𝑛 ∈ ℕ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) = ((coe1‘(𝑥𝑀𝑦))‘0)))
72 c0ex 11071 . . . 4 0 ∈ V
73 fveq2 6826 . . . . . 6 (𝑛 = 0 → ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0))
74 fveq2 6826 . . . . . 6 (𝑛 = 0 → ((coe1‘(𝑥𝑀𝑦))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘0))
7573, 74eqeq12d 2752 . . . . 5 (𝑛 = 0 → (((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) = ((coe1‘(𝑥𝑀𝑦))‘0)))
7675ralunsn 4839 . . . 4 (0 ∈ V → (∀𝑛 ∈ (ℕ ∪ {0})((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔ (∀𝑛 ∈ ℕ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) = ((coe1‘(𝑥𝑀𝑦))‘0))))
7772, 76mp1i 13 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → (∀𝑛 ∈ (ℕ ∪ {0})((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔ (∀𝑛 ∈ ℕ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧ ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) = ((coe1‘(𝑥𝑀𝑦))‘0))))
7871, 77mpbird 256 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → ∀𝑛 ∈ (ℕ ∪ {0})((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))
79 df-n0 12336 . . 3 0 = (ℕ ∪ {0})
8079raleqi 3307 . 2 (∀𝑛 ∈ ℕ0 ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔ ∀𝑛 ∈ (ℕ ∪ {0})((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))
8178, 80sylibr 233 1 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆) ∧ (𝑥𝑁𝑦𝑁)) → ∀𝑛 ∈ ℕ0 ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  wral 3061  Vcvv 3441  cun 3896  ifcif 4474  {csn 4574  cmpt 5176  cfv 6480  (class class class)co 7338  Fincfn 8805  0cc0 10973  cn 12075  0cn0 12335  Basecbs 17010  0gc0g 17248  Ringcrg 19879  algSccascl 21166  Poly1cpl1 21455  coe1cco1 21456   Mat cmat 21661   ConstPolyMat ccpmat 21959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-tp 4579  df-op 4581  df-ot 4583  df-uni 4854  df-int 4896  df-iun 4944  df-iin 4945  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-se 5577  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-isom 6489  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-of 7596  df-ofr 7597  df-om 7782  df-1st 7900  df-2nd 7901  df-supp 8049  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-1o 8368  df-er 8570  df-map 8689  df-pm 8690  df-ixp 8758  df-en 8806  df-dom 8807  df-sdom 8808  df-fin 8809  df-fsupp 9228  df-sup 9300  df-oi 9368  df-card 9797  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-nn 12076  df-2 12138  df-3 12139  df-4 12140  df-5 12141  df-6 12142  df-7 12143  df-8 12144  df-9 12145  df-n0 12336  df-z 12422  df-dec 12540  df-uz 12685  df-fz 13342  df-fzo 13485  df-seq 13824  df-hash 14147  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-sca 17076  df-vsca 17077  df-ip 17078  df-tset 17079  df-ple 17080  df-ds 17082  df-hom 17084  df-cco 17085  df-0g 17250  df-gsum 17251  df-prds 17256  df-pws 17258  df-mre 17393  df-mrc 17394  df-acs 17396  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-mhm 18528  df-submnd 18529  df-grp 18677  df-minusg 18678  df-sbg 18679  df-mulg 18798  df-subg 18849  df-ghm 18929  df-cntz 19020  df-cmn 19484  df-abl 19485  df-mgp 19817  df-ur 19834  df-ring 19881  df-subrg 20128  df-lmod 20232  df-lss 20301  df-sra 20541  df-rgmod 20542  df-dsmm 21046  df-frlm 21061  df-ascl 21169  df-psr 21219  df-mvr 21220  df-mpl 21221  df-opsr 21223  df-psr1 21458  df-vr1 21459  df-ply1 21460  df-coe1 21461  df-mat 21662  df-cpmat 21962
This theorem is referenced by:  m2cpminvid2  22011
  Copyright terms: Public domain W3C validator