Step | Hyp | Ref
| Expression |
1 | | mplsubg.s |
. . 3
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | eqid 2610 |
. . 3
⊢
(Base‘𝑆) =
(Base‘𝑆) |
3 | | eqid 2610 |
. . 3
⊢
(.r‘𝑆) = (.r‘𝑆) |
4 | | mpllss.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
5 | | mplsubg.p |
. . . . 5
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
6 | | mplsubg.u |
. . . . 5
⊢ 𝑈 = (Base‘𝑃) |
7 | 5, 1, 6, 2 | mplbasss 19253 |
. . . 4
⊢ 𝑈 ⊆ (Base‘𝑆) |
8 | | mplsubrglem.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
9 | 7, 8 | sseldi 3566 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (Base‘𝑆)) |
10 | | mplsubrglem.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑈) |
11 | 7, 10 | sseldi 3566 |
. . 3
⊢ (𝜑 → 𝑌 ∈ (Base‘𝑆)) |
12 | 1, 2, 3, 4, 9, 11 | psrmulcl 19209 |
. 2
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) ∈ (Base‘𝑆)) |
13 | | ovex 6577 |
. . . 4
⊢ (𝑋(.r‘𝑆)𝑌) ∈ V |
14 | 13 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) ∈ V) |
15 | 1, 2 | psrelbasfun 19201 |
. . . 4
⊢ ((𝑋(.r‘𝑆)𝑌) ∈ (Base‘𝑆) → Fun (𝑋(.r‘𝑆)𝑌)) |
16 | 12, 15 | syl 17 |
. . 3
⊢ (𝜑 → Fun (𝑋(.r‘𝑆)𝑌)) |
17 | | mplsubrglem.z |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
18 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝑅) ∈ V |
19 | 17, 18 | eqeltri 2684 |
. . . 4
⊢ 0 ∈
V |
20 | 19 | a1i 11 |
. . 3
⊢ (𝜑 → 0 ∈ V) |
21 | | mplsubrglem.p |
. . . . 5
⊢ 𝐴 = ( ∘𝑓
+ “ ((𝑋 supp 0 ) ×
(𝑌 supp 0 ))) |
22 | | df-ima 5051 |
. . . . 5
⊢ (
∘𝑓 + “ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) = ran (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) |
23 | 21, 22 | eqtri 2632 |
. . . 4
⊢ 𝐴 = ran (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) |
24 | 5, 1, 2, 17, 6 | mplelbas 19251 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ (Base‘𝑆) ∧ 𝑋 finSupp 0 )) |
25 | 24 | simprbi 479 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑈 → 𝑋 finSupp 0 ) |
26 | 8, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑋 finSupp 0 ) |
27 | 5, 1, 2, 17, 6 | mplelbas 19251 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝑈 ↔ (𝑌 ∈ (Base‘𝑆) ∧ 𝑌 finSupp 0 )) |
28 | 27 | simprbi 479 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑈 → 𝑌 finSupp 0 ) |
29 | 10, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑌 finSupp 0 ) |
30 | | fsuppxpfi 8175 |
. . . . . 6
⊢ ((𝑋 finSupp 0 ∧ 𝑌 finSupp 0 ) → ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∈
Fin) |
31 | 26, 29, 30 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∈
Fin) |
32 | | ofmres 7055 |
. . . . . . 7
⊢ (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) = (𝑓 ∈ (𝑋 supp 0 ), 𝑔 ∈ (𝑌 supp 0 ) ↦ (𝑓 ∘𝑓 +
𝑔)) |
33 | | ovex 6577 |
. . . . . . 7
⊢ (𝑓 ∘𝑓 +
𝑔) ∈
V |
34 | 32, 33 | fnmpt2i 7128 |
. . . . . 6
⊢ (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) |
35 | | dffn4 6034 |
. . . . . 6
⊢ ((
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) ↔ (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))):((𝑋 supp 0 ) × (𝑌 supp 0 ))–onto→ran ( ∘𝑓 + ↾
((𝑋 supp 0 ) × (𝑌 supp 0 )))) |
36 | 34, 35 | mpbi 219 |
. . . . 5
⊢ (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))):((𝑋 supp 0 ) × (𝑌 supp 0 ))–onto→ran ( ∘𝑓 + ↾
((𝑋 supp 0 ) × (𝑌 supp 0 ))) |
37 | | fofi 8135 |
. . . . 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) |
38 | 31, 36, 37 | sylancl 693 |
. . . 4
⊢ (𝜑 → ran (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) ∈
Fin) |
39 | 23, 38 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
40 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
41 | | mplsubrglem.d |
. . . . 5
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
42 | 1, 40, 41, 2, 12 | psrelbas 19200 |
. . . 4
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌):𝐷⟶(Base‘𝑅)) |
43 | | mplsubrglem.t |
. . . . . 6
⊢ · =
(.r‘𝑅) |
44 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑋 ∈ (Base‘𝑆)) |
45 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑌 ∈ (Base‘𝑆)) |
46 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑘 ∈ (𝐷 ∖ 𝐴) → 𝑘 ∈ 𝐷) |
47 | 46 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑘 ∈ 𝐷) |
48 | 1, 2, 43, 3, 41, 44, 45, 47 | psrmulval 19207 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → ((𝑋(.r‘𝑆)𝑌)‘𝑘) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥)))))) |
49 | 4 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑅 ∈ Ring) |
50 | 5, 40, 6, 41, 10 | mplelf 19254 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) |
51 | 50 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅)) |
52 | | ssrab2 3650 |
. . . . . . . . . . . 12
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ⊆ 𝐷 |
53 | | mplsubg.i |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
54 | 53 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝐼 ∈ 𝑊) |
55 | 47 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑘 ∈ 𝐷) |
56 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) |
57 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} |
58 | 41, 57 | psrbagconcl 19194 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) |
59 | 54, 55, 56, 58 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) |
60 | 52, 59 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑥) ∈ 𝐷) |
61 | 51, 60 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) ∈ (Base‘𝑅)) |
62 | 40, 43, 17 | ringlz 18410 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑌‘(𝑘 ∘𝑓 − 𝑥)) ∈ (Base‘𝑅)) → ( 0 · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 ) |
63 | 49, 61, 62 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ( 0 · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 ) |
64 | | oveq1 6556 |
. . . . . . . . . 10
⊢ ((𝑋‘𝑥) = 0 → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = ( 0 · (𝑌‘(𝑘 ∘𝑓 − 𝑥)))) |
65 | 64 | eqeq1d 2612 |
. . . . . . . . 9
⊢ ((𝑋‘𝑥) = 0 → (((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 ↔ ( 0 · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 )) |
66 | 63, 65 | syl5ibrcom 236 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋‘𝑥) = 0 → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 )) |
67 | 5, 40, 6, 41, 8 | mplelf 19254 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
68 | 67 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅)) |
69 | 52, 56 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥 ∈ 𝐷) |
70 | 68, 69 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
71 | 40, 43, 17 | ringrz 18411 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑥) ∈ (Base‘𝑅)) → ((𝑋‘𝑥) · 0 ) = 0 ) |
72 | 49, 70, 71 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋‘𝑥) · 0 ) = 0 ) |
73 | | oveq2 6557 |
. . . . . . . . . 10
⊢ ((𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = ((𝑋‘𝑥) · 0 )) |
74 | 73 | eqeq1d 2612 |
. . . . . . . . 9
⊢ ((𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 → (((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 ↔ ((𝑋‘𝑥) · 0 ) = 0 )) |
75 | 72, 74 | syl5ibrcom 236 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 )) |
76 | 41 | psrbagf 19186 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑥 ∈ 𝐷) → 𝑥:𝐼⟶ℕ0) |
77 | 54, 69, 76 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥:𝐼⟶ℕ0) |
78 | 77 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑛 ∈ 𝐼) → (𝑥‘𝑛) ∈
ℕ0) |
79 | 41 | psrbagf 19186 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷) → 𝑘:𝐼⟶ℕ0) |
80 | 54, 55, 79 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑘:𝐼⟶ℕ0) |
81 | 80 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑛 ∈ 𝐼) → (𝑘‘𝑛) ∈
ℕ0) |
82 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥‘𝑛) ∈ ℕ0 → (𝑥‘𝑛) ∈ ℂ) |
83 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘‘𝑛) ∈ ℕ0 → (𝑘‘𝑛) ∈ ℂ) |
84 | | pncan3 10168 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥‘𝑛) ∈ ℂ ∧ (𝑘‘𝑛) ∈ ℂ) → ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛))) = (𝑘‘𝑛)) |
85 | 82, 83, 84 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥‘𝑛) ∈ ℕ0 ∧ (𝑘‘𝑛) ∈ ℕ0) → ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛))) = (𝑘‘𝑛)) |
86 | 78, 81, 85 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑛 ∈ 𝐼) → ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛))) = (𝑘‘𝑛)) |
87 | 86 | mpteq2dva 4672 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑛 ∈ 𝐼 ↦ ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑘‘𝑛))) |
88 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘‘𝑛) − (𝑥‘𝑛)) ∈ V |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑛 ∈ 𝐼) → ((𝑘‘𝑛) − (𝑥‘𝑛)) ∈ V) |
90 | 77 | feqmptd 6159 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥 = (𝑛 ∈ 𝐼 ↦ (𝑥‘𝑛))) |
91 | 80 | feqmptd 6159 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑘 = (𝑛 ∈ 𝐼 ↦ (𝑘‘𝑛))) |
92 | 54, 81, 78, 91, 90 | offval2 6812 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑥) = (𝑛 ∈ 𝐼 ↦ ((𝑘‘𝑛) − (𝑥‘𝑛)))) |
93 | 54, 78, 89, 90, 92 | offval2 6812 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑥 ∘𝑓 + (𝑘 ∘𝑓
− 𝑥)) = (𝑛 ∈ 𝐼 ↦ ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛))))) |
94 | 87, 93, 91 | 3eqtr4d 2654 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑥 ∘𝑓 + (𝑘 ∘𝑓
− 𝑥)) = 𝑘) |
95 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑘 ∈ (𝐷 ∖ 𝐴)) |
96 | 94, 95 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑥 ∘𝑓 + (𝑘 ∘𝑓
− 𝑥)) ∈ (𝐷 ∖ 𝐴)) |
97 | 96 | eldifbd 3553 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ¬ (𝑥 ∘𝑓 +
(𝑘
∘𝑓 − 𝑥)) ∈ 𝐴) |
98 | | ovres 6698 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘𝑓 +
↾ ((𝑋 supp 0 ) ×
(𝑌 supp 0 )))(𝑘 ∘𝑓 − 𝑥)) = (𝑥 ∘𝑓 + (𝑘 ∘𝑓
− 𝑥))) |
99 | | fnovrn 6707 |
. . . . . . . . . . . . . 14
⊢ (((
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∧ 𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘𝑓 +
↾ ((𝑋 supp 0 ) ×
(𝑌 supp 0 )))(𝑘 ∘𝑓 − 𝑥)) ∈ ran (
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))) |
100 | 99, 23 | syl6eleqr 2699 |
. . . . . . . . . . . . 13
⊢ (((
∘𝑓 + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∧ 𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘𝑓 +
↾ ((𝑋 supp 0 ) ×
(𝑌 supp 0 )))(𝑘 ∘𝑓 − 𝑥)) ∈ 𝐴) |
101 | 34, 100 | mp3an1 1403 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘𝑓 +
↾ ((𝑋 supp 0 ) ×
(𝑌 supp 0 )))(𝑘 ∘𝑓 − 𝑥)) ∈ 𝐴) |
102 | 98, 101 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) → (𝑥 ∘𝑓 +
(𝑘
∘𝑓 − 𝑥)) ∈ 𝐴) |
103 | 97, 102 | nsyl 134 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ¬ (𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 ))) |
104 | | ianor 508 |
. . . . . . . . . 10
⊢ (¬
(𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) ↔ (¬ 𝑥 ∈ (𝑋 supp 0 ) ∨ ¬ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 ))) |
105 | 103, 104 | sylib 207 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (¬ 𝑥 ∈ (𝑋 supp 0 ) ∨ ¬ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 ))) |
106 | | eldif 3550 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ (𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ (𝑋 supp 0 ))) |
107 | 106 | baib 942 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ ¬ 𝑥 ∈ (𝑋 supp 0 ))) |
108 | 69, 107 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ ¬ 𝑥 ∈ (𝑋 supp 0 ))) |
109 | | ssid 3587 |
. . . . . . . . . . . . . 14
⊢ (𝑋 supp 0 ) ⊆ (𝑋 supp 0 ) |
110 | 109 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑋 supp 0 ) ⊆ (𝑋 supp 0 )) |
111 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
112 | 41, 111 | rabex2 4742 |
. . . . . . . . . . . . . 14
⊢ 𝐷 ∈ V |
113 | 112 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝐷 ∈ V) |
114 | 19 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 0 ∈ V) |
115 | 68, 110, 113, 114 | suppssr 7213 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋‘𝑥) = 0 ) |
116 | 115 | ex 449 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) → (𝑋‘𝑥) = 0 )) |
117 | 108, 116 | sylbird 249 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (¬ 𝑥 ∈ (𝑋 supp 0 ) → (𝑋‘𝑥) = 0 )) |
118 | | eldif 3550 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∘𝑓
− 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) ↔ ((𝑘 ∘𝑓
− 𝑥) ∈ 𝐷 ∧ ¬ (𝑘 ∘𝑓 − 𝑥) ∈ (𝑌 supp 0 ))) |
119 | 118 | baib 942 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∘𝑓
− 𝑥) ∈ 𝐷 → ((𝑘 ∘𝑓 − 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) ↔ ¬ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 ))) |
120 | 60, 119 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑘 ∘𝑓 − 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) ↔ ¬ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 ))) |
121 | | ssid 3587 |
. . . . . . . . . . . . . 14
⊢ (𝑌 supp 0 ) ⊆ (𝑌 supp 0 ) |
122 | 121 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑌 supp 0 ) ⊆ (𝑌 supp 0 )) |
123 | 51, 122, 113, 114 | suppssr 7213 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ (𝑘 ∘𝑓 − 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 ))) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 ) |
124 | 123 | ex 449 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑘 ∘𝑓 − 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 )) |
125 | 120, 124 | sylbird 249 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (¬ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 ) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 )) |
126 | 117, 125 | orim12d 879 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((¬ 𝑥 ∈ (𝑋 supp 0 ) ∨ ¬ (𝑘 ∘𝑓
− 𝑥) ∈ (𝑌 supp 0 )) → ((𝑋‘𝑥) = 0 ∨ (𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 ))) |
127 | 105, 126 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋‘𝑥) = 0 ∨ (𝑌‘(𝑘 ∘𝑓 − 𝑥)) = 0 )) |
128 | 66, 75, 127 | mpjaod 395 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))) = 0 ) |
129 | 128 | mpteq2dva 4672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ 0 )) |
130 | 129 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘𝑓 − 𝑥))))) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ 0 ))) |
131 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑅 ∈ Ring) |
132 | | ringmnd 18379 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
133 | 131, 132 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑅 ∈ Mnd) |
134 | 41 | psrbaglefi 19193 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ∈ Fin) |
135 | 53, 46, 134 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ∈ Fin) |
136 | 17 | gsumz 17197 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ∈ Fin) → (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ 0 )) = 0 ) |
137 | 133, 135,
136 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ 0 )) = 0 ) |
138 | 48, 130, 137 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → ((𝑋(.r‘𝑆)𝑌)‘𝑘) = 0 ) |
139 | 42, 138 | suppss 7212 |
. . 3
⊢ (𝜑 → ((𝑋(.r‘𝑆)𝑌) supp 0 ) ⊆ 𝐴) |
140 | | suppssfifsupp 8173 |
. . 3
⊢ ((((𝑋(.r‘𝑆)𝑌) ∈ V ∧ Fun (𝑋(.r‘𝑆)𝑌) ∧ 0 ∈ V) ∧ (𝐴 ∈ Fin ∧ ((𝑋(.r‘𝑆)𝑌) supp 0 ) ⊆ 𝐴)) → (𝑋(.r‘𝑆)𝑌) finSupp 0 ) |
141 | 14, 16, 20, 39, 139, 140 | syl32anc 1326 |
. 2
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) finSupp 0 ) |
142 | 5, 1, 2, 17, 6 | mplelbas 19251 |
. 2
⊢ ((𝑋(.r‘𝑆)𝑌) ∈ 𝑈 ↔ ((𝑋(.r‘𝑆)𝑌) ∈ (Base‘𝑆) ∧ (𝑋(.r‘𝑆)𝑌) finSupp 0 )) |
143 | 12, 141, 142 | sylanbrc 695 |
1
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) ∈ 𝑈) |