Step | Hyp | Ref
| Expression |
1 | | psrring.s |
. . . 4
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | eqid 2821 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | psr1cl.d |
. . . 4
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
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 20182 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝐵) |
12 | | psrlidm.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
13 | 1, 4, 5, 6, 11, 12 | psrmulcl 20168 |
. . . 4
⊢ (𝜑 → (𝑈 · 𝑋) ∈ 𝐵) |
14 | 1, 2, 3, 4, 13 | psrelbas 20159 |
. . 3
⊢ (𝜑 → (𝑈 · 𝑋):𝐷⟶(Base‘𝑅)) |
15 | 14 | ffnd 6515 |
. 2
⊢ (𝜑 → (𝑈 · 𝑋) Fn 𝐷) |
16 | 1, 2, 3, 4, 12 | psrelbas 20159 |
. . 3
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
17 | 16 | ffnd 6515 |
. 2
⊢ (𝜑 → 𝑋 Fn 𝐷) |
18 | | eqid 2821 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
19 | 11 | adantr 483 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈 ∈ 𝐵) |
20 | 12 | adantr 483 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑋 ∈ 𝐵) |
21 | | simpr 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷) |
22 | 1, 4, 18, 5, 3, 19, 20, 21 | psrmulval 20166 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))))) |
23 | | breq1 5069 |
. . . . . . . 8
⊢ (𝑔 = (𝐼 × {0}) → (𝑔 ∘r ≤ 𝑦 ↔ (𝐼 × {0}) ∘r ≤ 𝑦)) |
24 | | fconstmpt 5614 |
. . . . . . . . . 10
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) |
25 | 3 | fczpsrbag 20147 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷) |
26 | 7, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷) |
27 | 24, 26 | eqeltrid 2917 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷) |
28 | 27 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ 𝐷) |
29 | 3 | psrbagf 20145 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0) |
30 | 7, 29 | sylan 582 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0) |
31 | 30 | ffvelrnda 6851 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) ∈
ℕ0) |
32 | 31 | nn0ge0d 11959 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → 0 ≤ (𝑦‘𝑥)) |
33 | 32 | ralrimiva 3182 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ∀𝑥 ∈ 𝐼 0 ≤ (𝑦‘𝑥)) |
34 | | 0nn0 11913 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
35 | 34 | fconst6 6569 |
. . . . . . . . . . 11
⊢ (𝐼 × {0}):𝐼⟶ℕ0 |
36 | | ffn 6514 |
. . . . . . . . . . 11
⊢ ((𝐼 × {0}):𝐼⟶ℕ0 → (𝐼 × {0}) Fn 𝐼) |
37 | 35, 36 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) Fn 𝐼) |
38 | 30 | ffnd 6515 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 Fn 𝐼) |
39 | 7 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐼 ∈ 𝑉) |
40 | | inidm 4195 |
. . . . . . . . . 10
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
41 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈
ℕ0) |
42 | | fvconst2g 6964 |
. . . . . . . . . . 11
⊢ ((0
∈ ℕ0 ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {0})‘𝑥) = 0) |
43 | 41, 42 | sylan 582 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {0})‘𝑥) = 0) |
44 | | eqidd 2822 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) = (𝑦‘𝑥)) |
45 | 37, 38, 39, 39, 40, 43, 44 | ofrfval 7417 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐼 × {0}) ∘r ≤ 𝑦 ↔ ∀𝑥 ∈ 𝐼 0 ≤ (𝑦‘𝑥))) |
46 | 33, 45 | mpbird 259 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∘r ≤ 𝑦) |
47 | 23, 28, 46 | elrabd 3682 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) |
48 | 47 | snssd 4742 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {(𝐼 × {0})} ⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) |
49 | 48 | resmptd 5908 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ↾ {(𝐼 × {0})}) = (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) |
50 | 49 | oveq2d 7172 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))))) |
51 | | ringcmn 19331 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
52 | 6, 51 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CMnd) |
53 | 52 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ CMnd) |
54 | | ovex 7189 |
. . . . . . 7
⊢
(ℕ0 ↑m 𝐼) ∈ V |
55 | 3, 54 | rab2ex 5238 |
. . . . . 6
⊢ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∈ V |
56 | 55 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∈ V) |
57 | 6 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑅 ∈ Ring) |
58 | | simpr 487 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) |
59 | | breq1 5069 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑧 → (𝑔 ∘r ≤ 𝑦 ↔ 𝑧 ∘r ≤ 𝑦)) |
60 | 59 | elrab 3680 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↔ (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦)) |
61 | 58, 60 | sylib 220 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦)) |
62 | 61 | simpld 497 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∈ 𝐷) |
63 | 1, 2, 3, 4, 19 | psrelbas 20159 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈:𝐷⟶(Base‘𝑅)) |
64 | 63 | ffvelrnda 6851 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ 𝐷) → (𝑈‘𝑧) ∈ (Base‘𝑅)) |
65 | 62, 64 | syldan 593 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑈‘𝑧) ∈ (Base‘𝑅)) |
66 | 16 | ad2antrr 724 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑋:𝐷⟶(Base‘𝑅)) |
67 | 7 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝐼 ∈ 𝑉) |
68 | 21 | adantr 483 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑦 ∈ 𝐷) |
69 | 3 | psrbagf 20145 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐷) → 𝑧:𝐼⟶ℕ0) |
70 | 67, 62, 69 | syl2anc 586 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧:𝐼⟶ℕ0) |
71 | 61 | simprd 498 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∘r ≤ 𝑦) |
72 | 3 | psrbagcon 20151 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ 𝐷 ∧ 𝑧:𝐼⟶ℕ0 ∧ 𝑧 ∘r ≤ 𝑦)) → ((𝑦 ∘f − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘f − 𝑧) ∘r ≤ 𝑦)) |
73 | 67, 68, 70, 71, 72 | syl13anc 1368 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑦 ∘f − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘f − 𝑧) ∘r ≤ 𝑦)) |
74 | 73 | simpld 497 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑦 ∘f − 𝑧) ∈ 𝐷) |
75 | 66, 74 | ffvelrnd 6852 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) |
76 | 2, 18 | ringcl 19311 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑈‘𝑧) ∈ (Base‘𝑅) ∧ (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) ∈ (Base‘𝑅)) |
77 | 57, 65, 75, 76 | syl3anc 1367 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) ∈ (Base‘𝑅)) |
78 | 77 | fmpttd 6879 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))):{𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}⟶(Base‘𝑅)) |
79 | | eldifi 4103 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) |
80 | 79, 61 | sylan2 594 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦)) |
81 | 80 | simpld 497 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → 𝑧 ∈ 𝐷) |
82 | | eqeq1 2825 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 = (𝐼 × {0}) ↔ 𝑧 = (𝐼 × {0}))) |
83 | 82 | ifbid 4489 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = if(𝑧 = (𝐼 × {0}), 1 , 0 )) |
84 | 9 | fvexi 6684 |
. . . . . . . . . . . 12
⊢ 1 ∈
V |
85 | 8 | fvexi 6684 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
86 | 84, 85 | ifex 4515 |
. . . . . . . . . . 11
⊢ if(𝑧 = (𝐼 × {0}), 1 , 0 ) ∈
V |
87 | 83, 10, 86 | fvmpt 6768 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐷 → (𝑈‘𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 )) |
88 | 81, 87 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑈‘𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 )) |
89 | | eldifn 4104 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})}) → ¬ 𝑧 ∈ {(𝐼 × {0})}) |
90 | 89 | adantl 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 ∈ {(𝐼 × {0})}) |
91 | | velsn 4583 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {(𝐼 × {0})} ↔ 𝑧 = (𝐼 × {0})) |
92 | 90, 91 | sylnib 330 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 = (𝐼 × {0})) |
93 | 92 | iffalsed 4478 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → if(𝑧 = (𝐼 × {0}), 1 , 0 ) = 0 ) |
94 | 88, 93 | eqtrd 2856 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑈‘𝑧) = 0 ) |
95 | 94 | oveq1d 7171 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) |
96 | 6 | ad2antrr 724 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → 𝑅 ∈ Ring) |
97 | 79, 75 | sylan2 594 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) |
98 | 2, 18, 8 | ringlz 19337 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) → ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = 0 ) |
99 | 96, 97, 98 | syl2anc 586 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ( 0 (.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = 0 ) |
100 | 95, 99 | eqtrd 2856 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {(𝐼 × {0})})) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = 0 ) |
101 | 100, 56 | suppss2 7864 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})}) |
102 | 3, 54 | rabex2 5237 |
. . . . . . . 8
⊢ 𝐷 ∈ V |
103 | 102 | mptrabex 6988 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∈ V |
104 | 103 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∈ V) |
105 | | funmpt 6393 |
. . . . . . 7
⊢ Fun
(𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) |
106 | 105 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) |
107 | 85 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈ V) |
108 | | snfi 8594 |
. . . . . . 7
⊢ {(𝐼 × {0})} ∈
Fin |
109 | 108 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {(𝐼 × {0})} ∈ Fin) |
110 | | suppssfifsupp 8848 |
. . . . . 6
⊢ ((((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∈ V ∧ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ∧ 0 ∈ V) ∧ ({(𝐼 × {0})} ∈ Fin ∧
((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})})) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) finSupp 0 ) |
111 | 104, 106,
107, 109, 101, 110 | syl32anc 1374 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) finSupp 0 ) |
112 | 2, 8, 53, 56, 78, 101, 111 | gsumres 19033 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧)))))) |
113 | 6 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Ring) |
114 | | ringmnd 19306 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
115 | 113, 114 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Mnd) |
116 | | iftrue 4473 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐼 × {0}) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = 1 ) |
117 | 116, 10, 84 | fvmpt 6768 |
. . . . . . . . 9
⊢ ((𝐼 × {0}) ∈ 𝐷 → (𝑈‘(𝐼 × {0})) = 1 ) |
118 | 28, 117 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝐼 × {0})) = 1 ) |
119 | | nn0cn 11908 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ0
→ 𝑧 ∈
ℂ) |
120 | 119 | subid1d 10986 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ0
→ (𝑧 − 0) =
𝑧) |
121 | 120 | adantl 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ℕ0) → (𝑧 − 0) = 𝑧) |
122 | 39, 30, 41, 121 | caofid0r 7438 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑦 ∘f − (𝐼 × {0})) = 𝑦) |
123 | 122 | fveq2d 6674 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘(𝑦 ∘f − (𝐼 × {0}))) = (𝑋‘𝑦)) |
124 | 118, 123 | oveq12d 7174 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) = ( 1
(.r‘𝑅)(𝑋‘𝑦))) |
125 | 16 | ffvelrnda 6851 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅)) |
126 | 2, 18, 9 | ringlidm 19321 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑦) ∈ (Base‘𝑅)) → ( 1 (.r‘𝑅)(𝑋‘𝑦)) = (𝑋‘𝑦)) |
127 | 113, 125,
126 | syl2anc 586 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ( 1 (.r‘𝑅)(𝑋‘𝑦)) = (𝑋‘𝑦)) |
128 | 124, 127 | eqtrd 2856 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) = (𝑋‘𝑦)) |
129 | 128, 125 | eqeltrd 2913 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) ∈
(Base‘𝑅)) |
130 | | fveq2 6670 |
. . . . . . 7
⊢ (𝑧 = (𝐼 × {0}) → (𝑈‘𝑧) = (𝑈‘(𝐼 × {0}))) |
131 | | oveq2 7164 |
. . . . . . . 8
⊢ (𝑧 = (𝐼 × {0}) → (𝑦 ∘f − 𝑧) = (𝑦 ∘f − (𝐼 × {0}))) |
132 | 131 | fveq2d 6674 |
. . . . . . 7
⊢ (𝑧 = (𝐼 × {0}) → (𝑋‘(𝑦 ∘f − 𝑧)) = (𝑋‘(𝑦 ∘f − (𝐼 ×
{0})))) |
133 | 130, 132 | oveq12d 7174 |
. . . . . 6
⊢ (𝑧 = (𝐼 × {0}) → ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 ×
{0}))))) |
134 | 2, 133 | gsumsn 19074 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ (𝐼 × {0}) ∈ 𝐷 ∧ ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 × {0})))) ∈
(Base‘𝑅)) →
(𝑅
Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 ×
{0}))))) |
135 | 115, 28, 129, 134 | syl3anc 1367 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 ×
{0}))))) |
136 | 50, 112, 135 | 3eqtr3d 2864 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑈‘𝑧)(.r‘𝑅)(𝑋‘(𝑦 ∘f − 𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r‘𝑅)(𝑋‘(𝑦 ∘f − (𝐼 ×
{0}))))) |
137 | 22, 136, 128 | 3eqtrd 2860 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑋‘𝑦)) |
138 | 15, 17, 137 | eqfnfvd 6805 |
1
⊢ (𝜑 → (𝑈 · 𝑋) = 𝑋) |