Step | Hyp | Ref
| Expression |
1 | | psrring.s |
. . . 4
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | eqid 2622 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | psr1cl.d |
. . . 4
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
4 | | psr1cl.b |
. . . 4
⊢ 𝐵 = (Base‘𝑆) |
5 | | psrlidm.t |
. . . . 5
⊢ · =
(.r‘𝑆) |
6 | | psrring.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
7 | | psrring.i |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
8 | | psr1cl.z |
. . . . . 6
⊢ 0 =
(0g‘𝑅) |
9 | | psr1cl.o |
. . . . . 6
⊢ 1 =
(1r‘𝑅) |
10 | | psr1cl.u |
. . . . . 6
⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 )) |
11 | 1, 7, 6, 3, 8, 9, 10, 4 | psr1cl 19402 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝐵) |
12 | | psrlidm.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
13 | 1, 4, 5, 6, 11, 12 | psrmulcl 19388 |
. . . 4
⊢ (𝜑 → (𝑈 · 𝑋) ∈ 𝐵) |
14 | 1, 2, 3, 4, 13 | psrelbas 19379 |
. . 3
⊢ (𝜑 → (𝑈 · 𝑋):𝐷⟶(Base‘𝑅)) |
15 | 14 | ffnd 6046 |
. 2
⊢ (𝜑 → (𝑈 · 𝑋) Fn 𝐷) |
16 | 1, 2, 3, 4, 12 | psrelbas 19379 |
. . 3
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
17 | 16 | ffnd 6046 |
. 2
⊢ (𝜑 → 𝑋 Fn 𝐷) |
18 | | eqid 2622 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
19 | 11 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈 ∈ 𝐵) |
20 | 12 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑋 ∈ 𝐵) |
21 | | simpr 477 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷) |
22 | 1, 4, 18, 5, 3, 19, 20, 21 | psrmulval 19386 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))))) |
23 | | fconstmpt 5163 |
. . . . . . . . . 10
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) |
24 | 3 | fczpsrbag 19367 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷) |
25 | 7, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷) |
26 | 23, 25 | syl5eqel 2705 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷) |
27 | 26 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ 𝐷) |
28 | 3 | psrbagf 19365 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0) |
29 | 7, 28 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0) |
30 | 29 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) ∈
ℕ0) |
31 | 30 | nn0ge0d 11354 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → 0 ≤ (𝑦‘𝑥)) |
32 | 31 | ralrimiva 2966 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ∀𝑥 ∈ 𝐼 0 ≤ (𝑦‘𝑥)) |
33 | | 0nn0 11307 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
34 | 33 | fconst6 6095 |
. . . . . . . . . . 11
⊢ (𝐼 × {0}):𝐼⟶ℕ0 |
35 | | ffn 6045 |
. . . . . . . . . . 11
⊢ ((𝐼 × {0}):𝐼⟶ℕ0 → (𝐼 × {0}) Fn 𝐼) |
36 | 34, 35 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) Fn 𝐼) |
37 | 29 | ffnd 6046 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 Fn 𝐼) |
38 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐼 ∈ 𝑉) |
39 | | inidm 3822 |
. . . . . . . . . 10
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
40 | 33 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈
ℕ0) |
41 | | fvconst2g 6467 |
. . . . . . . . . . 11
⊢ ((0
∈ ℕ0 ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {0})‘𝑥) = 0) |
42 | 40, 41 | sylan 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {0})‘𝑥) = 0) |
43 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) = (𝑦‘𝑥)) |
44 | 36, 37, 38, 38, 39, 42, 43 | ofrfval 6905 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐼 × {0}) ∘𝑟
≤ 𝑦 ↔ ∀𝑥 ∈ 𝐼 0 ≤ (𝑦‘𝑥))) |
45 | 32, 44 | mpbird 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∘𝑟
≤ 𝑦) |
46 | | breq1 4656 |
. . . . . . . . 9
⊢ (𝑔 = (𝐼 × {0}) → (𝑔 ∘𝑟 ≤ 𝑦 ↔ (𝐼 × {0}) ∘𝑟
≤ 𝑦)) |
47 | 46 | elrab 3363 |
. . . . . . . 8
⊢ ((𝐼 × {0}) ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↔ ((𝐼 × {0}) ∈ 𝐷 ∧ (𝐼 × {0}) ∘𝑟
≤ 𝑦)) |
48 | 27, 45, 47 | sylanbrc 698 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) |
49 | 48 | snssd 4340 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {(𝐼 × {0})} ⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) |
50 | 49 | resmptd 5452 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ↾ {(𝐼 × {0})}) = (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))))) |
51 | 50 | oveq2d 6666 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))))) |
52 | | ringcmn 18581 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
53 | 6, 52 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CMnd) |
54 | 53 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ CMnd) |
55 | | ovex 6678 |
. . . . . . 7
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
56 | 3, 55 | rab2ex 4816 |
. . . . . 6
⊢ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∈ V |
57 | 56 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∈ V) |
58 | 6 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑅 ∈ Ring) |
59 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) |
60 | | breq1 4656 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑧 → (𝑔 ∘𝑟 ≤ 𝑦 ↔ 𝑧 ∘𝑟 ≤ 𝑦)) |
61 | 60 | elrab 3363 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↔ (𝑧 ∈ 𝐷 ∧ 𝑧 ∘𝑟 ≤ 𝑦)) |
62 | 59, 61 | sylib 208 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘𝑟 ≤ 𝑦)) |
63 | 62 | simpld 475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧 ∈ 𝐷) |
64 | 1, 2, 3, 4, 19 | psrelbas 19379 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈:𝐷⟶(Base‘𝑅)) |
65 | 64 | ffvelrnda 6359 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ 𝐷) → (𝑈‘𝑧) ∈ (Base‘𝑅)) |
66 | 63, 65 | syldan 487 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → (𝑈‘𝑧) ∈ (Base‘𝑅)) |
67 | 16 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑋:𝐷⟶(Base‘𝑅)) |
68 | 7 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝐼 ∈ 𝑉) |
69 | 21 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑦 ∈ 𝐷) |
70 | 3 | psrbagf 19365 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐷) → 𝑧:𝐼⟶ℕ0) |
71 | 68, 63, 70 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧:𝐼⟶ℕ0) |
72 | 62 | simprd 479 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧 ∘𝑟 ≤ 𝑦) |
73 | 3 | psrbagcon 19371 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ 𝐷 ∧ 𝑧:𝐼⟶ℕ0 ∧ 𝑧 ∘𝑟
≤ 𝑦)) → ((𝑦 ∘𝑓
− 𝑧) ∈ 𝐷 ∧ (𝑦 ∘𝑓 − 𝑧) ∘𝑟
≤ 𝑦)) |
74 | 68, 69, 71, 72, 73 | syl13anc 1328 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → ((𝑦 ∘𝑓 − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘𝑓 − 𝑧) ∘𝑟
≤ 𝑦)) |
75 | 74 | simpld 475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → (𝑦 ∘𝑓 − 𝑧) ∈ 𝐷) |
76 | 67, 75 | ffvelrnd 6360 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → (𝑋‘(𝑦 ∘𝑓 − 𝑧)) ∈ (Base‘𝑅)) |
77 | 2, 18 | ringcl 18561 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑈‘𝑧) ∈ (Base‘𝑅) ∧ (𝑋‘(𝑦 ∘𝑓 − 𝑧)) ∈ (Base‘𝑅)) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) ∈ (Base‘𝑅)) |
78 | 58, 66, 76, 77 | syl3anc 1326 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) ∈ (Base‘𝑅)) |
79 | | eqid 2622 |
. . . . . 6
⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) = (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) |
80 | 78, 79 | fmptd 6385 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))):{𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}⟶(Base‘𝑅)) |
81 | | eldifi 3732 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) |
82 | 81, 62 | sylan2 491 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘𝑟 ≤ 𝑦)) |
83 | 82 | simpld 475 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → 𝑧 ∈ 𝐷) |
84 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 = (𝐼 × {0}) ↔ 𝑧 = (𝐼 × {0}))) |
85 | 84 | ifbid 4108 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = if(𝑧 = (𝐼 × {0}), 1 , 0 )) |
86 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢
(1r‘𝑅) ∈ V |
87 | 9, 86 | eqeltri 2697 |
. . . . . . . . . . . 12
⊢ 1 ∈
V |
88 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑅) ∈ V |
89 | 8, 88 | eqeltri 2697 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
90 | 87, 89 | ifex 4156 |
. . . . . . . . . . 11
⊢ if(𝑧 = (𝐼 × {0}), 1 , 0 ) ∈
V |
91 | 85, 10, 90 | fvmpt 6282 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐷 → (𝑈‘𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 )) |
92 | 83, 91 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑈‘𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 )) |
93 | | eldifn 3733 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})}) → ¬ 𝑧 ∈ {(𝐼 × {0})}) |
94 | 93 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 ∈ {(𝐼 × {0})}) |
95 | | velsn 4193 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {(𝐼 × {0})} ↔ 𝑧 = (𝐼 × {0})) |
96 | 94, 95 | sylnib 318 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 = (𝐼 × {0})) |
97 | 96 | iffalsed 4097 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → if(𝑧 = (𝐼 × {0}), 1 , 0 ) = 0 ) |
98 | 92, 97 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑈‘𝑧) = 0 ) |
99 | 98 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) = ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) |
100 | 6 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → 𝑅 ∈ Ring) |
101 | 81, 76 | sylan2 491 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑋‘(𝑦 ∘𝑓 − 𝑧)) ∈ (Base‘𝑅)) |
102 | 2, 18, 8 | ringlz 18587 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘(𝑦 ∘𝑓 − 𝑧)) ∈ (Base‘𝑅)) → ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) = 0 ) |
103 | 100, 101,
102 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) = 0 ) |
104 | 99, 103 | eqtrd 2656 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) = 0 ) |
105 | 104, 57 | suppss2 7329 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})}) |
106 | 3, 55 | rabex2 4815 |
. . . . . . . 8
⊢ 𝐷 ∈ V |
107 | 106 | mptrabex 6488 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ∈ V |
108 | 107 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ∈ V) |
109 | | funmpt 5926 |
. . . . . . 7
⊢ Fun
(𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) |
110 | 109 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))))) |
111 | 89 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈ V) |
112 | | snfi 8038 |
. . . . . . 7
⊢ {(𝐼 × {0})} ∈
Fin |
113 | 112 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {(𝐼 × {0})} ∈ Fin) |
114 | | suppssfifsupp 8290 |
. . . . . 6
⊢ ((((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ∈ V ∧ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ∧ 0 ∈ V) ∧ ({(𝐼 × {0})} ∈ Fin ∧
((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})})) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) finSupp 0 ) |
115 | 108, 110,
111, 113, 105, 114 | syl32anc 1334 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) finSupp 0 ) |
116 | 2, 8, 54, 57, 80, 105, 115 | gsumres 18314 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))))) |
117 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Ring) |
118 | | ringmnd 18556 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
119 | 117, 118 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Mnd) |
120 | | iftrue 4092 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐼 × {0}) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = 1 ) |
121 | 120, 10, 87 | fvmpt 6282 |
. . . . . . . . 9
⊢ ((𝐼 × {0}) ∈ 𝐷 → (𝑈‘(𝐼 × {0})) = 1 ) |
122 | 27, 121 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝐼 × {0})) = 1 ) |
123 | | nn0cn 11302 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ0
→ 𝑧 ∈
ℂ) |
124 | 123 | subid1d 10381 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ0
→ (𝑧 − 0) =
𝑧) |
125 | 124 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ℕ0) → (𝑧 − 0) = 𝑧) |
126 | 38, 29, 40, 125 | caofid0r 6926 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑦 ∘𝑓 − (𝐼 × {0})) = 𝑦) |
127 | 126 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘(𝑦 ∘𝑓 − (𝐼 × {0}))) = (𝑋‘𝑦)) |
128 | 122, 127 | oveq12d 6668 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 × {0})))) = ( 1
(.r‘𝑅)(𝑋‘𝑦))) |
129 | 16 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅)) |
130 | 2, 18, 9 | ringlidm 18571 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑦) ∈ (Base‘𝑅)) → ( 1 (.r‘𝑅)(𝑋‘𝑦)) = (𝑋‘𝑦)) |
131 | 117, 129,
130 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ( 1 (.r‘𝑅)(𝑋‘𝑦)) = (𝑋‘𝑦)) |
132 | 128, 131 | eqtrd 2656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 × {0})))) = (𝑋‘𝑦)) |
133 | 132, 129 | eqeltrd 2701 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 × {0})))) ∈
(Base‘𝑅)) |
134 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑧 = (𝐼 × {0}) → (𝑈‘𝑧) = (𝑈‘(𝐼 × {0}))) |
135 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑧 = (𝐼 × {0}) → (𝑦 ∘𝑓 − 𝑧) = (𝑦 ∘𝑓 − (𝐼 × {0}))) |
136 | 135 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑧 = (𝐼 × {0}) → (𝑋‘(𝑦 ∘𝑓 − 𝑧)) = (𝑋‘(𝑦 ∘𝑓 − (𝐼 ×
{0})))) |
137 | 134, 136 | oveq12d 6668 |
. . . . . 6
⊢ (𝑧 = (𝐼 × {0}) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 ×
{0}))))) |
138 | 2, 137 | gsumsn 18354 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ (𝐼 × {0}) ∈ 𝐷 ∧ ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 × {0})))) ∈
(Base‘𝑅)) →
(𝑅
Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 ×
{0}))))) |
139 | 119, 27, 133, 138 | syl3anc 1326 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 ×
{0}))))) |
140 | 51, 116, 139 | 3eqtr3d 2664 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 ×
{0}))))) |
141 | 22, 140, 132 | 3eqtrd 2660 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑋‘𝑦)) |
142 | 15, 17, 141 | eqfnfvd 6314 |
1
⊢ (𝜑 → (𝑈 · 𝑋) = 𝑋) |