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

Theorem evl1gsumdlem 21296
Description: Lemma for evl1gsumd 21297 (induction step). (Contributed by AV, 17-Sep-2019.)
Hypotheses
Ref Expression
evl1gsumd.q 𝑂 = (eval1𝑅)
evl1gsumd.p 𝑃 = (Poly1𝑅)
evl1gsumd.b 𝐵 = (Base‘𝑅)
evl1gsumd.u 𝑈 = (Base‘𝑃)
evl1gsumd.r (𝜑𝑅 ∈ CRing)
evl1gsumd.y (𝜑𝑌𝐵)
Assertion
Ref Expression
evl1gsumdlem ((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) → ((∀𝑥𝑚 𝑀𝑈 → ((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌))))))
Distinct variable groups:   𝑥,𝑂   𝑥,𝑈   𝑥,𝑌   𝑥,𝑎   𝑥,𝑚
Allowed substitution hints:   𝜑(𝑥,𝑚,𝑎)   𝐵(𝑥,𝑚,𝑎)   𝑃(𝑥,𝑚,𝑎)   𝑅(𝑥,𝑚,𝑎)   𝑈(𝑚,𝑎)   𝑀(𝑥,𝑚,𝑎)   𝑂(𝑚,𝑎)   𝑌(𝑚,𝑎)

Proof of Theorem evl1gsumdlem
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ralunb 4119 . . 3 (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀𝑈 ↔ (∀𝑥𝑚 𝑀𝑈 ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈))
2 nfcv 2905 . . . . . . . . . . . . . . . . 17 𝑦𝑀
3 nfcsb1v 3850 . . . . . . . . . . . . . . . . 17 𝑥𝑦 / 𝑥𝑀
4 csbeq1a 3839 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦𝑀 = 𝑦 / 𝑥𝑀)
52, 3, 4cbvmpt 5170 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀) = (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑦 / 𝑥𝑀)
65oveq2i 7242 . . . . . . . . . . . . . . 15 (𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)) = (𝑃 Σg (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑦 / 𝑥𝑀))
7 evl1gsumd.u . . . . . . . . . . . . . . . 16 𝑈 = (Base‘𝑃)
8 eqid 2738 . . . . . . . . . . . . . . . 16 (+g𝑃) = (+g𝑃)
9 evl1gsumd.r . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑅 ∈ CRing)
10 crngring 19598 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
119, 10syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑅 ∈ Ring)
12 evl1gsumd.p . . . . . . . . . . . . . . . . . . . . 21 𝑃 = (Poly1𝑅)
1312ply1ring 21193 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
1411, 13syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑃 ∈ Ring)
15 ringcmn 19623 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
1614, 15syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑃 ∈ CMnd)
17163ad2ant3 1137 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) → 𝑃 ∈ CMnd)
1817ad2antrr 726 . . . . . . . . . . . . . . . 16 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → 𝑃 ∈ CMnd)
19 simpll1 1214 . . . . . . . . . . . . . . . 16 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → 𝑚 ∈ Fin)
20 rspcsbela 4364 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑚 ∧ ∀𝑥𝑚 𝑀𝑈) → 𝑦 / 𝑥𝑀𝑈)
2120expcom 417 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝑚 𝑀𝑈 → (𝑦𝑚𝑦 / 𝑥𝑀𝑈))
2221adantl 485 . . . . . . . . . . . . . . . . . 18 (((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) → (𝑦𝑚𝑦 / 𝑥𝑀𝑈))
2322adantr 484 . . . . . . . . . . . . . . . . 17 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → (𝑦𝑚𝑦 / 𝑥𝑀𝑈))
2423imp 410 . . . . . . . . . . . . . . . 16 (((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) ∧ 𝑦𝑚) → 𝑦 / 𝑥𝑀𝑈)
25 vex 3424 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
2625a1i 11 . . . . . . . . . . . . . . . 16 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → 𝑎 ∈ V)
27 simpll2 1215 . . . . . . . . . . . . . . . 16 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → ¬ 𝑎𝑚)
28 vsnid 4592 . . . . . . . . . . . . . . . . . 18 𝑎 ∈ {𝑎}
29 rspcsbela 4364 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ {𝑎} ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → 𝑎 / 𝑥𝑀𝑈)
3028, 29mpan 690 . . . . . . . . . . . . . . . . 17 (∀𝑥 ∈ {𝑎}𝑀𝑈𝑎 / 𝑥𝑀𝑈)
3130adantl 485 . . . . . . . . . . . . . . . 16 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → 𝑎 / 𝑥𝑀𝑈)
32 csbeq1 3828 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑎𝑦 / 𝑥𝑀 = 𝑎 / 𝑥𝑀)
337, 8, 18, 19, 24, 26, 27, 31, 32gsumunsn 19369 . . . . . . . . . . . . . . 15 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → (𝑃 Σg (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑦 / 𝑥𝑀)) = ((𝑃 Σg (𝑦𝑚𝑦 / 𝑥𝑀))(+g𝑃)𝑎 / 𝑥𝑀))
346, 33syl5eq 2791 . . . . . . . . . . . . . 14 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → (𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)) = ((𝑃 Σg (𝑦𝑚𝑦 / 𝑥𝑀))(+g𝑃)𝑎 / 𝑥𝑀))
352, 3, 4cbvmpt 5170 . . . . . . . . . . . . . . . . 17 (𝑥𝑚𝑀) = (𝑦𝑚𝑦 / 𝑥𝑀)
3635eqcomi 2747 . . . . . . . . . . . . . . . 16 (𝑦𝑚𝑦 / 𝑥𝑀) = (𝑥𝑚𝑀)
3736oveq2i 7242 . . . . . . . . . . . . . . 15 (𝑃 Σg (𝑦𝑚𝑦 / 𝑥𝑀)) = (𝑃 Σg (𝑥𝑚𝑀))
3837oveq1i 7241 . . . . . . . . . . . . . 14 ((𝑃 Σg (𝑦𝑚𝑦 / 𝑥𝑀))(+g𝑃)𝑎 / 𝑥𝑀) = ((𝑃 Σg (𝑥𝑚𝑀))(+g𝑃)𝑎 / 𝑥𝑀)
3934, 38eqtrdi 2795 . . . . . . . . . . . . 13 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → (𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)) = ((𝑃 Σg (𝑥𝑚𝑀))(+g𝑃)𝑎 / 𝑥𝑀))
4039fveq2d 6739 . . . . . . . . . . . 12 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → (𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀))) = (𝑂‘((𝑃 Σg (𝑥𝑚𝑀))(+g𝑃)𝑎 / 𝑥𝑀)))
4140fveq1d 6737 . . . . . . . . . . 11 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = ((𝑂‘((𝑃 Σg (𝑥𝑚𝑀))(+g𝑃)𝑎 / 𝑥𝑀))‘𝑌))
42 evl1gsumd.q . . . . . . . . . . . . 13 𝑂 = (eval1𝑅)
43 evl1gsumd.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝑅)
4493ad2ant3 1137 . . . . . . . . . . . . . 14 ((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) → 𝑅 ∈ CRing)
4544ad2antrr 726 . . . . . . . . . . . . 13 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → 𝑅 ∈ CRing)
46 evl1gsumd.y . . . . . . . . . . . . . . 15 (𝜑𝑌𝐵)
47463ad2ant3 1137 . . . . . . . . . . . . . 14 ((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) → 𝑌𝐵)
4847ad2antrr 726 . . . . . . . . . . . . 13 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → 𝑌𝐵)
49 simplr 769 . . . . . . . . . . . . . . 15 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → ∀𝑥𝑚 𝑀𝑈)
507, 18, 19, 49gsummptcl 19376 . . . . . . . . . . . . . 14 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → (𝑃 Σg (𝑥𝑚𝑀)) ∈ 𝑈)
51 eqidd 2739 . . . . . . . . . . . . . 14 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → ((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = ((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌))
5250, 51jca 515 . . . . . . . . . . . . 13 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → ((𝑃 Σg (𝑥𝑚𝑀)) ∈ 𝑈 ∧ ((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = ((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌)))
53 eqidd 2739 . . . . . . . . . . . . . 14 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → ((𝑂𝑎 / 𝑥𝑀)‘𝑌) = ((𝑂𝑎 / 𝑥𝑀)‘𝑌))
5431, 53jca 515 . . . . . . . . . . . . 13 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → (𝑎 / 𝑥𝑀𝑈 ∧ ((𝑂𝑎 / 𝑥𝑀)‘𝑌) = ((𝑂𝑎 / 𝑥𝑀)‘𝑌)))
55 eqid 2738 . . . . . . . . . . . . 13 (+g𝑅) = (+g𝑅)
5642, 12, 43, 7, 45, 48, 52, 54, 8, 55evl1addd 21281 . . . . . . . . . . . 12 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → (((𝑃 Σg (𝑥𝑚𝑀))(+g𝑃)𝑎 / 𝑥𝑀) ∈ 𝑈 ∧ ((𝑂‘((𝑃 Σg (𝑥𝑚𝑀))(+g𝑃)𝑎 / 𝑥𝑀))‘𝑌) = (((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌)(+g𝑅)((𝑂𝑎 / 𝑥𝑀)‘𝑌))))
5756simprd 499 . . . . . . . . . . 11 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → ((𝑂‘((𝑃 Σg (𝑥𝑚𝑀))(+g𝑃)𝑎 / 𝑥𝑀))‘𝑌) = (((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌)(+g𝑅)((𝑂𝑎 / 𝑥𝑀)‘𝑌)))
5841, 57eqtrd 2778 . . . . . . . . . 10 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌)(+g𝑅)((𝑂𝑎 / 𝑥𝑀)‘𝑌)))
59 oveq1 7238 . . . . . . . . . 10 (((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌))) → (((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌)(+g𝑅)((𝑂𝑎 / 𝑥𝑀)‘𝑌)) = ((𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)))(+g𝑅)((𝑂𝑎 / 𝑥𝑀)‘𝑌)))
6058, 59sylan9eq 2799 . . . . . . . . 9 (((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) ∧ ((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)))) → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = ((𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)))(+g𝑅)((𝑂𝑎 / 𝑥𝑀)‘𝑌)))
61 nfcv 2905 . . . . . . . . . . . . . 14 𝑦((𝑂𝑀)‘𝑌)
62 nfcsb1v 3850 . . . . . . . . . . . . . 14 𝑥𝑦 / 𝑥((𝑂𝑀)‘𝑌)
63 csbeq1a 3839 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑂𝑀)‘𝑌) = 𝑦 / 𝑥((𝑂𝑀)‘𝑌))
6461, 62, 63cbvmpt 5170 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌)) = (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑦 / 𝑥((𝑂𝑀)‘𝑌))
6564oveq2i 7242 . . . . . . . . . . . 12 (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌))) = (𝑅 Σg (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑦 / 𝑥((𝑂𝑀)‘𝑌)))
66 ringcmn 19623 . . . . . . . . . . . . . . . 16 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
6711, 66syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑅 ∈ CMnd)
68673ad2ant3 1137 . . . . . . . . . . . . . 14 ((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) → 𝑅 ∈ CMnd)
6968ad2antrr 726 . . . . . . . . . . . . 13 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → 𝑅 ∈ CMnd)
70 csbfv12 6778 . . . . . . . . . . . . . . 15 𝑦 / 𝑥((𝑂𝑀)‘𝑌) = (𝑦 / 𝑥(𝑂𝑀)‘𝑦 / 𝑥𝑌)
71 csbfv2g 6779 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ V → 𝑦 / 𝑥(𝑂𝑀) = (𝑂𝑦 / 𝑥𝑀))
7271elv 3426 . . . . . . . . . . . . . . . 16 𝑦 / 𝑥(𝑂𝑀) = (𝑂𝑦 / 𝑥𝑀)
73 csbconstg 3844 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ V → 𝑦 / 𝑥𝑌 = 𝑌)
7473elv 3426 . . . . . . . . . . . . . . . 16 𝑦 / 𝑥𝑌 = 𝑌
7572, 74fveq12i 6741 . . . . . . . . . . . . . . 15 (𝑦 / 𝑥(𝑂𝑀)‘𝑦 / 𝑥𝑌) = ((𝑂𝑦 / 𝑥𝑀)‘𝑌)
7670, 75eqtri 2766 . . . . . . . . . . . . . 14 𝑦 / 𝑥((𝑂𝑀)‘𝑌) = ((𝑂𝑦 / 𝑥𝑀)‘𝑌)
7745adantr 484 . . . . . . . . . . . . . . 15 (((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) ∧ 𝑦𝑚) → 𝑅 ∈ CRing)
7848adantr 484 . . . . . . . . . . . . . . 15 (((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) ∧ 𝑦𝑚) → 𝑌𝐵)
7942, 12, 43, 7, 77, 78, 24fveval1fvcl 21273 . . . . . . . . . . . . . 14 (((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) ∧ 𝑦𝑚) → ((𝑂𝑦 / 𝑥𝑀)‘𝑌) ∈ 𝐵)
8076, 79eqeltrid 2843 . . . . . . . . . . . . 13 (((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) ∧ 𝑦𝑚) → 𝑦 / 𝑥((𝑂𝑀)‘𝑌) ∈ 𝐵)
8142, 12, 43, 7, 45, 48, 31fveval1fvcl 21273 . . . . . . . . . . . . 13 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → ((𝑂𝑎 / 𝑥𝑀)‘𝑌) ∈ 𝐵)
82 nfcv 2905 . . . . . . . . . . . . . 14 𝑥𝑎
83 nfcv 2905 . . . . . . . . . . . . . . . 16 𝑥𝑂
84 nfcsb1v 3850 . . . . . . . . . . . . . . . 16 𝑥𝑎 / 𝑥𝑀
8583, 84nffv 6745 . . . . . . . . . . . . . . 15 𝑥(𝑂𝑎 / 𝑥𝑀)
86 nfcv 2905 . . . . . . . . . . . . . . 15 𝑥𝑌
8785, 86nffv 6745 . . . . . . . . . . . . . 14 𝑥((𝑂𝑎 / 𝑥𝑀)‘𝑌)
88 csbeq1a 3839 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎𝑀 = 𝑎 / 𝑥𝑀)
8988fveq2d 6739 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → (𝑂𝑀) = (𝑂𝑎 / 𝑥𝑀))
9089fveq1d 6737 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → ((𝑂𝑀)‘𝑌) = ((𝑂𝑎 / 𝑥𝑀)‘𝑌))
9182, 87, 90csbhypf 3854 . . . . . . . . . . . . 13 (𝑦 = 𝑎𝑦 / 𝑥((𝑂𝑀)‘𝑌) = ((𝑂𝑎 / 𝑥𝑀)‘𝑌))
9243, 55, 69, 19, 80, 26, 27, 81, 91gsumunsn 19369 . . . . . . . . . . . 12 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → (𝑅 Σg (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑦 / 𝑥((𝑂𝑀)‘𝑌))) = ((𝑅 Σg (𝑦𝑚𝑦 / 𝑥((𝑂𝑀)‘𝑌)))(+g𝑅)((𝑂𝑎 / 𝑥𝑀)‘𝑌)))
9365, 92syl5eq 2791 . . . . . . . . . . 11 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌))) = ((𝑅 Σg (𝑦𝑚𝑦 / 𝑥((𝑂𝑀)‘𝑌)))(+g𝑅)((𝑂𝑎 / 𝑥𝑀)‘𝑌)))
9461, 62, 63cbvmpt 5170 . . . . . . . . . . . . . 14 (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)) = (𝑦𝑚𝑦 / 𝑥((𝑂𝑀)‘𝑌))
9594eqcomi 2747 . . . . . . . . . . . . 13 (𝑦𝑚𝑦 / 𝑥((𝑂𝑀)‘𝑌)) = (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌))
9695oveq2i 7242 . . . . . . . . . . . 12 (𝑅 Σg (𝑦𝑚𝑦 / 𝑥((𝑂𝑀)‘𝑌))) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)))
9796oveq1i 7241 . . . . . . . . . . 11 ((𝑅 Σg (𝑦𝑚𝑦 / 𝑥((𝑂𝑀)‘𝑌)))(+g𝑅)((𝑂𝑎 / 𝑥𝑀)‘𝑌)) = ((𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)))(+g𝑅)((𝑂𝑎 / 𝑥𝑀)‘𝑌))
9893, 97eqtr2di 2796 . . . . . . . . . 10 ((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → ((𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)))(+g𝑅)((𝑂𝑎 / 𝑥𝑀)‘𝑌)) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌))))
9998adantr 484 . . . . . . . . 9 (((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) ∧ ((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)))) → ((𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)))(+g𝑅)((𝑂𝑎 / 𝑥𝑀)‘𝑌)) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌))))
10060, 99eqtrd 2778 . . . . . . . 8 (((((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) ∧ ((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)))) → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌))))
101100exp31 423 . . . . . . 7 (((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) → (∀𝑥 ∈ {𝑎}𝑀𝑈 → (((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌))) → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌))))))
102101com23 86 . . . . . 6 (((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ ∀𝑥𝑚 𝑀𝑈) → (((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌))) → (∀𝑥 ∈ {𝑎}𝑀𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌))))))
103102ex 416 . . . . 5 ((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) → (∀𝑥𝑚 𝑀𝑈 → (((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌))) → (∀𝑥 ∈ {𝑎}𝑀𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌)))))))
104103a2d 29 . . . 4 ((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) → ((∀𝑥𝑚 𝑀𝑈 → ((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)))) → (∀𝑥𝑚 𝑀𝑈 → (∀𝑥 ∈ {𝑎}𝑀𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌)))))))
105104imp4b 425 . . 3 (((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ (∀𝑥𝑚 𝑀𝑈 → ((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌))))) → ((∀𝑥𝑚 𝑀𝑈 ∧ ∀𝑥 ∈ {𝑎}𝑀𝑈) → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌)))))
1061, 105syl5bi 245 . 2 (((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) ∧ (∀𝑥𝑚 𝑀𝑈 → ((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌))))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌)))))
107106ex 416 1 ((𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑) → ((∀𝑥𝑚 𝑀𝑈 → ((𝑂‘(𝑃 Σg (𝑥𝑚𝑀)))‘𝑌) = (𝑅 Σg (𝑥𝑚 ↦ ((𝑂𝑀)‘𝑌)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂𝑀)‘𝑌))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2111  wral 3062  Vcvv 3420  csb 3825  cun 3878  {csn 4555  cmpt 5149  cfv 6397  (class class class)co 7231  Fincfn 8646  Basecbs 16784  +gcplusg 16826   Σg cgsu 16969  CMndccmn 19194  Ringcrg 19586  CRingccrg 19587  Poly1cpl1 21122  eval1ce1 21254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-cnex 10809  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-mulcom 10817  ax-addass 10818  ax-mulass 10819  ax-distr 10820  ax-i2m1 10821  ax-1ne0 10822  ax-1rid 10823  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826  ax-pre-lttri 10827  ax-pre-lttrn 10828  ax-pre-ltadd 10829  ax-pre-mulgt0 10830
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-int 4874  df-iun 4920  df-iin 4921  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-se 5524  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-pred 6175  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-isom 6406  df-riota 7188  df-ov 7234  df-oprab 7235  df-mpo 7236  df-of 7487  df-ofr 7488  df-om 7663  df-1st 7779  df-2nd 7780  df-supp 7924  df-wrecs 8067  df-recs 8128  df-rdg 8166  df-1o 8222  df-er 8411  df-map 8530  df-pm 8531  df-ixp 8599  df-en 8647  df-dom 8648  df-sdom 8649  df-fin 8650  df-fsupp 9010  df-sup 9082  df-oi 9150  df-card 9579  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-sub 11088  df-neg 11089  df-nn 11855  df-2 11917  df-3 11918  df-4 11919  df-5 11920  df-6 11921  df-7 11922  df-8 11923  df-9 11924  df-n0 12115  df-z 12201  df-dec 12318  df-uz 12463  df-fz 13120  df-fzo 13263  df-seq 13599  df-hash 13921  df-struct 16724  df-sets 16741  df-slot 16759  df-ndx 16769  df-base 16785  df-ress 16809  df-plusg 16839  df-mulr 16840  df-sca 16842  df-vsca 16843  df-ip 16844  df-tset 16845  df-ple 16846  df-ds 16848  df-hom 16850  df-cco 16851  df-0g 16970  df-gsum 16971  df-prds 16976  df-pws 16978  df-mre 17113  df-mrc 17114  df-acs 17116  df-mgm 18138  df-sgrp 18187  df-mnd 18198  df-mhm 18242  df-submnd 18243  df-grp 18392  df-minusg 18393  df-sbg 18394  df-mulg 18513  df-subg 18564  df-ghm 18644  df-cntz 18735  df-cmn 19196  df-abl 19197  df-mgp 19529  df-ur 19541  df-srg 19545  df-ring 19588  df-cring 19589  df-rnghom 19759  df-subrg 19822  df-lmod 19925  df-lss 19993  df-lsp 20033  df-assa 20839  df-asp 20840  df-ascl 20841  df-psr 20892  df-mvr 20893  df-mpl 20894  df-opsr 20896  df-evls 21056  df-evl 21057  df-psr1 21125  df-ply1 21127  df-evl1 21256
This theorem is referenced by:  evl1gsumd  21297
  Copyright terms: Public domain W3C validator