Step | Hyp | Ref
| Expression |
1 | | mplsubg.s |
. . 3
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | eqid 2778 |
. . 3
⊢
(Base‘𝑆) =
(Base‘𝑆) |
3 | | eqid 2778 |
. . 3
⊢
(.r‘𝑆) = (.r‘𝑆) |
4 | | mpllss.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
5 | | mplsubg.p |
. . . . 5
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
6 | | mplsubg.u |
. . . . 5
⊢ 𝑈 = (Base‘𝑃) |
7 | 5, 1, 6, 2 | mplbasss 19829 |
. . . 4
⊢ 𝑈 ⊆ (Base‘𝑆) |
8 | | mplsubrglem.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
9 | 7, 8 | sseldi 3819 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (Base‘𝑆)) |
10 | | mplsubrglem.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑈) |
11 | 7, 10 | sseldi 3819 |
. . 3
⊢ (𝜑 → 𝑌 ∈ (Base‘𝑆)) |
12 | 1, 2, 3, 4, 9, 11 | psrmulcl 19785 |
. 2
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) ∈ (Base‘𝑆)) |
13 | | ovexd 6956 |
. . 3
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) ∈ V) |
14 | 1, 2 | psrelbasfun 19777 |
. . . 4
⊢ ((𝑋(.r‘𝑆)𝑌) ∈ (Base‘𝑆) → Fun (𝑋(.r‘𝑆)𝑌)) |
15 | 12, 14 | syl 17 |
. . 3
⊢ (𝜑 → Fun (𝑋(.r‘𝑆)𝑌)) |
16 | | mplsubrglem.z |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
17 | 16 | fvexi 6460 |
. . . 4
⊢ 0 ∈
V |
18 | 17 | a1i 11 |
. . 3
⊢ (𝜑 → 0 ∈ V) |
19 | | mplsubrglem.p |
. . . . 5
⊢ 𝐴 = ( ∘𝑓
+ “ ((𝑋 supp 0 ) ×
(𝑌 supp 0 ))) |
20 | | df-ima 5368 |
. . . . 5
⊢ (
∘𝑓 + “ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) = ran (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) |
21 | 19, 20 | eqtri 2802 |
. . . 4
⊢ 𝐴 = ran (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) |
22 | 5, 1, 2, 16, 6 | mplelbas 19827 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ (Base‘𝑆) ∧ 𝑋 finSupp 0 )) |
23 | 22 | simprbi 492 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑈 → 𝑋 finSupp 0 ) |
24 | 8, 23 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑋 finSupp 0 ) |
25 | 5, 1, 2, 16, 6 | mplelbas 19827 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝑈 ↔ (𝑌 ∈ (Base‘𝑆) ∧ 𝑌 finSupp 0 )) |
26 | 25 | simprbi 492 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑈 → 𝑌 finSupp 0 ) |
27 | 10, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑌 finSupp 0 ) |
28 | | fsuppxpfi 8580 |
. . . . . 6
⊢ ((𝑋 finSupp 0 ∧ 𝑌 finSupp 0 ) → ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∈
Fin) |
29 | 24, 27, 28 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∈
Fin) |
30 | | ofmres 7441 |
. . . . . . 7
⊢ (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) = (𝑓 ∈ (𝑋 supp 0 ), 𝑔 ∈ (𝑌 supp 0 ) ↦ (𝑓 ∘𝑓 +
𝑔)) |
31 | | ovex 6954 |
. . . . . . 7
⊢ (𝑓 ∘𝑓 +
𝑔) ∈
V |
32 | 30, 31 | fnmpt2i 7519 |
. . . . . 6
⊢ (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) |
33 | | dffn4 6372 |
. . . . . 6
⊢ ((
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) ↔ (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))):((𝑋 supp 0 ) × (𝑌 supp 0 ))–onto→ran ( ∘𝑓 + ↾
((𝑋 supp 0 ) × (𝑌 supp 0 )))) |
34 | 32, 33 | mpbi 222 |
. . . . 5
⊢ (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))):((𝑋 supp 0 ) × (𝑌 supp 0 ))–onto→ran ( ∘𝑓 + ↾
((𝑋 supp 0 ) × (𝑌 supp 0 ))) |
35 | | fofi 8540 |
. . . . 5
⊢ ((((𝑋 supp 0 ) × (𝑌 supp 0 )) ∈ Fin ∧ (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))):((𝑋 supp 0 ) × (𝑌 supp 0 ))–onto→ran ( ∘𝑓 + ↾
((𝑋 supp 0 ) × (𝑌 supp 0 )))) → ran (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) ∈
Fin) |
36 | 29, 34, 35 | sylancl 580 |
. . . 4
⊢ (𝜑 → ran (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) ∈
Fin) |
37 | 21, 36 | syl5eqel 2863 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
38 | | eqid 2778 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
39 | | mplsubrglem.d |
. . . . 5
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
40 | 1, 38, 39, 2, 12 | psrelbas 19776 |
. . . 4
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌):𝐷⟶(Base‘𝑅)) |
41 | | mplsubrglem.t |
. . . . . 6
⊢ · =
(.r‘𝑅) |
42 | 9 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑋 ∈ (Base‘𝑆)) |
43 | 11 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑌 ∈ (Base‘𝑆)) |
44 | | eldifi 3955 |
. . . . . . 7
⊢ (𝑘 ∈ (𝐷 ∖ 𝐴) → 𝑘 ∈ 𝐷) |
45 | 44 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑘 ∈ 𝐷) |
46 | 1, 2, 41, 3, 39, 42, 43, 45 | psrmulval 19783 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → ((𝑋(.r‘𝑆)𝑌)‘𝑘) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥)))))) |
47 | 4 | ad2antrr 716 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑅 ∈ Ring) |
48 | 5, 38, 6, 39, 10 | mplelf 19830 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) |
49 | 48 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅)) |
50 | | ssrab2 3908 |
. . . . . . . . . . . 12
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ⊆ 𝐷 |
51 | | mplsubg.i |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
52 | 51 | ad2antrr 716 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝐼 ∈ 𝑊) |
53 | 45 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑘 ∈ 𝐷) |
54 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) |
55 | | eqid 2778 |
. . . . . . . . . . . . . 14
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} |
56 | 39, 55 | psrbagconcl 19770 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) |
57 | 52, 53, 54, 56 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) |
58 | 50, 57 | sseldi 3819 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑥) ∈ 𝐷) |
59 | 49, 58 | ffvelrnd 6624 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) ∈ (Base‘𝑅)) |
60 | 38, 41, 16 | ringlz 18974 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑌‘(𝑘 ∘𝑓 − 𝑥)) ∈ (Base‘𝑅)) → ( 0 · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 ) |
61 | 47, 59, 60 | syl2anc 579 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ( 0 · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 ) |
62 | | oveq1 6929 |
. . . . . . . . . 10
⊢ ((𝑋‘𝑥) = 0 → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = ( 0 · (𝑌‘(𝑘 ∘𝑓 − 𝑥)))) |
63 | 62 | eqeq1d 2780 |
. . . . . . . . 9
⊢ ((𝑋‘𝑥) = 0 → (((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 ↔ ( 0 · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 )) |
64 | 61, 63 | syl5ibrcom 239 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋‘𝑥) = 0 → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 )) |
65 | 5, 38, 6, 39, 8 | mplelf 19830 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
66 | 65 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅)) |
67 | 50, 54 | sseldi 3819 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥 ∈ 𝐷) |
68 | 66, 67 | ffvelrnd 6624 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
69 | 38, 41, 16 | ringrz 18975 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑥) ∈ (Base‘𝑅)) → ((𝑋‘𝑥) · 0 ) = 0 ) |
70 | 47, 68, 69 | syl2anc 579 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋‘𝑥) · 0 ) = 0 ) |
71 | | oveq2 6930 |
. . . . . . . . . 10
⊢ ((𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = ((𝑋‘𝑥) · 0 )) |
72 | 71 | eqeq1d 2780 |
. . . . . . . . 9
⊢ ((𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 → (((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 ↔ ((𝑋‘𝑥) · 0 ) = 0 )) |
73 | 70, 72 | syl5ibrcom 239 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 )) |
74 | 39 | psrbagf 19762 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑥 ∈ 𝐷) → 𝑥:𝐼⟶ℕ0) |
75 | 52, 67, 74 | syl2anc 579 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥:𝐼⟶ℕ0) |
76 | 75 | ffvelrnda 6623 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑛 ∈ 𝐼) → (𝑥‘𝑛) ∈
ℕ0) |
77 | 39 | psrbagf 19762 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷) → 𝑘:𝐼⟶ℕ0) |
78 | 52, 53, 77 | syl2anc 579 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑘:𝐼⟶ℕ0) |
79 | 78 | ffvelrnda 6623 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑛 ∈ 𝐼) → (𝑘‘𝑛) ∈
ℕ0) |
80 | | nn0cn 11653 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥‘𝑛) ∈ ℕ0 → (𝑥‘𝑛) ∈ ℂ) |
81 | | nn0cn 11653 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘‘𝑛) ∈ ℕ0 → (𝑘‘𝑛) ∈ ℂ) |
82 | | pncan3 10630 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥‘𝑛) ∈ ℂ ∧ (𝑘‘𝑛) ∈ ℂ) → ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛))) = (𝑘‘𝑛)) |
83 | 80, 81, 82 | syl2an 589 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥‘𝑛) ∈ ℕ0 ∧ (𝑘‘𝑛) ∈ ℕ0) → ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛))) = (𝑘‘𝑛)) |
84 | 76, 79, 83 | syl2anc 579 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑛 ∈ 𝐼) → ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛))) = (𝑘‘𝑛)) |
85 | 84 | mpteq2dva 4979 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑛 ∈ 𝐼 ↦ ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑘‘𝑛))) |
86 | | ovexd 6956 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑛 ∈ 𝐼) → ((𝑘‘𝑛) − (𝑥‘𝑛)) ∈ V) |
87 | 75 | feqmptd 6509 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥 = (𝑛 ∈ 𝐼 ↦ (𝑥‘𝑛))) |
88 | 78 | feqmptd 6509 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑘 = (𝑛 ∈ 𝐼 ↦ (𝑘‘𝑛))) |
89 | 52, 79, 76, 88, 87 | offval2 7191 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑥) = (𝑛 ∈ 𝐼 ↦ ((𝑘‘𝑛) − (𝑥‘𝑛)))) |
90 | 52, 76, 86, 87, 89 | offval2 7191 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑥 ∘𝑓 + (𝑘 ∘𝑓
− 𝑥)) = (𝑛 ∈ 𝐼 ↦ ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛))))) |
91 | 85, 90, 88 | 3eqtr4d 2824 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑥 ∘𝑓 + (𝑘 ∘𝑓
− 𝑥)) = 𝑘) |
92 | | simplr 759 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑘 ∈ (𝐷 ∖ 𝐴)) |
93 | 91, 92 | eqeltrd 2859 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑥 ∘𝑓 + (𝑘 ∘𝑓
− 𝑥)) ∈ (𝐷 ∖ 𝐴)) |
94 | 93 | eldifbd 3805 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ¬ (𝑥 ∘𝑓 +
(𝑘
∘𝑓 − 𝑥)) ∈ 𝐴) |
95 | | ovres 7077 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘𝑓 +
↾ ((𝑋 supp 0 ) ×
(𝑌 supp 0 )))(𝑘 ∘𝑓 − 𝑥)) = (𝑥 ∘𝑓 + (𝑘 ∘𝑓
− 𝑥))) |
96 | | fnovrn 7086 |
. . . . . . . . . . . . . 14
⊢ (((
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∧ 𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘𝑓 +
↾ ((𝑋 supp 0 ) ×
(𝑌 supp 0 )))(𝑘 ∘𝑓 − 𝑥)) ∈ ran (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))) |
97 | 96, 21 | syl6eleqr 2870 |
. . . . . . . . . . . . 13
⊢ (((
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∧ 𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘𝑓 +
↾ ((𝑋 supp 0 ) ×
(𝑌 supp 0 )))(𝑘 ∘𝑓 − 𝑥)) ∈ 𝐴) |
98 | 32, 97 | mp3an1 1521 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘𝑓 +
↾ ((𝑋 supp 0 ) ×
(𝑌 supp 0 )))(𝑘 ∘𝑓 − 𝑥)) ∈ 𝐴) |
99 | 95, 98 | eqeltrrd 2860 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) → (𝑥 ∘𝑓 +
(𝑘
∘𝑓 − 𝑥)) ∈ 𝐴) |
100 | 94, 99 | nsyl 138 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ¬ (𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 ))) |
101 | | ianor 967 |
. . . . . . . . . 10
⊢ (¬
(𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) ↔ (¬ 𝑥 ∈ (𝑋 supp 0 ) ∨ ¬ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 ))) |
102 | 100, 101 | sylib 210 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (¬ 𝑥 ∈ (𝑋 supp 0 ) ∨ ¬ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 ))) |
103 | | eldif 3802 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ (𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ (𝑋 supp 0 ))) |
104 | 103 | baib 531 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ ¬ 𝑥 ∈ (𝑋 supp 0 ))) |
105 | 67, 104 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ ¬ 𝑥 ∈ (𝑋 supp 0 ))) |
106 | | ssidd 3843 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑋 supp 0 ) ⊆ (𝑋 supp 0 )) |
107 | | ovex 6954 |
. . . . . . . . . . . . . . 15
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
108 | 39, 107 | rabex2 5051 |
. . . . . . . . . . . . . 14
⊢ 𝐷 ∈ V |
109 | 108 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝐷 ∈ V) |
110 | 17 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 0 ∈ V) |
111 | 66, 106, 109, 110 | suppssr 7608 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋‘𝑥) = 0 ) |
112 | 111 | ex 403 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) → (𝑋‘𝑥) = 0 )) |
113 | 105, 112 | sylbird 252 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (¬ 𝑥 ∈ (𝑋 supp 0 ) → (𝑋‘𝑥) = 0 )) |
114 | | eldif 3802 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∘𝑓
− 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) ↔ ((𝑘 ∘𝑓
− 𝑥) ∈ 𝐷 ∧ ¬ (𝑘 ∘𝑓 − 𝑥) ∈ (𝑌 supp 0 ))) |
115 | 114 | baib 531 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∘𝑓
− 𝑥) ∈ 𝐷 → ((𝑘 ∘𝑓 − 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) ↔ ¬ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 ))) |
116 | 58, 115 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑘 ∘𝑓 − 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) ↔ ¬ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 ))) |
117 | | ssidd 3843 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑌 supp 0 ) ⊆ (𝑌 supp 0 )) |
118 | 49, 117, 109, 110 | suppssr 7608 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ (𝑘 ∘𝑓 − 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 ))) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 ) |
119 | 118 | ex 403 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑘 ∘𝑓 − 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 )) |
120 | 116, 119 | sylbird 252 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (¬ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 ) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 )) |
121 | 113, 120 | orim12d 950 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((¬ 𝑥 ∈ (𝑋 supp 0 ) ∨ ¬ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) → ((𝑋‘𝑥) = 0 ∨ (𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 ))) |
122 | 102, 121 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋‘𝑥) = 0 ∨ (𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 )) |
123 | 64, 73, 122 | mpjaod 849 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 ) |
124 | 123 | mpteq2dva 4979 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ 0 )) |
125 | 124 | oveq2d 6938 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))))) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ 0 ))) |
126 | 4 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑅 ∈ Ring) |
127 | | ringmnd 18943 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
128 | 126, 127 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑅 ∈ Mnd) |
129 | 39 | psrbaglefi 19769 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ∈ Fin) |
130 | 51, 44, 129 | syl2an 589 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ∈ Fin) |
131 | 16 | gsumz 17760 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ∈ Fin) → (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ 0 )) = 0 ) |
132 | 128, 130,
131 | syl2anc 579 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ 0 )) = 0 ) |
133 | 46, 125, 132 | 3eqtrd 2818 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → ((𝑋(.r‘𝑆)𝑌)‘𝑘) = 0 ) |
134 | 40, 133 | suppss 7607 |
. . 3
⊢ (𝜑 → ((𝑋(.r‘𝑆)𝑌) supp 0 ) ⊆ 𝐴) |
135 | | suppssfifsupp 8578 |
. . 3
⊢ ((((𝑋(.r‘𝑆)𝑌) ∈ V ∧ Fun (𝑋(.r‘𝑆)𝑌) ∧ 0 ∈ V) ∧ (𝐴 ∈ Fin ∧ ((𝑋(.r‘𝑆)𝑌) supp 0 ) ⊆ 𝐴)) → (𝑋(.r‘𝑆)𝑌) finSupp 0 ) |
136 | 13, 15, 18, 37, 134, 135 | syl32anc 1446 |
. 2
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) finSupp 0 ) |
137 | 5, 1, 2, 16, 6 | mplelbas 19827 |
. 2
⊢ ((𝑋(.r‘𝑆)𝑌) ∈ 𝑈 ↔ ((𝑋(.r‘𝑆)𝑌) ∈ (Base‘𝑆) ∧ (𝑋(.r‘𝑆)𝑌) finSupp 0 )) |
138 | 12, 136, 137 | sylanbrc 578 |
1
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) ∈ 𝑈) |