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

Theorem psrdi 20778
Description: Distributive law for the ring of power series (left-distributivity). (Contributed by Mario Carneiro, 7-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 (𝜑𝑍𝐵)
psrdi.a + = (+g𝑆)
Assertion
Ref Expression
psrdi (𝜑 → (𝑋 × (𝑌 + 𝑍)) = ((𝑋 × 𝑌) + (𝑋 × 𝑍)))
Distinct variable groups:   𝑓,𝐼   𝑅,𝑓   𝑓,𝑋   𝑓,𝑍   𝑓,𝑌
Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑓)   𝐷(𝑓)   + (𝑓)   𝑆(𝑓)   × (𝑓)   𝑉(𝑓)

Proof of Theorem psrdi
Dummy variables 𝑥 𝑘 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 psrring.s . . . . . . . . . . . . 13 𝑆 = (𝐼 mPwSer 𝑅)
2 psrass.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝑆)
3 eqid 2738 . . . . . . . . . . . . 13 (+g𝑅) = (+g𝑅)
4 psrdi.a . . . . . . . . . . . . 13 + = (+g𝑆)
5 psrass.y . . . . . . . . . . . . 13 (𝜑𝑌𝐵)
6 psrass.z . . . . . . . . . . . . 13 (𝜑𝑍𝐵)
71, 2, 3, 4, 5, 6psradd 20754 . . . . . . . . . . . 12 (𝜑 → (𝑌 + 𝑍) = (𝑌f (+g𝑅)𝑍))
87fveq1d 6670 . . . . . . . . . . 11 (𝜑 → ((𝑌 + 𝑍)‘(𝑘f𝑥)) = ((𝑌f (+g𝑅)𝑍)‘(𝑘f𝑥)))
98ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑌 + 𝑍)‘(𝑘f𝑥)) = ((𝑌f (+g𝑅)𝑍)‘(𝑘f𝑥)))
10 ssrab2 3967 . . . . . . . . . . . 12 {𝑦𝐷𝑦r𝑘} ⊆ 𝐷
11 simplr 769 . . . . . . . . . . . . 13 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑘𝐷)
12 simpr 488 . . . . . . . . . . . . 13 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑥 ∈ {𝑦𝐷𝑦r𝑘})
13 psrass.d . . . . . . . . . . . . . 14 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
14 eqid 2738 . . . . . . . . . . . . . 14 {𝑦𝐷𝑦r𝑘} = {𝑦𝐷𝑦r𝑘}
1513, 14psrbagconcl 20740 . . . . . . . . . . . . 13 ((𝑘𝐷𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑘f𝑥) ∈ {𝑦𝐷𝑦r𝑘})
1611, 12, 15syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑘f𝑥) ∈ {𝑦𝐷𝑦r𝑘})
1710, 16sseldi 3873 . . . . . . . . . . 11 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑘f𝑥) ∈ 𝐷)
18 eqid 2738 . . . . . . . . . . . . . . 15 (Base‘𝑅) = (Base‘𝑅)
191, 18, 13, 2, 5psrelbas 20751 . . . . . . . . . . . . . 14 (𝜑𝑌:𝐷⟶(Base‘𝑅))
2019ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑌:𝐷⟶(Base‘𝑅))
2120ffnd 6499 . . . . . . . . . . . 12 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑌 Fn 𝐷)
221, 18, 13, 2, 6psrelbas 20751 . . . . . . . . . . . . . 14 (𝜑𝑍:𝐷⟶(Base‘𝑅))
2322ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑍:𝐷⟶(Base‘𝑅))
2423ffnd 6499 . . . . . . . . . . . 12 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑍 Fn 𝐷)
25 ovex 7197 . . . . . . . . . . . . . 14 (ℕ0m 𝐼) ∈ V
2613, 25rabex2 5199 . . . . . . . . . . . . 13 𝐷 ∈ V
2726a1i 11 . . . . . . . . . . . 12 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝐷 ∈ V)
28 inidm 4107 . . . . . . . . . . . 12 (𝐷𝐷) = 𝐷
29 eqidd 2739 . . . . . . . . . . . 12 ((((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) ∧ (𝑘f𝑥) ∈ 𝐷) → (𝑌‘(𝑘f𝑥)) = (𝑌‘(𝑘f𝑥)))
30 eqidd 2739 . . . . . . . . . . . 12 ((((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) ∧ (𝑘f𝑥) ∈ 𝐷) → (𝑍‘(𝑘f𝑥)) = (𝑍‘(𝑘f𝑥)))
3121, 24, 27, 27, 28, 29, 30ofval 7429 . . . . . . . . . . 11 ((((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) ∧ (𝑘f𝑥) ∈ 𝐷) → ((𝑌f (+g𝑅)𝑍)‘(𝑘f𝑥)) = ((𝑌‘(𝑘f𝑥))(+g𝑅)(𝑍‘(𝑘f𝑥))))
3217, 31mpdan 687 . . . . . . . . . 10 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑌f (+g𝑅)𝑍)‘(𝑘f𝑥)) = ((𝑌‘(𝑘f𝑥))(+g𝑅)(𝑍‘(𝑘f𝑥))))
339, 32eqtrd 2773 . . . . . . . . 9 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑌 + 𝑍)‘(𝑘f𝑥)) = ((𝑌‘(𝑘f𝑥))(+g𝑅)(𝑍‘(𝑘f𝑥))))
3433oveq2d 7180 . . . . . . . 8 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑋𝑥)(.r𝑅)((𝑌 + 𝑍)‘(𝑘f𝑥))) = ((𝑋𝑥)(.r𝑅)((𝑌‘(𝑘f𝑥))(+g𝑅)(𝑍‘(𝑘f𝑥)))))
35 psrring.r . . . . . . . . . 10 (𝜑𝑅 ∈ Ring)
3635ad2antrr 726 . . . . . . . . 9 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑅 ∈ Ring)
37 psrass.x . . . . . . . . . . . 12 (𝜑𝑋𝐵)
381, 18, 13, 2, 37psrelbas 20751 . . . . . . . . . . 11 (𝜑𝑋:𝐷⟶(Base‘𝑅))
3938ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑋:𝐷⟶(Base‘𝑅))
4010, 12sseldi 3873 . . . . . . . . . 10 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑥𝐷)
4139, 40ffvelrnd 6856 . . . . . . . . 9 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑋𝑥) ∈ (Base‘𝑅))
4220, 17ffvelrnd 6856 . . . . . . . . 9 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑌‘(𝑘f𝑥)) ∈ (Base‘𝑅))
4323, 17ffvelrnd 6856 . . . . . . . . 9 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑍‘(𝑘f𝑥)) ∈ (Base‘𝑅))
44 eqid 2738 . . . . . . . . . 10 (.r𝑅) = (.r𝑅)
4518, 3, 44ringdi 19431 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ ((𝑋𝑥) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘f𝑥)) ∈ (Base‘𝑅) ∧ (𝑍‘(𝑘f𝑥)) ∈ (Base‘𝑅))) → ((𝑋𝑥)(.r𝑅)((𝑌‘(𝑘f𝑥))(+g𝑅)(𝑍‘(𝑘f𝑥)))) = (((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))(+g𝑅)((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥)))))
4636, 41, 42, 43, 45syl13anc 1373 . . . . . . . 8 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑋𝑥)(.r𝑅)((𝑌‘(𝑘f𝑥))(+g𝑅)(𝑍‘(𝑘f𝑥)))) = (((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))(+g𝑅)((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥)))))
4734, 46eqtrd 2773 . . . . . . 7 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑋𝑥)(.r𝑅)((𝑌 + 𝑍)‘(𝑘f𝑥))) = (((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))(+g𝑅)((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥)))))
4847mpteq2dva 5122 . . . . . 6 ((𝜑𝑘𝐷) → (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)((𝑌 + 𝑍)‘(𝑘f𝑥)))) = (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ (((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))(+g𝑅)((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥))))))
4913psrbaglefi 20738 . . . . . . . 8 (𝑘𝐷 → {𝑦𝐷𝑦r𝑘} ∈ Fin)
5049adantl 485 . . . . . . 7 ((𝜑𝑘𝐷) → {𝑦𝐷𝑦r𝑘} ∈ Fin)
5118, 44ringcl 19426 . . . . . . . 8 ((𝑅 ∈ Ring ∧ (𝑋𝑥) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘f𝑥)) ∈ (Base‘𝑅)) → ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥))) ∈ (Base‘𝑅))
5236, 41, 42, 51syl3anc 1372 . . . . . . 7 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥))) ∈ (Base‘𝑅))
5318, 44ringcl 19426 . . . . . . . 8 ((𝑅 ∈ Ring ∧ (𝑋𝑥) ∈ (Base‘𝑅) ∧ (𝑍‘(𝑘f𝑥)) ∈ (Base‘𝑅)) → ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥))) ∈ (Base‘𝑅))
5436, 41, 43, 53syl3anc 1372 . . . . . . 7 (((𝜑𝑘𝐷) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥))) ∈ (Base‘𝑅))
55 eqidd 2739 . . . . . . 7 ((𝜑𝑘𝐷) → (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))) = (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))))
56 eqidd 2739 . . . . . . 7 ((𝜑𝑘𝐷) → (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥)))) = (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥)))))
5750, 52, 54, 55, 56offval2 7438 . . . . . 6 ((𝜑𝑘𝐷) → ((𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))) ∘f (+g𝑅)(𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥))))) = (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ (((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))(+g𝑅)((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥))))))
5848, 57eqtr4d 2776 . . . . 5 ((𝜑𝑘𝐷) → (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)((𝑌 + 𝑍)‘(𝑘f𝑥)))) = ((𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))) ∘f (+g𝑅)(𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥))))))
5958oveq2d 7180 . . . 4 ((𝜑𝑘𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)((𝑌 + 𝑍)‘(𝑘f𝑥))))) = (𝑅 Σg ((𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))) ∘f (+g𝑅)(𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥)))))))
6035adantr 484 . . . . . 6 ((𝜑𝑘𝐷) → 𝑅 ∈ Ring)
61 ringcmn 19446 . . . . . 6 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
6260, 61syl 17 . . . . 5 ((𝜑𝑘𝐷) → 𝑅 ∈ CMnd)
63 eqid 2738 . . . . 5 (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))) = (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥))))
64 eqid 2738 . . . . 5 (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥)))) = (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥))))
6518, 3, 62, 50, 52, 54, 63, 64gsummptfidmadd2 19158 . . . 4 ((𝜑𝑘𝐷) → (𝑅 Σg ((𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))) ∘f (+g𝑅)(𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥)))))) = ((𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))))(+g𝑅)(𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥)))))))
6659, 65eqtrd 2773 . . 3 ((𝜑𝑘𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)((𝑌 + 𝑍)‘(𝑘f𝑥))))) = ((𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))))(+g𝑅)(𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥)))))))
6766mpteq2dva 5122 . 2 (𝜑 → (𝑘𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)((𝑌 + 𝑍)‘(𝑘f𝑥)))))) = (𝑘𝐷 ↦ ((𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))))(+g𝑅)(𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥))))))))
68 psrass.t . . 3 × = (.r𝑆)
69 ringgrp 19414 . . . . 5 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
7035, 69syl 17 . . . 4 (𝜑𝑅 ∈ Grp)
711, 2, 4, 70, 5, 6psraddcl 20755 . . 3 (𝜑 → (𝑌 + 𝑍) ∈ 𝐵)
721, 2, 44, 68, 13, 37, 71psrmulfval 20757 . 2 (𝜑 → (𝑋 × (𝑌 + 𝑍)) = (𝑘𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)((𝑌 + 𝑍)‘(𝑘f𝑥)))))))
731, 2, 68, 35, 37, 5psrmulcl 20760 . . . 4 (𝜑 → (𝑋 × 𝑌) ∈ 𝐵)
741, 2, 68, 35, 37, 6psrmulcl 20760 . . . 4 (𝜑 → (𝑋 × 𝑍) ∈ 𝐵)
751, 2, 3, 4, 73, 74psradd 20754 . . 3 (𝜑 → ((𝑋 × 𝑌) + (𝑋 × 𝑍)) = ((𝑋 × 𝑌) ∘f (+g𝑅)(𝑋 × 𝑍)))
7626a1i 11 . . . 4 (𝜑𝐷 ∈ V)
77 ovexd 7199 . . . 4 ((𝜑𝑘𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥))))) ∈ V)
78 ovexd 7199 . . . 4 ((𝜑𝑘𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥))))) ∈ V)
791, 2, 44, 68, 13, 37, 5psrmulfval 20757 . . . 4 (𝜑 → (𝑋 × 𝑌) = (𝑘𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))))))
801, 2, 44, 68, 13, 37, 6psrmulfval 20757 . . . 4 (𝜑 → (𝑋 × 𝑍) = (𝑘𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥)))))))
8176, 77, 78, 79, 80offval2 7438 . . 3 (𝜑 → ((𝑋 × 𝑌) ∘f (+g𝑅)(𝑋 × 𝑍)) = (𝑘𝐷 ↦ ((𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))))(+g𝑅)(𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥))))))))
8275, 81eqtrd 2773 . 2 (𝜑 → ((𝑋 × 𝑌) + (𝑋 × 𝑍)) = (𝑘𝐷 ↦ ((𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑌‘(𝑘f𝑥)))))(+g𝑅)(𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥)(.r𝑅)(𝑍‘(𝑘f𝑥))))))))
8367, 72, 823eqtr4d 2783 1 (𝜑 → (𝑋 × (𝑌 + 𝑍)) = ((𝑋 × 𝑌) + (𝑋 × 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1542  wcel 2113  {crab 3057  Vcvv 3397   class class class wbr 5027  cmpt 5107  ccnv 5518  cima 5522  wf 6329  cfv 6333  (class class class)co 7164  f cof 7417  r cofr 7418  m cmap 8430  Fincfn 8548  cle 10747  cmin 10941  cn 11709  0cn0 11969  Basecbs 16579  +gcplusg 16661  .rcmulr 16662   Σg cgsu 16810  Grpcgrp 18212  CMndccmn 19017  Ringcrg 19409   mPwSer cmps 20710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-cnex 10664  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684  ax-pre-mulgt0 10685
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-isom 6342  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-of 7419  df-ofr 7420  df-om 7594  df-1st 7707  df-2nd 7708  df-supp 7850  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-1o 8124  df-er 8313  df-map 8432  df-pm 8433  df-ixp 8501  df-en 8549  df-dom 8550  df-sdom 8551  df-fin 8552  df-fsupp 8900  df-oi 9040  df-card 9434  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752  df-sub 10943  df-neg 10944  df-nn 11710  df-2 11772  df-3 11773  df-4 11774  df-5 11775  df-6 11776  df-7 11777  df-8 11778  df-9 11779  df-n0 11970  df-z 12056  df-uz 12318  df-fz 12975  df-fzo 13118  df-seq 13454  df-hash 13776  df-struct 16581  df-ndx 16582  df-slot 16583  df-base 16585  df-sets 16586  df-ress 16587  df-plusg 16674  df-mulr 16675  df-sca 16677  df-vsca 16678  df-tset 16680  df-0g 16811  df-gsum 16812  df-mgm 17961  df-sgrp 18010  df-mnd 18021  df-submnd 18066  df-grp 18215  df-minusg 18216  df-cntz 18558  df-cmn 19019  df-abl 19020  df-mgp 19352  df-ur 19364  df-ring 19411  df-psr 20715
This theorem is referenced by:  psrring  20783
  Copyright terms: Public domain W3C validator