Step | Hyp | Ref
| Expression |
1 | | mplsubg.s |
. . 3
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | eqid 2739 |
. . 3
⊢
(Base‘𝑆) =
(Base‘𝑆) |
3 | | eqid 2739 |
. . 3
⊢
(.r‘𝑆) = (.r‘𝑆) |
4 | | mpllss.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
5 | | mplsubg.p |
. . . . 5
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
6 | | mplsubg.u |
. . . . 5
⊢ 𝑈 = (Base‘𝑃) |
7 | 5, 1, 6, 2 | mplbasss 20991 |
. . . 4
⊢ 𝑈 ⊆ (Base‘𝑆) |
8 | | mplsubrglem.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
9 | 7, 8 | sselid 3915 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (Base‘𝑆)) |
10 | | mplsubrglem.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑈) |
11 | 7, 10 | sselid 3915 |
. . 3
⊢ (𝜑 → 𝑌 ∈ (Base‘𝑆)) |
12 | 1, 2, 3, 4, 9, 11 | psrmulcl 20945 |
. 2
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) ∈ (Base‘𝑆)) |
13 | | ovexd 7270 |
. . 3
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) ∈ V) |
14 | 1, 2 | psrelbasfun 20937 |
. . . 4
⊢ ((𝑋(.r‘𝑆)𝑌) ∈ (Base‘𝑆) → Fun (𝑋(.r‘𝑆)𝑌)) |
15 | 12, 14 | syl 17 |
. . 3
⊢ (𝜑 → Fun (𝑋(.r‘𝑆)𝑌)) |
16 | | mplsubrglem.z |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
17 | 16 | fvexi 6753 |
. . . 4
⊢ 0 ∈
V |
18 | 17 | a1i 11 |
. . 3
⊢ (𝜑 → 0 ∈ V) |
19 | | mplsubrglem.p |
. . . . 5
⊢ 𝐴 = ( ∘f +
“ ((𝑋 supp 0 ) ×
(𝑌 supp 0 ))) |
20 | | df-ima 5582 |
. . . . 5
⊢ (
∘f + “ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) = ran (
∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) |
21 | 19, 20 | eqtri 2767 |
. . . 4
⊢ 𝐴 = ran ( ∘f +
↾ ((𝑋 supp 0 ) ×
(𝑌 supp 0 ))) |
22 | 5, 1, 2, 16, 6 | mplelbas 20987 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ (Base‘𝑆) ∧ 𝑋 finSupp 0 )) |
23 | 22 | simprbi 500 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑈 → 𝑋 finSupp 0 ) |
24 | 8, 23 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑋 finSupp 0 ) |
25 | 5, 1, 2, 16, 6 | mplelbas 20987 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝑈 ↔ (𝑌 ∈ (Base‘𝑆) ∧ 𝑌 finSupp 0 )) |
26 | 25 | simprbi 500 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑈 → 𝑌 finSupp 0 ) |
27 | 10, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑌 finSupp 0 ) |
28 | | fsuppxpfi 9032 |
. . . . . 6
⊢ ((𝑋 finSupp 0 ∧ 𝑌 finSupp 0 ) → ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∈
Fin) |
29 | 24, 27, 28 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∈
Fin) |
30 | | ofmres 7779 |
. . . . . . 7
⊢ (
∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) = (𝑓 ∈ (𝑋 supp 0 ), 𝑔 ∈ (𝑌 supp 0 ) ↦ (𝑓 ∘f + 𝑔)) |
31 | | ovex 7268 |
. . . . . . 7
⊢ (𝑓 ∘f + 𝑔) ∈ V |
32 | 30, 31 | fnmpoi 7862 |
. . . . . 6
⊢ (
∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) |
33 | | dffn4 6661 |
. . . . . 6
⊢ ((
∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) ↔ (
∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))):((𝑋 supp 0 ) × (𝑌 supp 0 ))–onto→ran ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))) |
34 | 32, 33 | mpbi 233 |
. . . . 5
⊢ (
∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))):((𝑋 supp 0 ) × (𝑌 supp 0 ))–onto→ran ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) |
35 | | fofi 8992 |
. . . . 5
⊢ ((((𝑋 supp 0 ) × (𝑌 supp 0 )) ∈ Fin ∧ (
∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))):((𝑋 supp 0 ) × (𝑌 supp 0 ))–onto→ran ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))) → ran (
∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) ∈
Fin) |
36 | 29, 34, 35 | sylancl 589 |
. . . 4
⊢ (𝜑 → ran ( ∘f
+ ↾ ((𝑋 supp 0 ) ×
(𝑌 supp 0 ))) ∈
Fin) |
37 | 21, 36 | eqeltrid 2844 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
38 | | eqid 2739 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
39 | | mplsubrglem.d |
. . . . 5
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
40 | 1, 38, 39, 2, 12 | psrelbas 20936 |
. . . 4
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌):𝐷⟶(Base‘𝑅)) |
41 | | mplsubrglem.t |
. . . . . 6
⊢ · =
(.r‘𝑅) |
42 | 9 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑋 ∈ (Base‘𝑆)) |
43 | 11 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑌 ∈ (Base‘𝑆)) |
44 | | eldifi 4058 |
. . . . . . 7
⊢ (𝑘 ∈ (𝐷 ∖ 𝐴) → 𝑘 ∈ 𝐷) |
45 | 44 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑘 ∈ 𝐷) |
46 | 1, 2, 41, 3, 39, 42, 43, 45 | psrmulval 20943 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → ((𝑋(.r‘𝑆)𝑌)‘𝑘) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘f − 𝑥)))))) |
47 | 4 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑅 ∈ Ring) |
48 | 5, 38, 6, 39, 10 | mplelf 20992 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) |
49 | 48 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅)) |
50 | | ssrab2 4010 |
. . . . . . . . . . . 12
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ⊆ 𝐷 |
51 | 45 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑘 ∈ 𝐷) |
52 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
53 | | eqid 2739 |
. . . . . . . . . . . . . 14
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} |
54 | 39, 53 | psrbagconcl 20925 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
55 | 51, 52, 54 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
56 | 50, 55 | sselid 3915 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ 𝐷) |
57 | 49, 56 | ffvelrnd 6927 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) |
58 | 38, 41, 16 | ringlz 19638 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) → ( 0 · (𝑌‘(𝑘 ∘f − 𝑥))) = 0 ) |
59 | 47, 57, 58 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ( 0 · (𝑌‘(𝑘 ∘f − 𝑥))) = 0 ) |
60 | | oveq1 7242 |
. . . . . . . . . 10
⊢ ((𝑋‘𝑥) = 0 → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘f − 𝑥))) = ( 0 · (𝑌‘(𝑘 ∘f − 𝑥)))) |
61 | 60 | eqeq1d 2741 |
. . . . . . . . 9
⊢ ((𝑋‘𝑥) = 0 → (((𝑋‘𝑥) · (𝑌‘(𝑘 ∘f − 𝑥))) = 0 ↔ ( 0 · (𝑌‘(𝑘 ∘f − 𝑥))) = 0 )) |
62 | 59, 61 | syl5ibrcom 250 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥) = 0 → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘f − 𝑥))) = 0 )) |
63 | 5, 38, 6, 39, 8 | mplelf 20992 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
64 | 63 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅)) |
65 | 50, 52 | sselid 3915 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ 𝐷) |
66 | 64, 65 | ffvelrnd 6927 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
67 | 38, 41, 16 | ringrz 19639 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑥) ∈ (Base‘𝑅)) → ((𝑋‘𝑥) · 0 ) = 0 ) |
68 | 47, 66, 67 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥) · 0 ) = 0 ) |
69 | | oveq2 7243 |
. . . . . . . . . 10
⊢ ((𝑌‘(𝑘 ∘f − 𝑥)) = 0 → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘f − 𝑥))) = ((𝑋‘𝑥) · 0 )) |
70 | 69 | eqeq1d 2741 |
. . . . . . . . 9
⊢ ((𝑌‘(𝑘 ∘f − 𝑥)) = 0 → (((𝑋‘𝑥) · (𝑌‘(𝑘 ∘f − 𝑥))) = 0 ↔ ((𝑋‘𝑥) · 0 ) = 0 )) |
71 | 68, 70 | syl5ibrcom 250 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑌‘(𝑘 ∘f − 𝑥)) = 0 → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘f − 𝑥))) = 0 )) |
72 | 39 | psrbagf 20909 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐷 → 𝑥:𝐼⟶ℕ0) |
73 | 65, 72 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥:𝐼⟶ℕ0) |
74 | 73 | ffvelrnda 6926 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ 𝑛 ∈ 𝐼) → (𝑥‘𝑛) ∈
ℕ0) |
75 | 39 | psrbagf 20909 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝐷 → 𝑘:𝐼⟶ℕ0) |
76 | 51, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑘:𝐼⟶ℕ0) |
77 | 76 | ffvelrnda 6926 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ 𝑛 ∈ 𝐼) → (𝑘‘𝑛) ∈
ℕ0) |
78 | | nn0cn 12130 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥‘𝑛) ∈ ℕ0 → (𝑥‘𝑛) ∈ ℂ) |
79 | | nn0cn 12130 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘‘𝑛) ∈ ℕ0 → (𝑘‘𝑛) ∈ ℂ) |
80 | | pncan3 11116 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥‘𝑛) ∈ ℂ ∧ (𝑘‘𝑛) ∈ ℂ) → ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛))) = (𝑘‘𝑛)) |
81 | 78, 79, 80 | syl2an 599 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥‘𝑛) ∈ ℕ0 ∧ (𝑘‘𝑛) ∈ ℕ0) → ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛))) = (𝑘‘𝑛)) |
82 | 74, 77, 81 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ 𝑛 ∈ 𝐼) → ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛))) = (𝑘‘𝑛)) |
83 | 82 | mpteq2dva 5167 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑛 ∈ 𝐼 ↦ ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑘‘𝑛))) |
84 | | mplsubg.i |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
85 | 84 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝐼 ∈ 𝑊) |
86 | | ovexd 7270 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ 𝑛 ∈ 𝐼) → ((𝑘‘𝑛) − (𝑥‘𝑛)) ∈ V) |
87 | 73 | feqmptd 6802 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 = (𝑛 ∈ 𝐼 ↦ (𝑥‘𝑛))) |
88 | 76 | feqmptd 6802 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑘 = (𝑛 ∈ 𝐼 ↦ (𝑘‘𝑛))) |
89 | 85, 77, 74, 88, 87 | offval2 7510 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) = (𝑛 ∈ 𝐼 ↦ ((𝑘‘𝑛) − (𝑥‘𝑛)))) |
90 | 85, 74, 86, 87, 89 | offval2 7510 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑥 ∘f + (𝑘 ∘f − 𝑥)) = (𝑛 ∈ 𝐼 ↦ ((𝑥‘𝑛) + ((𝑘‘𝑛) − (𝑥‘𝑛))))) |
91 | 83, 90, 88 | 3eqtr4d 2789 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑥 ∘f + (𝑘 ∘f − 𝑥)) = 𝑘) |
92 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑘 ∈ (𝐷 ∖ 𝐴)) |
93 | 91, 92 | eqeltrd 2840 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑥 ∘f + (𝑘 ∘f − 𝑥)) ∈ (𝐷 ∖ 𝐴)) |
94 | 93 | eldifbd 3896 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ¬ (𝑥 ∘f + (𝑘 ∘f − 𝑥)) ∈ 𝐴) |
95 | | ovres 7396 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘f −
𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘f + ↾
((𝑋 supp 0 ) × (𝑌 supp 0 )))(𝑘 ∘f − 𝑥)) = (𝑥 ∘f + (𝑘 ∘f − 𝑥))) |
96 | | fnovrn 7405 |
. . . . . . . . . . . . . 14
⊢ (((
∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∧ 𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘f −
𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘f + ↾
((𝑋 supp 0 ) × (𝑌 supp 0 )))(𝑘 ∘f − 𝑥)) ∈ ran (
∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))) |
97 | 96, 21 | eleqtrrdi 2851 |
. . . . . . . . . . . . 13
⊢ (((
∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∧ 𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘f −
𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘f + ↾
((𝑋 supp 0 ) × (𝑌 supp 0 )))(𝑘 ∘f − 𝑥)) ∈ 𝐴) |
98 | 32, 97 | mp3an1 1450 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘f −
𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘f + ↾
((𝑋 supp 0 ) × (𝑌 supp 0 )))(𝑘 ∘f − 𝑥)) ∈ 𝐴) |
99 | 95, 98 | eqeltrrd 2841 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘f −
𝑥) ∈ (𝑌 supp 0 )) → (𝑥 ∘f + (𝑘 ∘f −
𝑥)) ∈ 𝐴) |
100 | 94, 99 | nsyl 142 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ¬ (𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘f −
𝑥) ∈ (𝑌 supp 0 ))) |
101 | | ianor 982 |
. . . . . . . . . 10
⊢ (¬
(𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘 ∘f −
𝑥) ∈ (𝑌 supp 0 )) ↔ (¬ 𝑥 ∈ (𝑋 supp 0 ) ∨ ¬ (𝑘 ∘f −
𝑥) ∈ (𝑌 supp 0 ))) |
102 | 100, 101 | sylib 221 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (¬ 𝑥 ∈ (𝑋 supp 0 ) ∨ ¬ (𝑘 ∘f −
𝑥) ∈ (𝑌 supp 0 ))) |
103 | | eldif 3893 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ (𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ (𝑋 supp 0 ))) |
104 | 103 | baib 539 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ ¬ 𝑥 ∈ (𝑋 supp 0 ))) |
105 | 65, 104 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ ¬ 𝑥 ∈ (𝑋 supp 0 ))) |
106 | | ssidd 3941 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑋 supp 0 ) ⊆ (𝑋 supp 0 )) |
107 | | ovex 7268 |
. . . . . . . . . . . . . . 15
⊢
(ℕ0 ↑m 𝐼) ∈ V |
108 | 39, 107 | rabex2 5244 |
. . . . . . . . . . . . . 14
⊢ 𝐷 ∈ V |
109 | 108 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝐷 ∈ V) |
110 | 17 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 0 ∈ V) |
111 | 64, 106, 109, 110 | suppssr 7962 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ 𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋‘𝑥) = 0 ) |
112 | 111 | ex 416 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) → (𝑋‘𝑥) = 0 )) |
113 | 105, 112 | sylbird 263 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (¬ 𝑥 ∈ (𝑋 supp 0 ) → (𝑋‘𝑥) = 0 )) |
114 | | eldif 3893 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∘f −
𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) ↔ ((𝑘 ∘f −
𝑥) ∈ 𝐷 ∧ ¬ (𝑘 ∘f − 𝑥) ∈ (𝑌 supp 0 ))) |
115 | 114 | baib 539 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∘f −
𝑥) ∈ 𝐷 → ((𝑘 ∘f − 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) ↔ ¬ (𝑘 ∘f −
𝑥) ∈ (𝑌 supp 0 ))) |
116 | 56, 115 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑘 ∘f − 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) ↔ ¬ (𝑘 ∘f −
𝑥) ∈ (𝑌 supp 0 ))) |
117 | | ssidd 3941 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑌 supp 0 ) ⊆ (𝑌 supp 0 )) |
118 | 49, 117, 109, 110 | suppssr 7962 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ (𝑘 ∘f − 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 ))) → (𝑌‘(𝑘 ∘f − 𝑥)) = 0 ) |
119 | 118 | ex 416 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑘 ∘f − 𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) → (𝑌‘(𝑘 ∘f − 𝑥)) = 0 )) |
120 | 116, 119 | sylbird 263 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (¬ (𝑘 ∘f − 𝑥) ∈ (𝑌 supp 0 ) → (𝑌‘(𝑘 ∘f − 𝑥)) = 0 )) |
121 | 113, 120 | orim12d 965 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((¬ 𝑥 ∈ (𝑋 supp 0 ) ∨ ¬ (𝑘 ∘f −
𝑥) ∈ (𝑌 supp 0 )) → ((𝑋‘𝑥) = 0 ∨ (𝑌‘(𝑘 ∘f − 𝑥)) = 0 ))) |
122 | 102, 121 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥) = 0 ∨ (𝑌‘(𝑘 ∘f − 𝑥)) = 0 )) |
123 | 62, 71, 122 | mpjaod 860 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘f − 𝑥))) = 0 ) |
124 | 123 | mpteq2dva 5167 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ 0 )) |
125 | 124 | oveq2d 7251 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥) · (𝑌‘(𝑘 ∘f − 𝑥))))) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ 0 ))) |
126 | 4 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑅 ∈ Ring) |
127 | | ringmnd 19605 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
128 | 126, 127 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → 𝑅 ∈ Mnd) |
129 | 39 | psrbaglefi 20923 |
. . . . . . 7
⊢ (𝑘 ∈ 𝐷 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
130 | 45, 129 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
131 | 16 | gsumz 18295 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ 0 )) = 0 ) |
132 | 128, 130,
131 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ 0 )) = 0 ) |
133 | 46, 125, 132 | 3eqtrd 2783 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ 𝐴)) → ((𝑋(.r‘𝑆)𝑌)‘𝑘) = 0 ) |
134 | 40, 133 | suppss 7960 |
. . 3
⊢ (𝜑 → ((𝑋(.r‘𝑆)𝑌) supp 0 ) ⊆ 𝐴) |
135 | | suppssfifsupp 9030 |
. . 3
⊢ ((((𝑋(.r‘𝑆)𝑌) ∈ V ∧ Fun (𝑋(.r‘𝑆)𝑌) ∧ 0 ∈ V) ∧ (𝐴 ∈ Fin ∧ ((𝑋(.r‘𝑆)𝑌) supp 0 ) ⊆ 𝐴)) → (𝑋(.r‘𝑆)𝑌) finSupp 0 ) |
136 | 13, 15, 18, 37, 134, 135 | syl32anc 1380 |
. 2
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) finSupp 0 ) |
137 | 5, 1, 2, 16, 6 | mplelbas 20987 |
. 2
⊢ ((𝑋(.r‘𝑆)𝑌) ∈ 𝑈 ↔ ((𝑋(.r‘𝑆)𝑌) ∈ (Base‘𝑆) ∧ (𝑋(.r‘𝑆)𝑌) finSupp 0 )) |
138 | 12, 136, 137 | sylanbrc 586 |
1
⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) ∈ 𝑈) |