Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  psrass1 Structured version   Visualization version   GIF version

Theorem psrass1 20650
 Description: Associative identity for the ring of power series. (Contributed by Mario Carneiro, 5-Jan-2015.)
Hypotheses
Ref Expression
psrring.s 𝑆 = (𝐼 mPwSer 𝑅)
psrring.i (𝜑𝐼𝑉)
psrring.r (𝜑𝑅 ∈ Ring)
psrass.d 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
psrass.t × = (.r𝑆)
psrass.b 𝐵 = (Base‘𝑆)
psrass.x (𝜑𝑋𝐵)
psrass.y (𝜑𝑌𝐵)
psrass.z (𝜑𝑍𝐵)
Assertion
Ref Expression
psrass1 (𝜑 → ((𝑋 × 𝑌) × 𝑍) = (𝑋 × (𝑌 × 𝑍)))
Distinct variable groups:   𝑓,𝐼   𝑅,𝑓   𝑓,𝑋   𝑓,𝑍   𝑓,𝑌
Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑓)   𝐷(𝑓)   𝑆(𝑓)   × (𝑓)   𝑉(𝑓)

Proof of Theorem psrass1
Dummy variables 𝑥 𝑘 𝑧 𝑔 𝑗 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 psrring.s . . . 4 𝑆 = (𝐼 mPwSer 𝑅)
2 eqid 2824 . . . 4 (Base‘𝑅) = (Base‘𝑅)
3 psrass.d . . . 4 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
4 psrass.b . . . 4 𝐵 = (Base‘𝑆)
5 psrass.t . . . . 5 × = (.r𝑆)
6 psrring.r . . . . 5 (𝜑𝑅 ∈ Ring)
7 psrass.x . . . . . 6 (𝜑𝑋𝐵)
8 psrass.y . . . . . 6 (𝜑𝑌𝐵)
91, 4, 5, 6, 7, 8psrmulcl 20633 . . . . 5 (𝜑 → (𝑋 × 𝑌) ∈ 𝐵)
10 psrass.z . . . . 5 (𝜑𝑍𝐵)
111, 4, 5, 6, 9, 10psrmulcl 20633 . . . 4 (𝜑 → ((𝑋 × 𝑌) × 𝑍) ∈ 𝐵)
121, 2, 3, 4, 11psrelbas 20624 . . 3 (𝜑 → ((𝑋 × 𝑌) × 𝑍):𝐷⟶(Base‘𝑅))
1312ffnd 6504 . 2 (𝜑 → ((𝑋 × 𝑌) × 𝑍) Fn 𝐷)
141, 4, 5, 6, 8, 10psrmulcl 20633 . . . . 5 (𝜑 → (𝑌 × 𝑍) ∈ 𝐵)
151, 4, 5, 6, 7, 14psrmulcl 20633 . . . 4 (𝜑 → (𝑋 × (𝑌 × 𝑍)) ∈ 𝐵)
161, 2, 3, 4, 15psrelbas 20624 . . 3 (𝜑 → (𝑋 × (𝑌 × 𝑍)):𝐷⟶(Base‘𝑅))
1716ffnd 6504 . 2 (𝜑 → (𝑋 × (𝑌 × 𝑍)) Fn 𝐷)
18 eqid 2824 . . . . 5 {𝑔𝐷𝑔r𝑥} = {𝑔𝐷𝑔r𝑥}
19 psrring.i . . . . . 6 (𝜑𝐼𝑉)
2019adantr 484 . . . . 5 ((𝜑𝑥𝐷) → 𝐼𝑉)
21 simpr 488 . . . . 5 ((𝜑𝑥𝐷) → 𝑥𝐷)
22 ringcmn 19334 . . . . . . 7 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
236, 22syl 17 . . . . . 6 (𝜑𝑅 ∈ CMnd)
2423adantr 484 . . . . 5 ((𝜑𝑥𝐷) → 𝑅 ∈ CMnd)
256ad2antrr 725 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑅 ∈ Ring)
2625adantr 484 . . . . . . 7 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → 𝑅 ∈ Ring)
271, 2, 3, 4, 7psrelbas 20624 . . . . . . . . . 10 (𝜑𝑋:𝐷⟶(Base‘𝑅))
2827ad2antrr 725 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑋:𝐷⟶(Base‘𝑅))
29 simpr 488 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑗 ∈ {𝑔𝐷𝑔r𝑥})
30 breq1 5055 . . . . . . . . . . . 12 (𝑔 = 𝑗 → (𝑔r𝑥𝑗r𝑥))
3130elrab 3666 . . . . . . . . . . 11 (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↔ (𝑗𝐷𝑗r𝑥))
3229, 31sylib 221 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑗𝐷𝑗r𝑥))
3332simpld 498 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑗𝐷)
3428, 33ffvelrnd 6843 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑋𝑗) ∈ (Base‘𝑅))
3534adantr 484 . . . . . . 7 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → (𝑋𝑗) ∈ (Base‘𝑅))
361, 2, 3, 4, 8psrelbas 20624 . . . . . . . . . 10 (𝜑𝑌:𝐷⟶(Base‘𝑅))
3736ad3antrrr 729 . . . . . . . . 9 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → 𝑌:𝐷⟶(Base‘𝑅))
38 simpr 488 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)})
39 breq1 5055 . . . . . . . . . . . 12 ( = 𝑛 → (r ≤ (𝑥f𝑗) ↔ 𝑛r ≤ (𝑥f𝑗)))
4039elrab 3666 . . . . . . . . . . 11 (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↔ (𝑛𝐷𝑛r ≤ (𝑥f𝑗)))
4138, 40sylib 221 . . . . . . . . . 10 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → (𝑛𝐷𝑛r ≤ (𝑥f𝑗)))
4241simpld 498 . . . . . . . . 9 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → 𝑛𝐷)
4337, 42ffvelrnd 6843 . . . . . . . 8 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → (𝑌𝑛) ∈ (Base‘𝑅))
441, 2, 3, 4, 10psrelbas 20624 . . . . . . . . . 10 (𝜑𝑍:𝐷⟶(Base‘𝑅))
4544ad3antrrr 729 . . . . . . . . 9 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → 𝑍:𝐷⟶(Base‘𝑅))
4619ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝐼𝑉)
4746adantr 484 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → 𝐼𝑉)
48 simplr 768 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑥𝐷)
493psrbagf 20610 . . . . . . . . . . . . . . 15 ((𝐼𝑉𝑗𝐷) → 𝑗:𝐼⟶ℕ0)
5046, 33, 49syl2anc 587 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑗:𝐼⟶ℕ0)
5132simprd 499 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑗r𝑥)
523psrbagcon 20616 . . . . . . . . . . . . . 14 ((𝐼𝑉 ∧ (𝑥𝐷𝑗:𝐼⟶ℕ0𝑗r𝑥)) → ((𝑥f𝑗) ∈ 𝐷 ∧ (𝑥f𝑗) ∘r𝑥))
5346, 48, 50, 51, 52syl13anc 1369 . . . . . . . . . . . . 13 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑥f𝑗) ∈ 𝐷 ∧ (𝑥f𝑗) ∘r𝑥))
5453simpld 498 . . . . . . . . . . . 12 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑥f𝑗) ∈ 𝐷)
5554adantr 484 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → (𝑥f𝑗) ∈ 𝐷)
563psrbagf 20610 . . . . . . . . . . . 12 ((𝐼𝑉𝑛𝐷) → 𝑛:𝐼⟶ℕ0)
5747, 42, 56syl2anc 587 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → 𝑛:𝐼⟶ℕ0)
5841simprd 499 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → 𝑛r ≤ (𝑥f𝑗))
593psrbagcon 20616 . . . . . . . . . . 11 ((𝐼𝑉 ∧ ((𝑥f𝑗) ∈ 𝐷𝑛:𝐼⟶ℕ0𝑛r ≤ (𝑥f𝑗))) → (((𝑥f𝑗) ∘f𝑛) ∈ 𝐷 ∧ ((𝑥f𝑗) ∘f𝑛) ∘r ≤ (𝑥f𝑗)))
6047, 55, 57, 58, 59syl13anc 1369 . . . . . . . . . 10 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → (((𝑥f𝑗) ∘f𝑛) ∈ 𝐷 ∧ ((𝑥f𝑗) ∘f𝑛) ∘r ≤ (𝑥f𝑗)))
6160simpld 498 . . . . . . . . 9 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → ((𝑥f𝑗) ∘f𝑛) ∈ 𝐷)
6245, 61ffvelrnd 6843 . . . . . . . 8 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → (𝑍‘((𝑥f𝑗) ∘f𝑛)) ∈ (Base‘𝑅))
63 eqid 2824 . . . . . . . . 9 (.r𝑅) = (.r𝑅)
642, 63ringcl 19314 . . . . . . . 8 ((𝑅 ∈ Ring ∧ (𝑌𝑛) ∈ (Base‘𝑅) ∧ (𝑍‘((𝑥f𝑗) ∘f𝑛)) ∈ (Base‘𝑅)) → ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛))) ∈ (Base‘𝑅))
6526, 43, 62, 64syl3anc 1368 . . . . . . 7 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛))) ∈ (Base‘𝑅))
662, 63ringcl 19314 . . . . . . 7 ((𝑅 ∈ Ring ∧ (𝑋𝑗) ∈ (Base‘𝑅) ∧ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛))) ∈ (Base‘𝑅)) → ((𝑋𝑗)(.r𝑅)((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) ∈ (Base‘𝑅))
6726, 35, 65, 66syl3anc 1368 . . . . . 6 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)}) → ((𝑋𝑗)(.r𝑅)((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) ∈ (Base‘𝑅))
6867anasss 470 . . . . 5 (((𝜑𝑥𝐷) ∧ (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ∧ 𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)})) → ((𝑋𝑗)(.r𝑅)((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) ∈ (Base‘𝑅))
69 fveq2 6661 . . . . . . 7 (𝑛 = (𝑘f𝑗) → (𝑌𝑛) = (𝑌‘(𝑘f𝑗)))
70 oveq2 7157 . . . . . . . 8 (𝑛 = (𝑘f𝑗) → ((𝑥f𝑗) ∘f𝑛) = ((𝑥f𝑗) ∘f − (𝑘f𝑗)))
7170fveq2d 6665 . . . . . . 7 (𝑛 = (𝑘f𝑗) → (𝑍‘((𝑥f𝑗) ∘f𝑛)) = (𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗))))
7269, 71oveq12d 7167 . . . . . 6 (𝑛 = (𝑘f𝑗) → ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛))) = ((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗)))))
7372oveq2d 7165 . . . . 5 (𝑛 = (𝑘f𝑗) → ((𝑋𝑗)(.r𝑅)((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) = ((𝑋𝑗)(.r𝑅)((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗))))))
743, 18, 20, 21, 2, 24, 68, 73psrass1lem 20622 . . . 4 ((𝜑𝑥𝐷) → (𝑅 Σg (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑅 Σg (𝑗 ∈ {𝐷r𝑘} ↦ ((𝑋𝑗)(.r𝑅)((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗))))))))) = (𝑅 Σg (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑅 Σg (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑋𝑗)(.r𝑅)((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))))))))
757ad2antrr 725 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑋𝐵)
768ad2antrr 725 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑌𝐵)
77 simpr 488 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑘 ∈ {𝑔𝐷𝑔r𝑥})
78 breq1 5055 . . . . . . . . . . . 12 (𝑔 = 𝑘 → (𝑔r𝑥𝑘r𝑥))
7978elrab 3666 . . . . . . . . . . 11 (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↔ (𝑘𝐷𝑘r𝑥))
8077, 79sylib 221 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑘𝐷𝑘r𝑥))
8180simpld 498 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑘𝐷)
821, 4, 63, 5, 3, 75, 76, 81psrmulval 20631 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑋 × 𝑌)‘𝑘) = (𝑅 Σg (𝑗 ∈ {𝐷r𝑘} ↦ ((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗))))))
8382oveq1d 7164 . . . . . . 7 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (((𝑋 × 𝑌)‘𝑘)(.r𝑅)(𝑍‘(𝑥f𝑘))) = ((𝑅 Σg (𝑗 ∈ {𝐷r𝑘} ↦ ((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗)))))(.r𝑅)(𝑍‘(𝑥f𝑘))))
84 eqid 2824 . . . . . . . 8 (0g𝑅) = (0g𝑅)
85 eqid 2824 . . . . . . . 8 (+g𝑅) = (+g𝑅)
866ad2antrr 725 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑅 ∈ Ring)
8719ad2antrr 725 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝐼𝑉)
883psrbaglefi 20617 . . . . . . . . 9 ((𝐼𝑉𝑘𝐷) → {𝐷r𝑘} ∈ Fin)
8987, 81, 88syl2anc 587 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → {𝐷r𝑘} ∈ Fin)
9044ad2antrr 725 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑍:𝐷⟶(Base‘𝑅))
91 simplr 768 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑥𝐷)
923psrbagf 20610 . . . . . . . . . . . 12 ((𝐼𝑉𝑘𝐷) → 𝑘:𝐼⟶ℕ0)
9387, 81, 92syl2anc 587 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑘:𝐼⟶ℕ0)
9480simprd 499 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑘r𝑥)
953psrbagcon 20616 . . . . . . . . . . 11 ((𝐼𝑉 ∧ (𝑥𝐷𝑘:𝐼⟶ℕ0𝑘r𝑥)) → ((𝑥f𝑘) ∈ 𝐷 ∧ (𝑥f𝑘) ∘r𝑥))
9687, 91, 93, 94, 95syl13anc 1369 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑥f𝑘) ∈ 𝐷 ∧ (𝑥f𝑘) ∘r𝑥))
9796simpld 498 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑥f𝑘) ∈ 𝐷)
9890, 97ffvelrnd 6843 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑍‘(𝑥f𝑘)) ∈ (Base‘𝑅))
9986adantr 484 . . . . . . . . 9 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑅 ∈ Ring)
10027ad3antrrr 729 . . . . . . . . . 10 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑋:𝐷⟶(Base‘𝑅))
101 simpr 488 . . . . . . . . . . . 12 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑗 ∈ {𝐷r𝑘})
102 breq1 5055 . . . . . . . . . . . . 13 ( = 𝑗 → (r𝑘𝑗r𝑘))
103102elrab 3666 . . . . . . . . . . . 12 (𝑗 ∈ {𝐷r𝑘} ↔ (𝑗𝐷𝑗r𝑘))
104101, 103sylib 221 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → (𝑗𝐷𝑗r𝑘))
105104simpld 498 . . . . . . . . . 10 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑗𝐷)
106100, 105ffvelrnd 6843 . . . . . . . . 9 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → (𝑋𝑗) ∈ (Base‘𝑅))
10736ad3antrrr 729 . . . . . . . . . 10 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑌:𝐷⟶(Base‘𝑅))
10887adantr 484 . . . . . . . . . . . 12 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝐼𝑉)
10981adantr 484 . . . . . . . . . . . 12 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑘𝐷)
110108, 105, 49syl2anc 587 . . . . . . . . . . . 12 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑗:𝐼⟶ℕ0)
111104simprd 499 . . . . . . . . . . . 12 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑗r𝑘)
1123psrbagcon 20616 . . . . . . . . . . . 12 ((𝐼𝑉 ∧ (𝑘𝐷𝑗:𝐼⟶ℕ0𝑗r𝑘)) → ((𝑘f𝑗) ∈ 𝐷 ∧ (𝑘f𝑗) ∘r𝑘))
113108, 109, 110, 111, 112syl13anc 1369 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → ((𝑘f𝑗) ∈ 𝐷 ∧ (𝑘f𝑗) ∘r𝑘))
114113simpld 498 . . . . . . . . . 10 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → (𝑘f𝑗) ∈ 𝐷)
115107, 114ffvelrnd 6843 . . . . . . . . 9 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → (𝑌‘(𝑘f𝑗)) ∈ (Base‘𝑅))
1162, 63ringcl 19314 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ (𝑋𝑗) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘f𝑗)) ∈ (Base‘𝑅)) → ((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗))) ∈ (Base‘𝑅))
11799, 106, 115, 116syl3anc 1368 . . . . . . . 8 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → ((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗))) ∈ (Base‘𝑅))
118 eqid 2824 . . . . . . . . 9 (𝑗 ∈ {𝐷r𝑘} ↦ ((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗)))) = (𝑗 ∈ {𝐷r𝑘} ↦ ((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗))))
119 fvex 6674 . . . . . . . . . 10 (0g𝑅) ∈ V
120119a1i 11 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (0g𝑅) ∈ V)
121118, 89, 117, 120fsuppmptdm 8841 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑗 ∈ {𝐷r𝑘} ↦ ((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗)))) finSupp (0g𝑅))
1222, 84, 85, 63, 86, 89, 98, 117, 121gsummulc1 19359 . . . . . . 7 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑅 Σg (𝑗 ∈ {𝐷r𝑘} ↦ (((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗)))(.r𝑅)(𝑍‘(𝑥f𝑘))))) = ((𝑅 Σg (𝑗 ∈ {𝐷r𝑘} ↦ ((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗)))))(.r𝑅)(𝑍‘(𝑥f𝑘))))
12398adantr 484 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → (𝑍‘(𝑥f𝑘)) ∈ (Base‘𝑅))
1242, 63ringass 19317 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ ((𝑋𝑗) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘f𝑗)) ∈ (Base‘𝑅) ∧ (𝑍‘(𝑥f𝑘)) ∈ (Base‘𝑅))) → (((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗)))(.r𝑅)(𝑍‘(𝑥f𝑘))) = ((𝑋𝑗)(.r𝑅)((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘(𝑥f𝑘)))))
12599, 106, 115, 123, 124syl13anc 1369 . . . . . . . . . 10 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → (((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗)))(.r𝑅)(𝑍‘(𝑥f𝑘))) = ((𝑋𝑗)(.r𝑅)((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘(𝑥f𝑘)))))
1263psrbagf 20610 . . . . . . . . . . . . . . . . . . 19 ((𝐼𝑉𝑥𝐷) → 𝑥:𝐼⟶ℕ0)
12719, 126sylan 583 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐷) → 𝑥:𝐼⟶ℕ0)
128127ad2antrr 725 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑥:𝐼⟶ℕ0)
129128ffvelrnda 6842 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) ∧ 𝑧𝐼) → (𝑥𝑧) ∈ ℕ0)
13093adantr 484 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑘:𝐼⟶ℕ0)
131130ffvelrnda 6842 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) ∧ 𝑧𝐼) → (𝑘𝑧) ∈ ℕ0)
132110ffvelrnda 6842 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) ∧ 𝑧𝐼) → (𝑗𝑧) ∈ ℕ0)
133 nn0cn 11904 . . . . . . . . . . . . . . . . 17 ((𝑥𝑧) ∈ ℕ0 → (𝑥𝑧) ∈ ℂ)
134 nn0cn 11904 . . . . . . . . . . . . . . . . 17 ((𝑘𝑧) ∈ ℕ0 → (𝑘𝑧) ∈ ℂ)
135 nn0cn 11904 . . . . . . . . . . . . . . . . 17 ((𝑗𝑧) ∈ ℕ0 → (𝑗𝑧) ∈ ℂ)
136 nnncan2 10921 . . . . . . . . . . . . . . . . 17 (((𝑥𝑧) ∈ ℂ ∧ (𝑘𝑧) ∈ ℂ ∧ (𝑗𝑧) ∈ ℂ) → (((𝑥𝑧) − (𝑗𝑧)) − ((𝑘𝑧) − (𝑗𝑧))) = ((𝑥𝑧) − (𝑘𝑧)))
137133, 134, 135, 136syl3an 1157 . . . . . . . . . . . . . . . 16 (((𝑥𝑧) ∈ ℕ0 ∧ (𝑘𝑧) ∈ ℕ0 ∧ (𝑗𝑧) ∈ ℕ0) → (((𝑥𝑧) − (𝑗𝑧)) − ((𝑘𝑧) − (𝑗𝑧))) = ((𝑥𝑧) − (𝑘𝑧)))
138129, 131, 132, 137syl3anc 1368 . . . . . . . . . . . . . . 15 (((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) ∧ 𝑧𝐼) → (((𝑥𝑧) − (𝑗𝑧)) − ((𝑘𝑧) − (𝑗𝑧))) = ((𝑥𝑧) − (𝑘𝑧)))
139138mpteq2dva 5147 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → (𝑧𝐼 ↦ (((𝑥𝑧) − (𝑗𝑧)) − ((𝑘𝑧) − (𝑗𝑧)))) = (𝑧𝐼 ↦ ((𝑥𝑧) − (𝑘𝑧))))
140 ovexd 7184 . . . . . . . . . . . . . . 15 (((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) ∧ 𝑧𝐼) → ((𝑥𝑧) − (𝑗𝑧)) ∈ V)
141 ovexd 7184 . . . . . . . . . . . . . . 15 (((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) ∧ 𝑧𝐼) → ((𝑘𝑧) − (𝑗𝑧)) ∈ V)
142128feqmptd 6724 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑥 = (𝑧𝐼 ↦ (𝑥𝑧)))
143110feqmptd 6724 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑗 = (𝑧𝐼 ↦ (𝑗𝑧)))
144108, 129, 132, 142, 143offval2 7420 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → (𝑥f𝑗) = (𝑧𝐼 ↦ ((𝑥𝑧) − (𝑗𝑧))))
145130feqmptd 6724 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → 𝑘 = (𝑧𝐼 ↦ (𝑘𝑧)))
146108, 131, 132, 145, 143offval2 7420 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → (𝑘f𝑗) = (𝑧𝐼 ↦ ((𝑘𝑧) − (𝑗𝑧))))
147108, 140, 141, 144, 146offval2 7420 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → ((𝑥f𝑗) ∘f − (𝑘f𝑗)) = (𝑧𝐼 ↦ (((𝑥𝑧) − (𝑗𝑧)) − ((𝑘𝑧) − (𝑗𝑧)))))
148108, 129, 131, 142, 145offval2 7420 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → (𝑥f𝑘) = (𝑧𝐼 ↦ ((𝑥𝑧) − (𝑘𝑧))))
149139, 147, 1483eqtr4d 2869 . . . . . . . . . . . . 13 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → ((𝑥f𝑗) ∘f − (𝑘f𝑗)) = (𝑥f𝑘))
150149fveq2d 6665 . . . . . . . . . . . 12 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → (𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗))) = (𝑍‘(𝑥f𝑘)))
151150oveq2d 7165 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → ((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗)))) = ((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘(𝑥f𝑘))))
152151oveq2d 7165 . . . . . . . . . 10 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → ((𝑋𝑗)(.r𝑅)((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗))))) = ((𝑋𝑗)(.r𝑅)((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘(𝑥f𝑘)))))
153125, 152eqtr4d 2862 . . . . . . . . 9 ((((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑗 ∈ {𝐷r𝑘}) → (((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗)))(.r𝑅)(𝑍‘(𝑥f𝑘))) = ((𝑋𝑗)(.r𝑅)((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗))))))
154153mpteq2dva 5147 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑗 ∈ {𝐷r𝑘} ↦ (((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗)))(.r𝑅)(𝑍‘(𝑥f𝑘)))) = (𝑗 ∈ {𝐷r𝑘} ↦ ((𝑋𝑗)(.r𝑅)((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗)))))))
155154oveq2d 7165 . . . . . . 7 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑅 Σg (𝑗 ∈ {𝐷r𝑘} ↦ (((𝑋𝑗)(.r𝑅)(𝑌‘(𝑘f𝑗)))(.r𝑅)(𝑍‘(𝑥f𝑘))))) = (𝑅 Σg (𝑗 ∈ {𝐷r𝑘} ↦ ((𝑋𝑗)(.r𝑅)((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗))))))))
15683, 122, 1553eqtr2d 2865 . . . . . 6 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (((𝑋 × 𝑌)‘𝑘)(.r𝑅)(𝑍‘(𝑥f𝑘))) = (𝑅 Σg (𝑗 ∈ {𝐷r𝑘} ↦ ((𝑋𝑗)(.r𝑅)((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗))))))))
157156mpteq2dva 5147 . . . . 5 ((𝜑𝑥𝐷) → (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ (((𝑋 × 𝑌)‘𝑘)(.r𝑅)(𝑍‘(𝑥f𝑘)))) = (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑅 Σg (𝑗 ∈ {𝐷r𝑘} ↦ ((𝑋𝑗)(.r𝑅)((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗)))))))))
158157oveq2d 7165 . . . 4 ((𝜑𝑥𝐷) → (𝑅 Σg (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ (((𝑋 × 𝑌)‘𝑘)(.r𝑅)(𝑍‘(𝑥f𝑘))))) = (𝑅 Σg (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑅 Σg (𝑗 ∈ {𝐷r𝑘} ↦ ((𝑋𝑗)(.r𝑅)((𝑌‘(𝑘f𝑗))(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f − (𝑘f𝑗))))))))))
1598ad2antrr 725 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑌𝐵)
16010ad2antrr 725 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑍𝐵)
1611, 4, 63, 5, 3, 159, 160, 54psrmulval 20631 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑌 × 𝑍)‘(𝑥f𝑗)) = (𝑅 Σg (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛))))))
162161oveq2d 7165 . . . . . . 7 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑋𝑗)(.r𝑅)((𝑌 × 𝑍)‘(𝑥f𝑗))) = ((𝑋𝑗)(.r𝑅)(𝑅 Σg (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))))))
1633psrbaglefi 20617 . . . . . . . . 9 ((𝐼𝑉 ∧ (𝑥f𝑗) ∈ 𝐷) → {𝐷r ≤ (𝑥f𝑗)} ∈ Fin)
16446, 54, 163syl2anc 587 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → {𝐷r ≤ (𝑥f𝑗)} ∈ Fin)
165 ovex 7182 . . . . . . . . . . . . 13 (ℕ0m 𝐼) ∈ V
1663, 165rab2ex 5224 . . . . . . . . . . . 12 {𝐷r ≤ (𝑥f𝑗)} ∈ V
167166mptex 6977 . . . . . . . . . . 11 (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) ∈ V
168 funmpt 6381 . . . . . . . . . . 11 Fun (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛))))
169167, 168, 1193pm3.2i 1336 . . . . . . . . . 10 ((𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) ∈ V ∧ Fun (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) ∧ (0g𝑅) ∈ V)
170169a1i 11 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) ∈ V ∧ Fun (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) ∧ (0g𝑅) ∈ V))
171 suppssdm 7839 . . . . . . . . . . 11 ((𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) supp (0g𝑅)) ⊆ dom (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛))))
172 eqid 2824 . . . . . . . . . . . 12 (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) = (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛))))
173172dmmptss 6082 . . . . . . . . . . 11 dom (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) ⊆ {𝐷r ≤ (𝑥f𝑗)}
174171, 173sstri 3962 . . . . . . . . . 10 ((𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) supp (0g𝑅)) ⊆ {𝐷r ≤ (𝑥f𝑗)}
175174a1i 11 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) supp (0g𝑅)) ⊆ {𝐷r ≤ (𝑥f𝑗)})
176 suppssfifsupp 8845 . . . . . . . . 9 ((((𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) ∈ V ∧ Fun (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) ∧ (0g𝑅) ∈ V) ∧ ({𝐷r ≤ (𝑥f𝑗)} ∈ Fin ∧ ((𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) supp (0g𝑅)) ⊆ {𝐷r ≤ (𝑥f𝑗)})) → (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) finSupp (0g𝑅))
177170, 164, 175, 176syl12anc 835 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))) finSupp (0g𝑅))
1782, 84, 85, 63, 25, 164, 34, 65, 177gsummulc2 19360 . . . . . . 7 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑅 Σg (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑋𝑗)(.r𝑅)((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))))) = ((𝑋𝑗)(.r𝑅)(𝑅 Σg (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))))))
179162, 178eqtr4d 2862 . . . . . 6 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑋𝑗)(.r𝑅)((𝑌 × 𝑍)‘(𝑥f𝑗))) = (𝑅 Σg (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑋𝑗)(.r𝑅)((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))))))
180179mpteq2dva 5147 . . . . 5 ((𝜑𝑥𝐷) → (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑗)(.r𝑅)((𝑌 × 𝑍)‘(𝑥f𝑗)))) = (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑅 Σg (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑋𝑗)(.r𝑅)((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛))))))))
181180oveq2d 7165 . . . 4 ((𝜑𝑥𝐷) → (𝑅 Σg (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑗)(.r𝑅)((𝑌 × 𝑍)‘(𝑥f𝑗))))) = (𝑅 Σg (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑅 Σg (𝑛 ∈ {𝐷r ≤ (𝑥f𝑗)} ↦ ((𝑋𝑗)(.r𝑅)((𝑌𝑛)(.r𝑅)(𝑍‘((𝑥f𝑗) ∘f𝑛)))))))))
18274, 158, 1813eqtr4d 2869 . . 3 ((𝜑𝑥𝐷) → (𝑅 Σg (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ (((𝑋 × 𝑌)‘𝑘)(.r𝑅)(𝑍‘(𝑥f𝑘))))) = (𝑅 Σg (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑗)(.r𝑅)((𝑌 × 𝑍)‘(𝑥f𝑗))))))
1839adantr 484 . . . 4 ((𝜑𝑥𝐷) → (𝑋 × 𝑌) ∈ 𝐵)
18410adantr 484 . . . 4 ((𝜑𝑥𝐷) → 𝑍𝐵)
1851, 4, 63, 5, 3, 183, 184, 21psrmulval 20631 . . 3 ((𝜑𝑥𝐷) → (((𝑋 × 𝑌) × 𝑍)‘𝑥) = (𝑅 Σg (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ (((𝑋 × 𝑌)‘𝑘)(.r𝑅)(𝑍‘(𝑥f𝑘))))))
1867adantr 484 . . . 4 ((𝜑𝑥𝐷) → 𝑋𝐵)
18714adantr 484 . . . 4 ((𝜑𝑥𝐷) → (𝑌 × 𝑍) ∈ 𝐵)
1881, 4, 63, 5, 3, 186, 187, 21psrmulval 20631 . . 3 ((𝜑𝑥𝐷) → ((𝑋 × (𝑌 × 𝑍))‘𝑥) = (𝑅 Σg (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑗)(.r𝑅)((𝑌 × 𝑍)‘(𝑥f𝑗))))))
189182, 185, 1883eqtr4d 2869 . 2 ((𝜑𝑥𝐷) → (((𝑋 × 𝑌) × 𝑍)‘𝑥) = ((𝑋 × (𝑌 × 𝑍))‘𝑥))
19013, 17, 189eqfnfvd 6796 1 (𝜑 → ((𝑋 × 𝑌) × 𝑍) = (𝑋 × (𝑌 × 𝑍)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115  {crab 3137  Vcvv 3480   ⊆ wss 3919   class class class wbr 5052   ↦ cmpt 5132  ◡ccnv 5541  dom cdm 5542   “ cima 5545  Fun wfun 6337  ⟶wf 6339  ‘cfv 6343  (class class class)co 7149   ∘f cof 7401   ∘r cofr 7402   supp csupp 7826   ↑m cmap 8402  Fincfn 8505   finSupp cfsupp 8830  ℂcc 10533   ≤ cle 10674   − cmin 10868  ℕcn 11634  ℕ0cn0 11894  Basecbs 16483  +gcplusg 16565  .rcmulr 16566  0gc0g 16713   Σg cgsu 16714  CMndccmn 18906  Ringcrg 19297   mPwSer cmps 20596 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-of 7403  df-ofr 7404  df-om 7575  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8285  df-map 8404  df-pm 8405  df-ixp 8458  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-fsupp 8831  df-oi 8971  df-card 9365  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-nn 11635  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702  df-8 11703  df-9 11704  df-n0 11895  df-z 11979  df-uz 12241  df-fz 12895  df-fzo 13038  df-seq 13374  df-hash 13696  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-mulr 16579  df-sca 16581  df-vsca 16582  df-tset 16584  df-0g 16715  df-gsum 16716  df-mre 16857  df-mrc 16858  df-acs 16860  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-mhm 17956  df-submnd 17957  df-grp 18106  df-minusg 18107  df-mulg 18225  df-ghm 18356  df-cntz 18447  df-cmn 18908  df-abl 18909  df-mgp 19240  df-ur 19252  df-ring 19299  df-psr 20601 This theorem is referenced by:  psrring  20656
 Copyright terms: Public domain W3C validator