Step | Hyp | Ref
| Expression |
1 | | eqid 2651 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2651 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | | psrring.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | | ringcmn 18627 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CMnd) |
6 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑅 ∈ CMnd) |
7 | | psrring.i |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
8 | | psrass.d |
. . . . . . 7
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
9 | 8 | psrbaglefi 19420 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ∈ Fin) |
10 | 7, 9 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ∈ Fin) |
11 | 3 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑅 ∈ Ring) |
12 | | psrring.s |
. . . . . . . . . 10
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
13 | | psrass.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑆) |
14 | | psrass.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
15 | 12, 1, 8, 13, 14 | psrelbas 19427 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
16 | 15 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑋:𝐷⟶(Base‘𝑅)) |
17 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) |
18 | | breq1 4688 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑘 → (𝑔 ∘𝑟 ≤ 𝑥 ↔ 𝑘 ∘𝑟 ≤ 𝑥)) |
19 | 18 | elrab 3396 |
. . . . . . . . . 10
⊢ (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↔ (𝑘 ∈ 𝐷 ∧ 𝑘 ∘𝑟 ≤ 𝑥)) |
20 | 17, 19 | sylib 208 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑘 ∈ 𝐷 ∧ 𝑘 ∘𝑟 ≤ 𝑥)) |
21 | 20 | simpld 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑘 ∈ 𝐷) |
22 | 16, 21 | ffvelrnd 6400 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑋‘𝑘) ∈ (Base‘𝑅)) |
23 | | psrass.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
24 | 12, 1, 8, 13, 23 | psrelbas 19427 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) |
25 | 24 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑌:𝐷⟶(Base‘𝑅)) |
26 | 7 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝐼 ∈ 𝑉) |
27 | | simplr 807 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑥 ∈ 𝐷) |
28 | 8 | psrbagf 19413 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑘 ∈ 𝐷) → 𝑘:𝐼⟶ℕ0) |
29 | 26, 21, 28 | syl2anc 694 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑘:𝐼⟶ℕ0) |
30 | 20 | simprd 478 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑘 ∘𝑟 ≤ 𝑥) |
31 | 8 | psrbagcon 19419 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝐷 ∧ 𝑘:𝐼⟶ℕ0 ∧ 𝑘 ∘𝑟
≤ 𝑥)) → ((𝑥 ∘𝑓
− 𝑘) ∈ 𝐷 ∧ (𝑥 ∘𝑓 − 𝑘) ∘𝑟
≤ 𝑥)) |
32 | 26, 27, 29, 30, 31 | syl13anc 1368 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑥 ∘𝑓 − 𝑘) ∈ 𝐷 ∧ (𝑥 ∘𝑓 − 𝑘) ∘𝑟
≤ 𝑥)) |
33 | 32 | simpld 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑘) ∈ 𝐷) |
34 | 25, 33 | ffvelrnd 6400 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑌‘(𝑥 ∘𝑓 − 𝑘)) ∈ (Base‘𝑅)) |
35 | | eqid 2651 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
36 | 1, 35 | ringcl 18607 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑘) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑥 ∘𝑓 − 𝑘)) ∈ (Base‘𝑅)) → ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘))) ∈ (Base‘𝑅)) |
37 | 11, 22, 34, 36 | syl3anc 1366 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘))) ∈ (Base‘𝑅)) |
38 | | eqid 2651 |
. . . . . 6
⊢ (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) = (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) |
39 | 37, 38 | fmptd 6425 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))):{𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}⟶(Base‘𝑅)) |
40 | | ovex 6718 |
. . . . . . . . . 10
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
41 | 8, 40 | rabex2 4847 |
. . . . . . . . 9
⊢ 𝐷 ∈ V |
42 | 41 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐷 ∈ V) |
43 | | rabexg 4844 |
. . . . . . . 8
⊢ (𝐷 ∈ V → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ∈ V) |
44 | 42, 43 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ∈ V) |
45 | | mptexg 6525 |
. . . . . . 7
⊢ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ∈ V → (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) ∈ V) |
46 | 44, 45 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) ∈ V) |
47 | | funmpt 5964 |
. . . . . . 7
⊢ Fun
(𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) |
48 | 47 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → Fun (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘))))) |
49 | | fvexd 6241 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0g‘𝑅) ∈ V) |
50 | | suppssdm 7353 |
. . . . . . . 8
⊢ ((𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) supp
(0g‘𝑅))
⊆ dom (𝑘 ∈
{𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) |
51 | 38 | dmmptss 5669 |
. . . . . . . 8
⊢ dom
(𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) ⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} |
52 | 50, 51 | sstri 3645 |
. . . . . . 7
⊢ ((𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) supp
(0g‘𝑅))
⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} |
53 | 52 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) supp
(0g‘𝑅))
⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) |
54 | | suppssfifsupp 8331 |
. . . . . 6
⊢ ((((𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) ∈ V ∧ Fun (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) ∧
(0g‘𝑅)
∈ V) ∧ ({𝑔 ∈
𝐷 ∣ 𝑔 ∘𝑟
≤ 𝑥} ∈ Fin ∧
((𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) supp
(0g‘𝑅))
⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥})) → (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) finSupp
(0g‘𝑅)) |
55 | 46, 48, 49, 10, 53, 54 | syl32anc 1374 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) finSupp
(0g‘𝑅)) |
56 | | eqid 2651 |
. . . . . . 7
⊢ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} = {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} |
57 | 8, 56 | psrbagconf1o 19422 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) → (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑥 ∘𝑓 − 𝑗)):{𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}–1-1-onto→{𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) |
58 | 7, 57 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑥 ∘𝑓 − 𝑗)):{𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}–1-1-onto→{𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) |
59 | 1, 2, 6, 10, 39, 55, 58 | gsumf1o 18363 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑅 Σg (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘))))) = (𝑅 Σg ((𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) ∘ (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑥 ∘𝑓 − 𝑗))))) |
60 | 7 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝐼 ∈ 𝑉) |
61 | | simplr 807 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑥 ∈ 𝐷) |
62 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) |
63 | 8, 56 | psrbagconcl 19421 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷 ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑗) ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) |
64 | 60, 61, 62, 63 | syl3anc 1366 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑗) ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) |
65 | | eqidd 2652 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑥 ∘𝑓 − 𝑗)) = (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑥 ∘𝑓 − 𝑗))) |
66 | | eqidd 2652 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) = (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘))))) |
67 | | fveq2 6229 |
. . . . . . . 8
⊢ (𝑘 = (𝑥 ∘𝑓 − 𝑗) → (𝑋‘𝑘) = (𝑋‘(𝑥 ∘𝑓 − 𝑗))) |
68 | | oveq2 6698 |
. . . . . . . . 9
⊢ (𝑘 = (𝑥 ∘𝑓 − 𝑗) → (𝑥 ∘𝑓 − 𝑘) = (𝑥 ∘𝑓 − (𝑥 ∘𝑓
− 𝑗))) |
69 | 68 | fveq2d 6233 |
. . . . . . . 8
⊢ (𝑘 = (𝑥 ∘𝑓 − 𝑗) → (𝑌‘(𝑥 ∘𝑓 − 𝑘)) = (𝑌‘(𝑥 ∘𝑓 − (𝑥 ∘𝑓
− 𝑗)))) |
70 | 67, 69 | oveq12d 6708 |
. . . . . . 7
⊢ (𝑘 = (𝑥 ∘𝑓 − 𝑗) → ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘))) = ((𝑋‘(𝑥 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − (𝑥 ∘𝑓
− 𝑗))))) |
71 | 64, 65, 66, 70 | fmptco 6436 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) ∘ (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑥 ∘𝑓 − 𝑗))) = (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘(𝑥 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − (𝑥 ∘𝑓
− 𝑗)))))) |
72 | 8 | psrbagf 19413 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) → 𝑥:𝐼⟶ℕ0) |
73 | 7, 72 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥:𝐼⟶ℕ0) |
74 | 73 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑥:𝐼⟶ℕ0) |
75 | 74 | ffvelrnda 6399 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑧 ∈ 𝐼) → (𝑥‘𝑧) ∈
ℕ0) |
76 | | breq1 4688 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑗 → (𝑔 ∘𝑟 ≤ 𝑥 ↔ 𝑗 ∘𝑟 ≤ 𝑥)) |
77 | 76 | elrab 3396 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↔ (𝑗 ∈ 𝐷 ∧ 𝑗 ∘𝑟 ≤ 𝑥)) |
78 | 62, 77 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑗 ∈ 𝐷 ∧ 𝑗 ∘𝑟 ≤ 𝑥)) |
79 | 78 | simpld 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑗 ∈ 𝐷) |
80 | 8 | psrbagf 19413 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐷) → 𝑗:𝐼⟶ℕ0) |
81 | 60, 79, 80 | syl2anc 694 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑗:𝐼⟶ℕ0) |
82 | 81 | ffvelrnda 6399 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑧 ∈ 𝐼) → (𝑗‘𝑧) ∈
ℕ0) |
83 | | nn0cn 11340 |
. . . . . . . . . . . . . 14
⊢ ((𝑥‘𝑧) ∈ ℕ0 → (𝑥‘𝑧) ∈ ℂ) |
84 | | nn0cn 11340 |
. . . . . . . . . . . . . 14
⊢ ((𝑗‘𝑧) ∈ ℕ0 → (𝑗‘𝑧) ∈ ℂ) |
85 | | nncan 10348 |
. . . . . . . . . . . . . 14
⊢ (((𝑥‘𝑧) ∈ ℂ ∧ (𝑗‘𝑧) ∈ ℂ) → ((𝑥‘𝑧) − ((𝑥‘𝑧) − (𝑗‘𝑧))) = (𝑗‘𝑧)) |
86 | 83, 84, 85 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ (((𝑥‘𝑧) ∈ ℕ0 ∧ (𝑗‘𝑧) ∈ ℕ0) → ((𝑥‘𝑧) − ((𝑥‘𝑧) − (𝑗‘𝑧))) = (𝑗‘𝑧)) |
87 | 75, 82, 86 | syl2anc 694 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑧 ∈ 𝐼) → ((𝑥‘𝑧) − ((𝑥‘𝑧) − (𝑗‘𝑧))) = (𝑗‘𝑧)) |
88 | 87 | mpteq2dva 4777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧) − ((𝑥‘𝑧) − (𝑗‘𝑧)))) = (𝑧 ∈ 𝐼 ↦ (𝑗‘𝑧))) |
89 | | ovex 6718 |
. . . . . . . . . . . . 13
⊢ ((𝑥‘𝑧) − (𝑗‘𝑧)) ∈ V |
90 | 89 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑧 ∈ 𝐼) → ((𝑥‘𝑧) − (𝑗‘𝑧)) ∈ V) |
91 | 74 | feqmptd 6288 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑥 = (𝑧 ∈ 𝐼 ↦ (𝑥‘𝑧))) |
92 | 81 | feqmptd 6288 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑗 = (𝑧 ∈ 𝐼 ↦ (𝑗‘𝑧))) |
93 | 60, 75, 82, 91, 92 | offval2 6956 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑗) = (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧) − (𝑗‘𝑧)))) |
94 | 60, 75, 90, 91, 93 | offval2 6956 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − (𝑥 ∘𝑓
− 𝑗)) = (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧) − ((𝑥‘𝑧) − (𝑗‘𝑧))))) |
95 | 88, 94, 92 | 3eqtr4d 2695 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − (𝑥 ∘𝑓
− 𝑗)) = 𝑗) |
96 | 95 | fveq2d 6233 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑌‘(𝑥 ∘𝑓 − (𝑥 ∘𝑓
− 𝑗))) = (𝑌‘𝑗)) |
97 | 96 | oveq2d 6706 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑋‘(𝑥 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − (𝑥 ∘𝑓
− 𝑗)))) = ((𝑋‘(𝑥 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑌‘𝑗))) |
98 | | psrcom.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ CRing) |
99 | 98 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑅 ∈ CRing) |
100 | 15 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑋:𝐷⟶(Base‘𝑅)) |
101 | 78 | simprd 478 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑗 ∘𝑟 ≤ 𝑥) |
102 | 8 | psrbagcon 19419 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝐷 ∧ 𝑗:𝐼⟶ℕ0 ∧ 𝑗 ∘𝑟
≤ 𝑥)) → ((𝑥 ∘𝑓
− 𝑗) ∈ 𝐷 ∧ (𝑥 ∘𝑓 − 𝑗) ∘𝑟
≤ 𝑥)) |
103 | 60, 61, 81, 101, 102 | syl13anc 1368 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑥 ∘𝑓 − 𝑗) ∈ 𝐷 ∧ (𝑥 ∘𝑓 − 𝑗) ∘𝑟
≤ 𝑥)) |
104 | 103 | simpld 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑗) ∈ 𝐷) |
105 | 100, 104 | ffvelrnd 6400 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑋‘(𝑥 ∘𝑓 − 𝑗)) ∈ (Base‘𝑅)) |
106 | 24 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑌:𝐷⟶(Base‘𝑅)) |
107 | 106, 79 | ffvelrnd 6400 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑌‘𝑗) ∈ (Base‘𝑅)) |
108 | 1, 35 | crngcom 18608 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ (𝑋‘(𝑥 ∘𝑓 − 𝑗)) ∈ (Base‘𝑅) ∧ (𝑌‘𝑗) ∈ (Base‘𝑅)) → ((𝑋‘(𝑥 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑌‘𝑗)) = ((𝑌‘𝑗)(.r‘𝑅)(𝑋‘(𝑥 ∘𝑓 − 𝑗)))) |
109 | 99, 105, 107, 108 | syl3anc 1366 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑋‘(𝑥 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑌‘𝑗)) = ((𝑌‘𝑗)(.r‘𝑅)(𝑋‘(𝑥 ∘𝑓 − 𝑗)))) |
110 | 97, 109 | eqtrd 2685 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑋‘(𝑥 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − (𝑥 ∘𝑓
− 𝑗)))) = ((𝑌‘𝑗)(.r‘𝑅)(𝑋‘(𝑥 ∘𝑓 − 𝑗)))) |
111 | 110 | mpteq2dva 4777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘(𝑥 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − (𝑥 ∘𝑓
− 𝑗))))) = (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑌‘𝑗)(.r‘𝑅)(𝑋‘(𝑥 ∘𝑓 − 𝑗))))) |
112 | 71, 111 | eqtrd 2685 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) ∘ (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑥 ∘𝑓 − 𝑗))) = (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑌‘𝑗)(.r‘𝑅)(𝑋‘(𝑥 ∘𝑓 − 𝑗))))) |
113 | 112 | oveq2d 6706 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑅 Σg ((𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))) ∘ (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑥 ∘𝑓 − 𝑗)))) = (𝑅 Σg (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑌‘𝑗)(.r‘𝑅)(𝑋‘(𝑥 ∘𝑓 − 𝑗)))))) |
114 | 59, 113 | eqtrd 2685 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑅 Σg (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘))))) = (𝑅 Σg (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑌‘𝑗)(.r‘𝑅)(𝑋‘(𝑥 ∘𝑓 − 𝑗)))))) |
115 | 114 | mpteq2dva 4777 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝑅 Σg (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘)))))) = (𝑥 ∈ 𝐷 ↦ (𝑅 Σg (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑌‘𝑗)(.r‘𝑅)(𝑋‘(𝑥 ∘𝑓 − 𝑗))))))) |
116 | | psrass.t |
. . 3
⊢ × =
(.r‘𝑆) |
117 | 12, 13, 35, 116, 8, 14, 23 | psrmulfval 19433 |
. 2
⊢ (𝜑 → (𝑋 × 𝑌) = (𝑥 ∈ 𝐷 ↦ (𝑅 Σg (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑘)(.r‘𝑅)(𝑌‘(𝑥 ∘𝑓 − 𝑘))))))) |
118 | 12, 13, 35, 116, 8, 23, 14 | psrmulfval 19433 |
. 2
⊢ (𝜑 → (𝑌 × 𝑋) = (𝑥 ∈ 𝐷 ↦ (𝑅 Σg (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑌‘𝑗)(.r‘𝑅)(𝑋‘(𝑥 ∘𝑓 − 𝑗))))))) |
119 | 115, 117,
118 | 3eqtr4d 2695 |
1
⊢ (𝜑 → (𝑋 × 𝑌) = (𝑌 × 𝑋)) |