Step | Hyp | Ref
| Expression |
1 | | psrring.s |
. . . 4
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | eqid 2772 |
. . . 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 19886 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝐵) |
12 | | psrlidm.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
13 | 1, 4, 5, 6, 11, 12 | psrmulcl 19872 |
. . . 4
⊢ (𝜑 → (𝑈 · 𝑋) ∈ 𝐵) |
14 | 1, 2, 3, 4, 13 | psrelbas 19863 |
. . 3
⊢ (𝜑 → (𝑈 · 𝑋):𝐷⟶(Base‘𝑅)) |
15 | 14 | ffnd 6339 |
. 2
⊢ (𝜑 → (𝑈 · 𝑋) Fn 𝐷) |
16 | 1, 2, 3, 4, 12 | psrelbas 19863 |
. . 3
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
17 | 16 | ffnd 6339 |
. 2
⊢ (𝜑 → 𝑋 Fn 𝐷) |
18 | | eqid 2772 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
19 | 11 | adantr 473 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈 ∈ 𝐵) |
20 | 12 | adantr 473 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑋 ∈ 𝐵) |
21 | | simpr 477 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷) |
22 | 1, 4, 18, 5, 3, 19, 20, 21 | psrmulval 19870 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))))) |
23 | | breq1 4926 |
. . . . . . . 8
⊢ (𝑔 = (𝐼 × {0}) → (𝑔 ∘𝑟 ≤ 𝑦 ↔ (𝐼 × {0}) ∘𝑟
≤ 𝑦)) |
24 | | fconstmpt 5457 |
. . . . . . . . . 10
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) |
25 | 3 | fczpsrbag 19851 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷) |
26 | 7, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷) |
27 | 24, 26 | syl5eqel 2864 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷) |
28 | 27 | adantr 473 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ 𝐷) |
29 | 3 | psrbagf 19849 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0) |
30 | 7, 29 | sylan 572 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0) |
31 | 30 | ffvelrnda 6670 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) ∈
ℕ0) |
32 | 31 | nn0ge0d 11763 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → 0 ≤ (𝑦‘𝑥)) |
33 | 32 | ralrimiva 3126 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ∀𝑥 ∈ 𝐼 0 ≤ (𝑦‘𝑥)) |
34 | | 0nn0 11717 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
35 | 34 | fconst6 6392 |
. . . . . . . . . . 11
⊢ (𝐼 × {0}):𝐼⟶ℕ0 |
36 | | ffn 6338 |
. . . . . . . . . . 11
⊢ ((𝐼 × {0}):𝐼⟶ℕ0 → (𝐼 × {0}) Fn 𝐼) |
37 | 35, 36 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) Fn 𝐼) |
38 | 30 | ffnd 6339 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 Fn 𝐼) |
39 | 7 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐼 ∈ 𝑉) |
40 | | inidm 4077 |
. . . . . . . . . 10
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
41 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈
ℕ0) |
42 | | fvconst2g 6785 |
. . . . . . . . . . 11
⊢ ((0
∈ ℕ0 ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {0})‘𝑥) = 0) |
43 | 41, 42 | sylan 572 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {0})‘𝑥) = 0) |
44 | | eqidd 2773 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) = (𝑦‘𝑥)) |
45 | 37, 38, 39, 39, 40, 43, 44 | ofrfval 7229 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐼 × {0}) ∘𝑟
≤ 𝑦 ↔ ∀𝑥 ∈ 𝐼 0 ≤ (𝑦‘𝑥))) |
46 | 33, 45 | mpbird 249 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∘𝑟
≤ 𝑦) |
47 | 23, 28, 46 | elrabd 3592 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) |
48 | 47 | snssd 4610 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {(𝐼 × {0})} ⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) |
49 | 48 | resmptd 5747 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ↾ {(𝐼 × {0})}) = (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))))) |
50 | 49 | oveq2d 6986 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))))) |
51 | | ringcmn 19044 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
52 | 6, 51 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CMnd) |
53 | 52 | adantr 473 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ CMnd) |
54 | | ovex 7002 |
. . . . . . 7
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
55 | 3, 54 | rab2ex 5088 |
. . . . . 6
⊢ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∈ V |
56 | 55 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∈ V) |
57 | 6 | ad2antrr 713 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑅 ∈ Ring) |
58 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) |
59 | | breq1 4926 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑧 → (𝑔 ∘𝑟 ≤ 𝑦 ↔ 𝑧 ∘𝑟 ≤ 𝑦)) |
60 | 59 | elrab 3589 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↔ (𝑧 ∈ 𝐷 ∧ 𝑧 ∘𝑟 ≤ 𝑦)) |
61 | 58, 60 | sylib 210 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘𝑟 ≤ 𝑦)) |
62 | 61 | simpld 487 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧 ∈ 𝐷) |
63 | 1, 2, 3, 4, 19 | psrelbas 19863 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈:𝐷⟶(Base‘𝑅)) |
64 | 63 | ffvelrnda 6670 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ 𝐷) → (𝑈‘𝑧) ∈ (Base‘𝑅)) |
65 | 62, 64 | syldan 582 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → (𝑈‘𝑧) ∈ (Base‘𝑅)) |
66 | 16 | ad2antrr 713 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑋:𝐷⟶(Base‘𝑅)) |
67 | 7 | ad2antrr 713 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝐼 ∈ 𝑉) |
68 | 21 | adantr 473 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑦 ∈ 𝐷) |
69 | 3 | psrbagf 19849 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐷) → 𝑧:𝐼⟶ℕ0) |
70 | 67, 62, 69 | syl2anc 576 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧:𝐼⟶ℕ0) |
71 | 61 | simprd 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → 𝑧 ∘𝑟 ≤ 𝑦) |
72 | 3 | psrbagcon 19855 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ 𝐷 ∧ 𝑧:𝐼⟶ℕ0 ∧ 𝑧 ∘𝑟
≤ 𝑦)) → ((𝑦 ∘𝑓
− 𝑧) ∈ 𝐷 ∧ (𝑦 ∘𝑓 − 𝑧) ∘𝑟
≤ 𝑦)) |
73 | 67, 68, 70, 71, 72 | syl13anc 1352 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → ((𝑦 ∘𝑓 − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘𝑓 − 𝑧) ∘𝑟
≤ 𝑦)) |
74 | 73 | simpld 487 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → (𝑦 ∘𝑓 − 𝑧) ∈ 𝐷) |
75 | 66, 74 | ffvelrnd 6671 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → (𝑋‘(𝑦 ∘𝑓 − 𝑧)) ∈ (Base‘𝑅)) |
76 | 2, 18 | ringcl 19024 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑈‘𝑧) ∈ (Base‘𝑅) ∧ (𝑋‘(𝑦 ∘𝑓 − 𝑧)) ∈ (Base‘𝑅)) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) ∈ (Base‘𝑅)) |
77 | 57, 65, 75, 76 | syl3anc 1351 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) ∈ (Base‘𝑅)) |
78 | 77 | fmpttd 6696 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))):{𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}⟶(Base‘𝑅)) |
79 | | eldifi 3989 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦}) |
80 | 79, 61 | sylan2 583 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘𝑟 ≤ 𝑦)) |
81 | 80 | simpld 487 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → 𝑧 ∈ 𝐷) |
82 | | eqeq1 2776 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 = (𝐼 × {0}) ↔ 𝑧 = (𝐼 × {0}))) |
83 | 82 | ifbid 4366 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = if(𝑧 = (𝐼 × {0}), 1 , 0 )) |
84 | 9 | fvexi 6507 |
. . . . . . . . . . . 12
⊢ 1 ∈
V |
85 | 8 | fvexi 6507 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
86 | 84, 85 | ifex 4392 |
. . . . . . . . . . 11
⊢ if(𝑧 = (𝐼 × {0}), 1 , 0 ) ∈
V |
87 | 83, 10, 86 | fvmpt 6589 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐷 → (𝑈‘𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 )) |
88 | 81, 87 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑈‘𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 )) |
89 | | eldifn 3990 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})}) → ¬ 𝑧 ∈ {(𝐼 × {0})}) |
90 | 89 | adantl 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 ∈ {(𝐼 × {0})}) |
91 | | velsn 4451 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {(𝐼 × {0})} ↔ 𝑧 = (𝐼 × {0})) |
92 | 90, 91 | sylnib 320 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 = (𝐼 × {0})) |
93 | 92 | iffalsed 4355 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → if(𝑧 = (𝐼 × {0}), 1 , 0 ) = 0 ) |
94 | 88, 93 | eqtrd 2808 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑈‘𝑧) = 0 ) |
95 | 94 | oveq1d 6985 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) = ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) |
96 | 6 | ad2antrr 713 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → 𝑅 ∈ Ring) |
97 | 79, 75 | sylan2 583 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑋‘(𝑦 ∘𝑓 − 𝑧)) ∈ (Base‘𝑅)) |
98 | 2, 18, 8 | ringlz 19050 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘(𝑦 ∘𝑓 − 𝑧)) ∈ (Base‘𝑅)) → ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) = 0 ) |
99 | 96, 97, 98 | syl2anc 576 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) = 0 ) |
100 | 95, 99 | eqtrd 2808 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ∖ {(𝐼 × {0})})) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) = 0 ) |
101 | 100, 56 | suppss2 7660 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})}) |
102 | 3, 54 | rabex2 5087 |
. . . . . . . 8
⊢ 𝐷 ∈ V |
103 | 102 | mptrabex 6808 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ∈ V |
104 | 103 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ∈ V) |
105 | | funmpt 6220 |
. . . . . . 7
⊢ Fun
(𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) |
106 | 105 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))))) |
107 | 85 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈ V) |
108 | | snfi 8383 |
. . . . . . 7
⊢ {(𝐼 × {0})} ∈
Fin |
109 | 108 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {(𝐼 × {0})} ∈ Fin) |
110 | | suppssfifsupp 8635 |
. . . . . 6
⊢ ((((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ∈ V ∧ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ∧ 0 ∈ V) ∧ ({(𝐼 × {0})} ∈ Fin ∧
((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})})) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) finSupp 0 ) |
111 | 104, 106,
107, 109, 101, 110 | syl32anc 1358 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) finSupp 0 ) |
112 | 2, 8, 53, 56, 78, 101, 111 | gsumres 18777 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧)))))) |
113 | 6 | adantr 473 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Ring) |
114 | | ringmnd 19019 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
115 | 113, 114 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Mnd) |
116 | | iftrue 4350 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐼 × {0}) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = 1 ) |
117 | 116, 10, 84 | fvmpt 6589 |
. . . . . . . . 9
⊢ ((𝐼 × {0}) ∈ 𝐷 → (𝑈‘(𝐼 × {0})) = 1 ) |
118 | 28, 117 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝐼 × {0})) = 1 ) |
119 | | nn0cn 11711 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ0
→ 𝑧 ∈
ℂ) |
120 | 119 | subid1d 10779 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ0
→ (𝑧 − 0) =
𝑧) |
121 | 120 | adantl 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ℕ0) → (𝑧 − 0) = 𝑧) |
122 | 39, 30, 41, 121 | caofid0r 7250 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑦 ∘𝑓 − (𝐼 × {0})) = 𝑦) |
123 | 122 | fveq2d 6497 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘(𝑦 ∘𝑓 − (𝐼 × {0}))) = (𝑋‘𝑦)) |
124 | 118, 123 | oveq12d 6988 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 × {0})))) = ( 1
(.r‘𝑅)(𝑋‘𝑦))) |
125 | 16 | ffvelrnda 6670 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅)) |
126 | 2, 18, 9 | ringlidm 19034 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑦) ∈ (Base‘𝑅)) → ( 1 (.r‘𝑅)(𝑋‘𝑦)) = (𝑋‘𝑦)) |
127 | 113, 125,
126 | syl2anc 576 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ( 1 (.r‘𝑅)(𝑋‘𝑦)) = (𝑋‘𝑦)) |
128 | 124, 127 | eqtrd 2808 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 × {0})))) = (𝑋‘𝑦)) |
129 | 128, 125 | eqeltrd 2860 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 × {0})))) ∈
(Base‘𝑅)) |
130 | | fveq2 6493 |
. . . . . . 7
⊢ (𝑧 = (𝐼 × {0}) → (𝑈‘𝑧) = (𝑈‘(𝐼 × {0}))) |
131 | | oveq2 6978 |
. . . . . . . 8
⊢ (𝑧 = (𝐼 × {0}) → (𝑦 ∘𝑓 − 𝑧) = (𝑦 ∘𝑓 − (𝐼 × {0}))) |
132 | 131 | fveq2d 6497 |
. . . . . . 7
⊢ (𝑧 = (𝐼 × {0}) → (𝑋‘(𝑦 ∘𝑓 − 𝑧)) = (𝑋‘(𝑦 ∘𝑓 − (𝐼 ×
{0})))) |
133 | 130, 132 | oveq12d 6988 |
. . . . . 6
⊢ (𝑧 = (𝐼 × {0}) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 ×
{0}))))) |
134 | 2, 133 | gsumsn 18817 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ (𝐼 × {0}) ∈ 𝐷 ∧ ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 × {0})))) ∈
(Base‘𝑅)) →
(𝑅
Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 ×
{0}))))) |
135 | 115, 28, 129, 134 | syl3anc 1351 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 ×
{0}))))) |
136 | 50, 112, 135 | 3eqtr3d 2816 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘𝑓 − (𝐼 ×
{0}))))) |
137 | 22, 136, 128 | 3eqtrd 2812 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑋‘𝑦)) |
138 | 15, 17, 137 | eqfnfvd 6624 |
1
⊢ (𝜑 → (𝑈 · 𝑋) = 𝑋) |