Step | Hyp | Ref
| Expression |
1 | | psrring.s |
. . . 4
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | psrass.d |
. . . 4
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
4 | | psrass.b |
. . . 4
⊢ 𝐵 = (Base‘𝑆) |
5 | | psrass.t |
. . . . 5
⊢ × =
(.r‘𝑆) |
6 | | psrring.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
7 | | psrass.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
8 | | psrass.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
9 | 1, 4, 5, 6, 7, 8 | psrmulcl 19209 |
. . . . 5
⊢ (𝜑 → (𝑋 × 𝑌) ∈ 𝐵) |
10 | | psrass.z |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
11 | 1, 4, 5, 6, 9, 10 | psrmulcl 19209 |
. . . 4
⊢ (𝜑 → ((𝑋 × 𝑌) × 𝑍) ∈ 𝐵) |
12 | 1, 2, 3, 4, 11 | psrelbas 19200 |
. . 3
⊢ (𝜑 → ((𝑋 × 𝑌) × 𝑍):𝐷⟶(Base‘𝑅)) |
13 | 12 | ffnd 5959 |
. 2
⊢ (𝜑 → ((𝑋 × 𝑌) × 𝑍) Fn 𝐷) |
14 | 1, 4, 5, 6, 8, 10 | psrmulcl 19209 |
. . . . 5
⊢ (𝜑 → (𝑌 × 𝑍) ∈ 𝐵) |
15 | 1, 4, 5, 6, 7, 14 | psrmulcl 19209 |
. . . 4
⊢ (𝜑 → (𝑋 × (𝑌 × 𝑍)) ∈ 𝐵) |
16 | 1, 2, 3, 4, 15 | psrelbas 19200 |
. . 3
⊢ (𝜑 → (𝑋 × (𝑌 × 𝑍)):𝐷⟶(Base‘𝑅)) |
17 | 16 | ffnd 5959 |
. 2
⊢ (𝜑 → (𝑋 × (𝑌 × 𝑍)) Fn 𝐷) |
18 | | eqid 2610 |
. . . . 5
⊢ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} = {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} |
19 | | psrring.i |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐼 ∈ 𝑉) |
21 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷) |
22 | | ringcmn 18404 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
23 | 6, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CMnd) |
24 | 23 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑅 ∈ CMnd) |
25 | 6 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑅 ∈ Ring) |
26 | 25 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → 𝑅 ∈ Ring) |
27 | 1, 2, 3, 4, 7 | psrelbas 19200 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
28 | 27 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑋:𝐷⟶(Base‘𝑅)) |
29 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) |
30 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑗 → (𝑔 ∘𝑟 ≤ 𝑥 ↔ 𝑗 ∘𝑟 ≤ 𝑥)) |
31 | 30 | elrab 3331 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↔ (𝑗 ∈ 𝐷 ∧ 𝑗 ∘𝑟 ≤ 𝑥)) |
32 | 29, 31 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑗 ∈ 𝐷 ∧ 𝑗 ∘𝑟 ≤ 𝑥)) |
33 | 32 | simpld 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑗 ∈ 𝐷) |
34 | 28, 33 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑋‘𝑗) ∈ (Base‘𝑅)) |
35 | 34 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → (𝑋‘𝑗) ∈ (Base‘𝑅)) |
36 | 1, 2, 3, 4, 8 | psrelbas 19200 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) |
37 | 36 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → 𝑌:𝐷⟶(Base‘𝑅)) |
38 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) |
39 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑛 → (ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗) ↔ 𝑛 ∘𝑟
≤ (𝑥
∘𝑓 − 𝑗))) |
40 | 39 | elrab 3331 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↔ (𝑛 ∈ 𝐷 ∧ 𝑛 ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗))) |
41 | 38, 40 | sylib 207 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → (𝑛 ∈ 𝐷 ∧ 𝑛 ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗))) |
42 | 41 | simpld 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → 𝑛 ∈ 𝐷) |
43 | 37, 42 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → (𝑌‘𝑛) ∈ (Base‘𝑅)) |
44 | 1, 2, 3, 4, 10 | psrelbas 19200 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍:𝐷⟶(Base‘𝑅)) |
45 | 44 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → 𝑍:𝐷⟶(Base‘𝑅)) |
46 | 19 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝐼 ∈ 𝑉) |
47 | 46 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → 𝐼 ∈ 𝑉) |
48 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑥 ∈ 𝐷) |
49 | 3 | psrbagf 19186 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐷) → 𝑗:𝐼⟶ℕ0) |
50 | 46, 33, 49 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑗:𝐼⟶ℕ0) |
51 | 32 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑗 ∘𝑟 ≤ 𝑥) |
52 | 3 | psrbagcon 19192 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝐷 ∧ 𝑗:𝐼⟶ℕ0 ∧ 𝑗 ∘𝑟
≤ 𝑥)) → ((𝑥 ∘𝑓
− 𝑗) ∈ 𝐷 ∧ (𝑥 ∘𝑓 − 𝑗) ∘𝑟
≤ 𝑥)) |
53 | 46, 48, 50, 51, 52 | syl13anc 1320 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑥 ∘𝑓 − 𝑗) ∈ 𝐷 ∧ (𝑥 ∘𝑓 − 𝑗) ∘𝑟
≤ 𝑥)) |
54 | 53 | simpld 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑗) ∈ 𝐷) |
55 | 54 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → (𝑥 ∘𝑓
− 𝑗) ∈ 𝐷) |
56 | 3 | psrbagf 19186 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑛 ∈ 𝐷) → 𝑛:𝐼⟶ℕ0) |
57 | 47, 42, 56 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → 𝑛:𝐼⟶ℕ0) |
58 | 41 | simprd 478 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → 𝑛 ∘𝑟
≤ (𝑥
∘𝑓 − 𝑗)) |
59 | 3 | psrbagcon 19192 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ ((𝑥 ∘𝑓 − 𝑗) ∈ 𝐷 ∧ 𝑛:𝐼⟶ℕ0 ∧ 𝑛 ∘𝑟
≤ (𝑥
∘𝑓 − 𝑗))) → (((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛) ∈ 𝐷 ∧ ((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)
∘𝑟 ≤ (𝑥 ∘𝑓 − 𝑗))) |
60 | 47, 55, 57, 58, 59 | syl13anc 1320 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) →
(((𝑥
∘𝑓 − 𝑗) ∘𝑓 − 𝑛) ∈ 𝐷 ∧ ((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)
∘𝑟 ≤ (𝑥 ∘𝑓 − 𝑗))) |
61 | 60 | simpld 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → ((𝑥 ∘𝑓
− 𝑗)
∘𝑓 − 𝑛) ∈ 𝐷) |
62 | 45, 61 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → (𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)) ∈
(Base‘𝑅)) |
63 | | eqid 2610 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
64 | 2, 63 | ringcl 18384 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑌‘𝑛) ∈ (Base‘𝑅) ∧ (𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)) ∈
(Base‘𝑅)) →
((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛))) ∈
(Base‘𝑅)) |
65 | 26, 43, 62, 64 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛))) ∈
(Base‘𝑅)) |
66 | 2, 63 | ringcl 18384 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑗) ∈ (Base‘𝑅) ∧ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛))) ∈
(Base‘𝑅)) →
((𝑋‘𝑗)(.r‘𝑅)((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) ∈
(Base‘𝑅)) |
67 | 26, 35, 65, 66 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) → ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) ∈
(Base‘𝑅)) |
68 | 67 | anasss 677 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ∧ 𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)})) →
((𝑋‘𝑗)(.r‘𝑅)((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) ∈
(Base‘𝑅)) |
69 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑛 = (𝑘 ∘𝑓 − 𝑗) → (𝑌‘𝑛) = (𝑌‘(𝑘 ∘𝑓 − 𝑗))) |
70 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑛 = (𝑘 ∘𝑓 − 𝑗) → ((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛) = ((𝑥 ∘𝑓
− 𝑗)
∘𝑓 − (𝑘 ∘𝑓 − 𝑗))) |
71 | 70 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑛 = (𝑘 ∘𝑓 − 𝑗) → (𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)) = (𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗)))) |
72 | 69, 71 | oveq12d 6567 |
. . . . . 6
⊢ (𝑛 = (𝑘 ∘𝑓 − 𝑗) → ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛))) = ((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗))))) |
73 | 72 | oveq2d 6565 |
. . . . 5
⊢ (𝑛 = (𝑘 ∘𝑓 − 𝑗) → ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) = ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗)))))) |
74 | 3, 18, 20, 21, 2, 24, 68, 73 | psrass1lem 19198 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑅 Σg (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑅 Σg (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗))))))))) = (𝑅 Σg (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑅 Σg (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛))))))))) |
75 | 7 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑋 ∈ 𝐵) |
76 | 8 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑌 ∈ 𝐵) |
77 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) |
78 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑘 → (𝑔 ∘𝑟 ≤ 𝑥 ↔ 𝑘 ∘𝑟 ≤ 𝑥)) |
79 | 78 | elrab 3331 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↔ (𝑘 ∈ 𝐷 ∧ 𝑘 ∘𝑟 ≤ 𝑥)) |
80 | 77, 79 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑘 ∈ 𝐷 ∧ 𝑘 ∘𝑟 ≤ 𝑥)) |
81 | 80 | simpld 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑘 ∈ 𝐷) |
82 | 1, 4, 63, 5, 3, 75, 76, 81 | psrmulval 19207 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑋 × 𝑌)‘𝑘) = (𝑅 Σg (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗)))))) |
83 | 82 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (((𝑋 × 𝑌)‘𝑘)(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘))) = ((𝑅 Σg (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗)))))(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘)))) |
84 | | eqid 2610 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
85 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝑅) = (+g‘𝑅) |
86 | 6 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑅 ∈ Ring) |
87 | 19 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝐼 ∈ 𝑉) |
88 | 3 | psrbaglefi 19193 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑘 ∈ 𝐷) → {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ∈ Fin) |
89 | 87, 81, 88 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ∈ Fin) |
90 | 44 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑍:𝐷⟶(Base‘𝑅)) |
91 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑥 ∈ 𝐷) |
92 | 3 | psrbagf 19186 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑘 ∈ 𝐷) → 𝑘:𝐼⟶ℕ0) |
93 | 87, 81, 92 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑘:𝐼⟶ℕ0) |
94 | 80 | simprd 478 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑘 ∘𝑟 ≤ 𝑥) |
95 | 3 | psrbagcon 19192 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝐷 ∧ 𝑘:𝐼⟶ℕ0 ∧ 𝑘 ∘𝑟
≤ 𝑥)) → ((𝑥 ∘𝑓
− 𝑘) ∈ 𝐷 ∧ (𝑥 ∘𝑓 − 𝑘) ∘𝑟
≤ 𝑥)) |
96 | 87, 91, 93, 94, 95 | syl13anc 1320 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑥 ∘𝑓 − 𝑘) ∈ 𝐷 ∧ (𝑥 ∘𝑓 − 𝑘) ∘𝑟
≤ 𝑥)) |
97 | 96 | simpld 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑘) ∈ 𝐷) |
98 | 90, 97 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑍‘(𝑥 ∘𝑓 − 𝑘)) ∈ (Base‘𝑅)) |
99 | 86 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑅 ∈ Ring) |
100 | 27 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅)) |
101 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) |
102 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑗 → (ℎ ∘𝑟 ≤ 𝑘 ↔ 𝑗 ∘𝑟 ≤ 𝑘)) |
103 | 102 | elrab 3331 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↔ (𝑗 ∈ 𝐷 ∧ 𝑗 ∘𝑟 ≤ 𝑘)) |
104 | 101, 103 | sylib 207 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → (𝑗 ∈ 𝐷 ∧ 𝑗 ∘𝑟 ≤ 𝑘)) |
105 | 104 | simpld 474 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑗 ∈ 𝐷) |
106 | 100, 105 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → (𝑋‘𝑗) ∈ (Base‘𝑅)) |
107 | 36 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅)) |
108 | 87 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝐼 ∈ 𝑉) |
109 | 81 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑘 ∈ 𝐷) |
110 | 108, 105,
49 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑗:𝐼⟶ℕ0) |
111 | 104 | simprd 478 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑗 ∘𝑟 ≤ 𝑘) |
112 | 3 | psrbagcon 19192 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑘 ∈ 𝐷 ∧ 𝑗:𝐼⟶ℕ0 ∧ 𝑗 ∘𝑟
≤ 𝑘)) → ((𝑘 ∘𝑓
− 𝑗) ∈ 𝐷 ∧ (𝑘 ∘𝑓 − 𝑗) ∘𝑟
≤ 𝑘)) |
113 | 108, 109,
110, 111, 112 | syl13anc 1320 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → ((𝑘 ∘𝑓 − 𝑗) ∈ 𝐷 ∧ (𝑘 ∘𝑓 − 𝑗) ∘𝑟
≤ 𝑘)) |
114 | 113 | simpld 474 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑗) ∈ 𝐷) |
115 | 107, 114 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → (𝑌‘(𝑘 ∘𝑓 − 𝑗)) ∈ (Base‘𝑅)) |
116 | 2, 63 | ringcl 18384 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑗) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘 ∘𝑓 − 𝑗)) ∈ (Base‘𝑅)) → ((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗))) ∈ (Base‘𝑅)) |
117 | 99, 106, 115, 116 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → ((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗))) ∈ (Base‘𝑅)) |
118 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗)))) = (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗)))) |
119 | | fvex 6113 |
. . . . . . . . . 10
⊢
(0g‘𝑅) ∈ V |
120 | 119 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) →
(0g‘𝑅)
∈ V) |
121 | 118, 89, 117, 120 | fsuppmptdm 8169 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗)))) finSupp
(0g‘𝑅)) |
122 | 2, 84, 85, 63, 86, 89, 98, 117, 121 | gsummulc1 18429 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑅 Σg (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ (((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗)))(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘))))) = ((𝑅 Σg (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗)))))(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘)))) |
123 | 98 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → (𝑍‘(𝑥 ∘𝑓 − 𝑘)) ∈ (Base‘𝑅)) |
124 | 2, 63 | ringass 18387 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ ((𝑋‘𝑗) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘 ∘𝑓 − 𝑗)) ∈ (Base‘𝑅) ∧ (𝑍‘(𝑥 ∘𝑓 − 𝑘)) ∈ (Base‘𝑅))) → (((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗)))(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘))) = ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘))))) |
125 | 99, 106, 115, 123, 124 | syl13anc 1320 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → (((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗)))(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘))) = ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘))))) |
126 | 3 | psrbagf 19186 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) → 𝑥:𝐼⟶ℕ0) |
127 | 19, 126 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥:𝐼⟶ℕ0) |
128 | 127 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑥:𝐼⟶ℕ0) |
129 | 128 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) ∧ 𝑧 ∈ 𝐼) → (𝑥‘𝑧) ∈
ℕ0) |
130 | 93 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑘:𝐼⟶ℕ0) |
131 | 130 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) ∧ 𝑧 ∈ 𝐼) → (𝑘‘𝑧) ∈
ℕ0) |
132 | 110 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) ∧ 𝑧 ∈ 𝐼) → (𝑗‘𝑧) ∈
ℕ0) |
133 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥‘𝑧) ∈ ℕ0 → (𝑥‘𝑧) ∈ ℂ) |
134 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘‘𝑧) ∈ ℕ0 → (𝑘‘𝑧) ∈ ℂ) |
135 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗‘𝑧) ∈ ℕ0 → (𝑗‘𝑧) ∈ ℂ) |
136 | | nnncan2 10197 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥‘𝑧) ∈ ℂ ∧ (𝑘‘𝑧) ∈ ℂ ∧ (𝑗‘𝑧) ∈ ℂ) → (((𝑥‘𝑧) − (𝑗‘𝑧)) − ((𝑘‘𝑧) − (𝑗‘𝑧))) = ((𝑥‘𝑧) − (𝑘‘𝑧))) |
137 | 133, 134,
135, 136 | syl3an 1360 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥‘𝑧) ∈ ℕ0 ∧ (𝑘‘𝑧) ∈ ℕ0 ∧ (𝑗‘𝑧) ∈ ℕ0) → (((𝑥‘𝑧) − (𝑗‘𝑧)) − ((𝑘‘𝑧) − (𝑗‘𝑧))) = ((𝑥‘𝑧) − (𝑘‘𝑧))) |
138 | 129, 131,
132, 137 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) ∧ 𝑧 ∈ 𝐼) → (((𝑥‘𝑧) − (𝑗‘𝑧)) − ((𝑘‘𝑧) − (𝑗‘𝑧))) = ((𝑥‘𝑧) − (𝑘‘𝑧))) |
139 | 138 | mpteq2dva 4672 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → (𝑧 ∈ 𝐼 ↦ (((𝑥‘𝑧) − (𝑗‘𝑧)) − ((𝑘‘𝑧) − (𝑗‘𝑧)))) = (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧) − (𝑘‘𝑧)))) |
140 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥‘𝑧) − (𝑗‘𝑧)) ∈ V |
141 | 140 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) ∧ 𝑧 ∈ 𝐼) → ((𝑥‘𝑧) − (𝑗‘𝑧)) ∈ V) |
142 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘‘𝑧) − (𝑗‘𝑧)) ∈ V |
143 | 142 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) ∧ 𝑧 ∈ 𝐼) → ((𝑘‘𝑧) − (𝑗‘𝑧)) ∈ V) |
144 | 128 | feqmptd 6159 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑥 = (𝑧 ∈ 𝐼 ↦ (𝑥‘𝑧))) |
145 | 110 | feqmptd 6159 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑗 = (𝑧 ∈ 𝐼 ↦ (𝑗‘𝑧))) |
146 | 108, 129,
132, 144, 145 | offval2 6812 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → (𝑥 ∘𝑓 − 𝑗) = (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧) − (𝑗‘𝑧)))) |
147 | 130 | feqmptd 6159 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → 𝑘 = (𝑧 ∈ 𝐼 ↦ (𝑘‘𝑧))) |
148 | 108, 131,
132, 147, 145 | offval2 6812 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑗) = (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧) − (𝑗‘𝑧)))) |
149 | 108, 141,
143, 146, 148 | offval2 6812 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → ((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗)) = (𝑧 ∈ 𝐼 ↦ (((𝑥‘𝑧) − (𝑗‘𝑧)) − ((𝑘‘𝑧) − (𝑗‘𝑧))))) |
150 | 108, 129,
131, 144, 147 | offval2 6812 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → (𝑥 ∘𝑓 − 𝑘) = (𝑧 ∈ 𝐼 ↦ ((𝑥‘𝑧) − (𝑘‘𝑧)))) |
151 | 139, 149,
150 | 3eqtr4d 2654 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → ((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗)) = (𝑥 ∘𝑓 − 𝑘)) |
152 | 151 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → (𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗))) = (𝑍‘(𝑥 ∘𝑓 − 𝑘))) |
153 | 152 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → ((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗)))) = ((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘)))) |
154 | 153 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗))))) = ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘))))) |
155 | 125, 154 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) ∧ 𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘}) → (((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗)))(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘))) = ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗)))))) |
156 | 155 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ (((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗)))(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘)))) = (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗))))))) |
157 | 156 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑅 Σg (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ (((𝑋‘𝑗)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑗)))(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘))))) = (𝑅 Σg (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗)))))))) |
158 | 83, 122, 157 | 3eqtr2d 2650 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (((𝑋 × 𝑌)‘𝑘)(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘))) = (𝑅 Σg (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗)))))))) |
159 | 158 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (((𝑋 × 𝑌)‘𝑘)(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘)))) = (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑅 Σg (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗))))))))) |
160 | 159 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑅 Σg (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (((𝑋 × 𝑌)‘𝑘)(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘))))) = (𝑅 Σg (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑅 Σg (𝑗 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘(𝑘 ∘𝑓 − 𝑗))(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− (𝑘
∘𝑓 − 𝑗)))))))))) |
161 | 8 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑌 ∈ 𝐵) |
162 | 10 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → 𝑍 ∈ 𝐵) |
163 | 1, 4, 63, 5, 3, 161, 162, 54 | psrmulval 19207 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑌 × 𝑍)‘(𝑥 ∘𝑓 − 𝑗)) = (𝑅 Σg (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))))) |
164 | 163 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑋‘𝑗)(.r‘𝑅)((𝑌 × 𝑍)‘(𝑥 ∘𝑓 − 𝑗))) = ((𝑋‘𝑗)(.r‘𝑅)(𝑅 Σg (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛))))))) |
165 | 3 | psrbaglefi 19193 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∘𝑓 − 𝑗) ∈ 𝐷) → {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ∈
Fin) |
166 | 46, 54, 165 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ∈
Fin) |
167 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
168 | 3, 167 | rab2ex 4743 |
. . . . . . . . . . . 12
⊢ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ∈
V |
169 | 168 | mptex 6390 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) ∈
V |
170 | | funmpt 5840 |
. . . . . . . . . . 11
⊢ Fun
(𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) |
171 | 169, 170,
119 | 3pm3.2i 1232 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) ∈ V
∧ Fun (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) ∧
(0g‘𝑅)
∈ V) |
172 | 171 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) ∈ V
∧ Fun (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) ∧
(0g‘𝑅)
∈ V)) |
173 | | suppssdm 7195 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) supp
(0g‘𝑅))
⊆ dom (𝑛 ∈
{ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) |
174 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) = (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) |
175 | 174 | dmmptss 5548 |
. . . . . . . . . . 11
⊢ dom
(𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) ⊆
{ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} |
176 | 173, 175 | sstri 3577 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) supp
(0g‘𝑅))
⊆ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} |
177 | 176 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) supp
(0g‘𝑅))
⊆ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)}) |
178 | | suppssfifsupp 8173 |
. . . . . . . . 9
⊢ ((((𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) ∈ V
∧ Fun (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) ∧
(0g‘𝑅)
∈ V) ∧ ({ℎ ∈
𝐷 ∣ ℎ ∘𝑟 ≤
(𝑥
∘𝑓 − 𝑗)} ∈ Fin ∧ ((𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) supp
(0g‘𝑅))
⊆ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)})) → (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) finSupp
(0g‘𝑅)) |
179 | 172, 166,
177, 178 | syl12anc 1316 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))) finSupp
(0g‘𝑅)) |
180 | 2, 84, 85, 63, 25, 166, 34, 65, 179 | gsummulc2 18430 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → (𝑅 Σg (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))))) = ((𝑋‘𝑗)(.r‘𝑅)(𝑅 Σg (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛))))))) |
181 | 164, 180 | eqtr4d 2647 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥}) → ((𝑋‘𝑗)(.r‘𝑅)((𝑌 × 𝑍)‘(𝑥 ∘𝑓 − 𝑗))) = (𝑅 Σg (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛))))))) |
182 | 181 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌 × 𝑍)‘(𝑥 ∘𝑓 − 𝑗)))) = (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑅 Σg (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛)))))))) |
183 | 182 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑅 Σg (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌 × 𝑍)‘(𝑥 ∘𝑓 − 𝑗))))) = (𝑅 Σg (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (𝑅 Σg (𝑛 ∈ {ℎ ∈ 𝐷 ∣ ℎ ∘𝑟 ≤ (𝑥 ∘𝑓
− 𝑗)} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌‘𝑛)(.r‘𝑅)(𝑍‘((𝑥 ∘𝑓 − 𝑗) ∘𝑓
− 𝑛))))))))) |
184 | 74, 160, 183 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑅 Σg (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (((𝑋 × 𝑌)‘𝑘)(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘))))) = (𝑅 Σg (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌 × 𝑍)‘(𝑥 ∘𝑓 − 𝑗)))))) |
185 | 9 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑋 × 𝑌) ∈ 𝐵) |
186 | 10 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑍 ∈ 𝐵) |
187 | 1, 4, 63, 5, 3, 185, 186, 21 | psrmulval 19207 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (((𝑋 × 𝑌) × 𝑍)‘𝑥) = (𝑅 Σg (𝑘 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ (((𝑋 × 𝑌)‘𝑘)(.r‘𝑅)(𝑍‘(𝑥 ∘𝑓 − 𝑘)))))) |
188 | 7 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑋 ∈ 𝐵) |
189 | 14 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑌 × 𝑍) ∈ 𝐵) |
190 | 1, 4, 63, 5, 3, 188, 189, 21 | psrmulval 19207 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑋 × (𝑌 × 𝑍))‘𝑥) = (𝑅 Σg (𝑗 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘𝑟 ≤ 𝑥} ↦ ((𝑋‘𝑗)(.r‘𝑅)((𝑌 × 𝑍)‘(𝑥 ∘𝑓 − 𝑗)))))) |
191 | 184, 187,
190 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (((𝑋 × 𝑌) × 𝑍)‘𝑥) = ((𝑋 × (𝑌 × 𝑍))‘𝑥)) |
192 | 13, 17, 191 | eqfnfvd 6222 |
1
⊢ (𝜑 → ((𝑋 × 𝑌) × 𝑍) = (𝑋 × (𝑌 × 𝑍))) |