Step | Hyp | Ref
| Expression |
1 | | ralunb 4119 |
. . 3
⊢
(∀𝑥 ∈
(𝑚 ∪ {𝑎})𝑀 ∈ 𝑈 ↔ (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈)) |
2 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦𝑀 |
3 | | nfcsb1v 3850 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑀 |
4 | | csbeq1a 3839 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → 𝑀 = ⦋𝑦 / 𝑥⦌𝑀) |
5 | 2, 3, 4 | cbvmpt 5170 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀) = (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ ⦋𝑦 / 𝑥⦌𝑀) |
6 | 5 | oveq2i 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) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑅 ∈ Ring) |
12 | | evl1gsumd.p |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑃 = (Poly1‘𝑅) |
13 | 12 | ply1ring 21193 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
14 | 11, 13 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑃 ∈ Ring) |
15 | | ringcmn 19623 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑃 ∈ CMnd) |
17 | 16 | 3ad2ant3 1137 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → 𝑃 ∈ CMnd) |
18 | 17 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → 𝑃 ∈ CMnd) |
19 | | simpll1 1214 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → 𝑚 ∈ Fin) |
20 | | rspcsbela 4364 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ 𝑚 ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) → ⦋𝑦 / 𝑥⦌𝑀 ∈ 𝑈) |
21 | 20 | expcom 417 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
𝑚 𝑀 ∈ 𝑈 → (𝑦 ∈ 𝑚 → ⦋𝑦 / 𝑥⦌𝑀 ∈ 𝑈)) |
22 | 21 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) → (𝑦 ∈ 𝑚 → ⦋𝑦 / 𝑥⦌𝑀 ∈ 𝑈)) |
23 | 22 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → (𝑦 ∈ 𝑚 → ⦋𝑦 / 𝑥⦌𝑀 ∈ 𝑈)) |
24 | 23 | imp 410 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑚 ∈ Fin
∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) ∧ 𝑦 ∈ 𝑚) → ⦋𝑦 / 𝑥⦌𝑀 ∈ 𝑈) |
25 | | vex 3424 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑎 ∈ V |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → 𝑎 ∈ V) |
27 | | simpll2 1215 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ¬ 𝑎 ∈ 𝑚) |
28 | | vsnid 4592 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑎 ∈ {𝑎} |
29 | | rspcsbela 4364 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ {𝑎} ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ⦋𝑎 / 𝑥⦌𝑀 ∈ 𝑈) |
30 | 28, 29 | mpan 690 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
{𝑎}𝑀 ∈ 𝑈 → ⦋𝑎 / 𝑥⦌𝑀 ∈ 𝑈) |
31 | 30 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ⦋𝑎 / 𝑥⦌𝑀 ∈ 𝑈) |
32 | | csbeq1 3828 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑎 → ⦋𝑦 / 𝑥⦌𝑀 = ⦋𝑎 / 𝑥⦌𝑀) |
33 | 7, 8, 18, 19, 24, 26, 27, 31, 32 | gsumunsn 19369 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → (𝑃 Σg (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ ⦋𝑦 / 𝑥⦌𝑀)) = ((𝑃 Σg (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀)) |
34 | 6, 33 | syl5eq 2791 |
. . . . . . . . . . . . . 14
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → (𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)) = ((𝑃 Σg (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀)) |
35 | 2, 3, 4 | cbvmpt 5170 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑚 ↦ 𝑀) = (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌𝑀) |
36 | 35 | eqcomi 2747 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌𝑀) = (𝑥 ∈ 𝑚 ↦ 𝑀) |
37 | 36 | oveq2i 7242 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 Σg
(𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌𝑀)) = (𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)) |
38 | 37 | oveq1i 7241 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 Σg
(𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀) = ((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀) |
39 | 34, 38 | eqtrdi 2795 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → (𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)) = ((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀)) |
40 | 39 | fveq2d 6739 |
. . . . . . . . . . . 12
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → (𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀))) = (𝑂‘((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀))) |
41 | 40 | fveq1d 6737 |
. . . . . . . . . . 11
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = ((𝑂‘((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀))‘𝑌)) |
42 | | evl1gsumd.q |
. . . . . . . . . . . . 13
⊢ 𝑂 = (eval1‘𝑅) |
43 | | evl1gsumd.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑅) |
44 | 9 | 3ad2ant3 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → 𝑅 ∈ CRing) |
45 | 44 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → 𝑅 ∈ CRing) |
46 | | evl1gsumd.y |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
47 | 46 | 3ad2ant3 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → 𝑌 ∈ 𝐵) |
48 | 47 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → 𝑌 ∈ 𝐵) |
49 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) |
50 | 7, 18, 19, 49 | gsummptcl 19376 |
. . . . . . . . . . . . . 14
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → (𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)) ∈ 𝑈) |
51 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌)) |
52 | 50, 51 | jca 515 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)) ∈ 𝑈 ∧ ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌))) |
53 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌) = ((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌)) |
54 | 31, 53 | jca 515 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → (⦋𝑎 / 𝑥⦌𝑀 ∈ 𝑈 ∧ ((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌) = ((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌))) |
55 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(+g‘𝑅) = (+g‘𝑅) |
56 | 42, 12, 43, 7, 45, 48, 52, 54, 8, 55 | evl1addd 21281 |
. . . . . . . . . . . 12
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → (((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀) ∈ 𝑈 ∧ ((𝑂‘((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀))‘𝑌) = (((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌)(+g‘𝑅)((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌)))) |
57 | 56 | simprd 499 |
. . . . . . . . . . 11
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ((𝑂‘((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀))‘𝑌) = (((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌)(+g‘𝑅)((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌))) |
58 | 41, 57 | eqtrd 2778 |
. . . . . . . . . 10
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌)(+g‘𝑅)((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌))) |
59 | | oveq1 7238 |
. . . . . . . . . 10
⊢ (((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌))) → (((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌)(+g‘𝑅)((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌)) = ((𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))(+g‘𝑅)((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌))) |
60 | 58, 59 | sylan9eq 2799 |
. . . . . . . . 9
⊢
(((((𝑚 ∈ Fin
∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) ∧ ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = ((𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))(+g‘𝑅)((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌))) |
61 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦((𝑂‘𝑀)‘𝑌) |
62 | | nfcsb1v 3850 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌) |
63 | | csbeq1a 3839 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝑂‘𝑀)‘𝑌) = ⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌)) |
64 | 61, 62, 63 | cbvmpt 5170 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌)) = (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ ⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌)) |
65 | 64 | oveq2i 7242 |
. . . . . . . . . . . 12
⊢ (𝑅 Σg
(𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌))) = (𝑅 Σg (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ ⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌))) |
66 | | ringcmn 19623 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
67 | 11, 66 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ CMnd) |
68 | 67 | 3ad2ant3 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → 𝑅 ∈ CMnd) |
69 | 68 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → 𝑅 ∈ CMnd) |
70 | | csbfv12 6778 |
. . . . . . . . . . . . . . 15
⊢
⦋𝑦 /
𝑥⦌((𝑂‘𝑀)‘𝑌) = (⦋𝑦 / 𝑥⦌(𝑂‘𝑀)‘⦋𝑦 / 𝑥⦌𝑌) |
71 | | csbfv2g 6779 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑥⦌(𝑂‘𝑀) = (𝑂‘⦋𝑦 / 𝑥⦌𝑀)) |
72 | 71 | elv 3426 |
. . . . . . . . . . . . . . . 16
⊢
⦋𝑦 /
𝑥⦌(𝑂‘𝑀) = (𝑂‘⦋𝑦 / 𝑥⦌𝑀) |
73 | | csbconstg 3844 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑥⦌𝑌 = 𝑌) |
74 | 73 | elv 3426 |
. . . . . . . . . . . . . . . 16
⊢
⦋𝑦 /
𝑥⦌𝑌 = 𝑌 |
75 | 72, 74 | fveq12i 6741 |
. . . . . . . . . . . . . . 15
⊢
(⦋𝑦 /
𝑥⦌(𝑂‘𝑀)‘⦋𝑦 / 𝑥⦌𝑌) = ((𝑂‘⦋𝑦 / 𝑥⦌𝑀)‘𝑌) |
76 | 70, 75 | eqtri 2766 |
. . . . . . . . . . . . . 14
⊢
⦋𝑦 /
𝑥⦌((𝑂‘𝑀)‘𝑌) = ((𝑂‘⦋𝑦 / 𝑥⦌𝑀)‘𝑌) |
77 | 45 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑚 ∈ Fin
∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) ∧ 𝑦 ∈ 𝑚) → 𝑅 ∈ CRing) |
78 | 48 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑚 ∈ Fin
∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) ∧ 𝑦 ∈ 𝑚) → 𝑌 ∈ 𝐵) |
79 | 42, 12, 43, 7, 77, 78, 24 | fveval1fvcl 21273 |
. . . . . . . . . . . . . 14
⊢
(((((𝑚 ∈ Fin
∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) ∧ 𝑦 ∈ 𝑚) → ((𝑂‘⦋𝑦 / 𝑥⦌𝑀)‘𝑌) ∈ 𝐵) |
80 | 76, 79 | eqeltrid 2843 |
. . . . . . . . . . . . 13
⊢
(((((𝑚 ∈ Fin
∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) ∧ 𝑦 ∈ 𝑚) → ⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌) ∈ 𝐵) |
81 | 42, 12, 43, 7, 45, 48, 31 | fveval1fvcl 21273 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌) ∈ 𝐵) |
82 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑎 |
83 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥𝑂 |
84 | | nfcsb1v 3850 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋𝑎 / 𝑥⦌𝑀 |
85 | 83, 84 | nffv 6745 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑂‘⦋𝑎 / 𝑥⦌𝑀) |
86 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝑌 |
87 | 85, 86 | nffv 6745 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌) |
88 | | csbeq1a 3839 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → 𝑀 = ⦋𝑎 / 𝑥⦌𝑀) |
89 | 88 | fveq2d 6739 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (𝑂‘𝑀) = (𝑂‘⦋𝑎 / 𝑥⦌𝑀)) |
90 | 89 | fveq1d 6737 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → ((𝑂‘𝑀)‘𝑌) = ((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌)) |
91 | 82, 87, 90 | csbhypf 3854 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑎 → ⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌) = ((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌)) |
92 | 43, 55, 69, 19, 80, 26, 27, 81, 91 | gsumunsn 19369 |
. . . . . . . . . . . 12
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → (𝑅 Σg (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ ⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌))) = ((𝑅 Σg (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌)))(+g‘𝑅)((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌))) |
93 | 65, 92 | syl5eq 2791 |
. . . . . . . . . . 11
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌))) = ((𝑅 Σg (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌)))(+g‘𝑅)((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌))) |
94 | 61, 62, 63 | cbvmpt 5170 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)) = (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌)) |
95 | 94 | eqcomi 2747 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌)) = (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)) |
96 | 95 | oveq2i 7242 |
. . . . . . . . . . . 12
⊢ (𝑅 Σg
(𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌))) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌))) |
97 | 96 | oveq1i 7241 |
. . . . . . . . . . 11
⊢ ((𝑅 Σg
(𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌((𝑂‘𝑀)‘𝑌)))(+g‘𝑅)((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌)) = ((𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))(+g‘𝑅)((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌)) |
98 | 93, 97 | eqtr2di 2796 |
. . . . . . . . . 10
⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ((𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))(+g‘𝑅)((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌)) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌)))) |
99 | 98 | adantr 484 |
. . . . . . . . 9
⊢
(((((𝑚 ∈ Fin
∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) ∧ ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → ((𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))(+g‘𝑅)((𝑂‘⦋𝑎 / 𝑥⦌𝑀)‘𝑌)) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌)))) |
100 | 60, 99 | eqtrd 2778 |
. . . . . . . 8
⊢
(((((𝑚 ∈ Fin
∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) ∧ ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌)))) |
101 | 100 | exp31 423 |
. . . . . . 7
⊢ (((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) → (∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈 → (((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌))) → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌)))))) |
102 | 101 | com23 86 |
. . . . . 6
⊢ (((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈) → (((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌))) → (∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌)))))) |
103 | 102 | ex 416 |
. . . . 5
⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → (((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌))) → (∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌))))))) |
104 | 103 | a2d 29 |
. . . 4
⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → (∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌))))))) |
105 | 104 | imp4b 425 |
. . 3
⊢ (((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌))))) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝑈) → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌))))) |
106 | 1, 105 | syl5bi 245 |
. 2
⊢ (((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌))))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌))))) |
107 | 106 | ex 416 |
1
⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌)))))) |