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

Theorem psrcom 20683
 Description: Commutative law for the ring of power series. (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 (𝜑𝑌𝐵)
psrcom.c (𝜑𝑅 ∈ CRing)
Assertion
Ref Expression
psrcom (𝜑 → (𝑋 × 𝑌) = (𝑌 × 𝑋))
Distinct variable groups:   𝑓,𝐼   𝑅,𝑓   𝑓,𝑋   𝑓,𝑌
Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑓)   𝐷(𝑓)   𝑆(𝑓)   × (𝑓)   𝑉(𝑓)

Proof of Theorem psrcom
Dummy variables 𝑥 𝑘 𝑧 𝑔 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2798 . . . . 5 (Base‘𝑅) = (Base‘𝑅)
2 eqid 2798 . . . . 5 (0g𝑅) = (0g𝑅)
3 psrring.r . . . . . . 7 (𝜑𝑅 ∈ Ring)
4 ringcmn 19348 . . . . . . 7 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
53, 4syl 17 . . . . . 6 (𝜑𝑅 ∈ CMnd)
65adantr 484 . . . . 5 ((𝜑𝑥𝐷) → 𝑅 ∈ CMnd)
7 psrass.d . . . . . . 7 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
87psrbaglefi 20640 . . . . . 6 (𝑥𝐷 → {𝑔𝐷𝑔r𝑥} ∈ Fin)
98adantl 485 . . . . 5 ((𝜑𝑥𝐷) → {𝑔𝐷𝑔r𝑥} ∈ Fin)
103ad2antrr 725 . . . . . . 7 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑅 ∈ Ring)
11 psrring.s . . . . . . . . . 10 𝑆 = (𝐼 mPwSer 𝑅)
12 psrass.b . . . . . . . . . 10 𝐵 = (Base‘𝑆)
13 psrass.x . . . . . . . . . 10 (𝜑𝑋𝐵)
1411, 1, 7, 12, 13psrelbas 20653 . . . . . . . . 9 (𝜑𝑋:𝐷⟶(Base‘𝑅))
1514ad2antrr 725 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑋:𝐷⟶(Base‘𝑅))
16 simpr 488 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑘 ∈ {𝑔𝐷𝑔r𝑥})
17 breq1 5037 . . . . . . . . . . 11 (𝑔 = 𝑘 → (𝑔r𝑥𝑘r𝑥))
1817elrab 3630 . . . . . . . . . 10 (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↔ (𝑘𝐷𝑘r𝑥))
1916, 18sylib 221 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑘𝐷𝑘r𝑥))
2019simpld 498 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑘𝐷)
2115, 20ffvelrnd 6839 . . . . . . 7 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑋𝑘) ∈ (Base‘𝑅))
22 psrass.y . . . . . . . . . 10 (𝜑𝑌𝐵)
2311, 1, 7, 12, 22psrelbas 20653 . . . . . . . . 9 (𝜑𝑌:𝐷⟶(Base‘𝑅))
2423ad2antrr 725 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑌:𝐷⟶(Base‘𝑅))
25 simplr 768 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑥𝐷)
267psrbagf 20626 . . . . . . . . . . 11 (𝑘𝐷𝑘:𝐼⟶ℕ0)
2720, 26syl 17 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑘:𝐼⟶ℕ0)
2819simprd 499 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑘r𝑥)
297psrbagcon 20638 . . . . . . . . . 10 ((𝑥𝐷𝑘:𝐼⟶ℕ0𝑘r𝑥) → ((𝑥f𝑘) ∈ 𝐷 ∧ (𝑥f𝑘) ∘r𝑥))
3025, 27, 28, 29syl3anc 1368 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑥f𝑘) ∈ 𝐷 ∧ (𝑥f𝑘) ∘r𝑥))
3130simpld 498 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑥f𝑘) ∈ 𝐷)
3224, 31ffvelrnd 6839 . . . . . . 7 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑌‘(𝑥f𝑘)) ∈ (Base‘𝑅))
33 eqid 2798 . . . . . . . 8 (.r𝑅) = (.r𝑅)
341, 33ringcl 19328 . . . . . . 7 ((𝑅 ∈ Ring ∧ (𝑋𝑘) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑥f𝑘)) ∈ (Base‘𝑅)) → ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘))) ∈ (Base‘𝑅))
3510, 21, 32, 34syl3anc 1368 . . . . . 6 (((𝜑𝑥𝐷) ∧ 𝑘 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘))) ∈ (Base‘𝑅))
3635fmpttd 6866 . . . . 5 ((𝜑𝑥𝐷) → (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))):{𝑔𝐷𝑔r𝑥}⟶(Base‘𝑅))
37 ovex 7178 . . . . . . . . . 10 (ℕ0m 𝐼) ∈ V
387, 37rabex2 5205 . . . . . . . . 9 𝐷 ∈ V
3938a1i 11 . . . . . . . 8 ((𝜑𝑥𝐷) → 𝐷 ∈ V)
40 rabexg 5202 . . . . . . . 8 (𝐷 ∈ V → {𝑔𝐷𝑔r𝑥} ∈ V)
4139, 40syl 17 . . . . . . 7 ((𝜑𝑥𝐷) → {𝑔𝐷𝑔r𝑥} ∈ V)
4241mptexd 6974 . . . . . 6 ((𝜑𝑥𝐷) → (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) ∈ V)
43 funmpt 6370 . . . . . . 7 Fun (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘))))
4443a1i 11 . . . . . 6 ((𝜑𝑥𝐷) → Fun (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))))
45 fvexd 6670 . . . . . 6 ((𝜑𝑥𝐷) → (0g𝑅) ∈ V)
46 suppssdm 7842 . . . . . . . 8 ((𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) supp (0g𝑅)) ⊆ dom (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘))))
47 eqid 2798 . . . . . . . . 9 (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) = (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘))))
4847dmmptss 6067 . . . . . . . 8 dom (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) ⊆ {𝑔𝐷𝑔r𝑥}
4946, 48sstri 3926 . . . . . . 7 ((𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) supp (0g𝑅)) ⊆ {𝑔𝐷𝑔r𝑥}
5049a1i 11 . . . . . 6 ((𝜑𝑥𝐷) → ((𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) supp (0g𝑅)) ⊆ {𝑔𝐷𝑔r𝑥})
51 suppssfifsupp 8850 . . . . . 6 ((((𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) ∈ V ∧ Fun (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) ∧ (0g𝑅) ∈ V) ∧ ({𝑔𝐷𝑔r𝑥} ∈ Fin ∧ ((𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) supp (0g𝑅)) ⊆ {𝑔𝐷𝑔r𝑥})) → (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) finSupp (0g𝑅))
5242, 44, 45, 9, 50, 51syl32anc 1375 . . . . 5 ((𝜑𝑥𝐷) → (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) finSupp (0g𝑅))
53 eqid 2798 . . . . . . 7 {𝑔𝐷𝑔r𝑥} = {𝑔𝐷𝑔r𝑥}
547, 53psrbagconf1o 20644 . . . . . 6 (𝑥𝐷 → (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑥f𝑗)):{𝑔𝐷𝑔r𝑥}–1-1-onto→{𝑔𝐷𝑔r𝑥})
5554adantl 485 . . . . 5 ((𝜑𝑥𝐷) → (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑥f𝑗)):{𝑔𝐷𝑔r𝑥}–1-1-onto→{𝑔𝐷𝑔r𝑥})
561, 2, 6, 9, 36, 52, 55gsumf1o 19050 . . . 4 ((𝜑𝑥𝐷) → (𝑅 Σg (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘))))) = (𝑅 Σg ((𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) ∘ (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑥f𝑗)))))
57 simplr 768 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑥𝐷)
58 simpr 488 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑗 ∈ {𝑔𝐷𝑔r𝑥})
597, 53psrbagconcl 20642 . . . . . . . 8 ((𝑥𝐷𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑥f𝑗) ∈ {𝑔𝐷𝑔r𝑥})
6057, 58, 59syl2anc 587 . . . . . . 7 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑥f𝑗) ∈ {𝑔𝐷𝑔r𝑥})
61 eqidd 2799 . . . . . . 7 ((𝜑𝑥𝐷) → (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑥f𝑗)) = (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑥f𝑗)))
62 eqidd 2799 . . . . . . 7 ((𝜑𝑥𝐷) → (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) = (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))))
63 fveq2 6655 . . . . . . . 8 (𝑘 = (𝑥f𝑗) → (𝑋𝑘) = (𝑋‘(𝑥f𝑗)))
64 oveq2 7153 . . . . . . . . 9 (𝑘 = (𝑥f𝑗) → (𝑥f𝑘) = (𝑥f − (𝑥f𝑗)))
6564fveq2d 6659 . . . . . . . 8 (𝑘 = (𝑥f𝑗) → (𝑌‘(𝑥f𝑘)) = (𝑌‘(𝑥f − (𝑥f𝑗))))
6663, 65oveq12d 7163 . . . . . . 7 (𝑘 = (𝑥f𝑗) → ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘))) = ((𝑋‘(𝑥f𝑗))(.r𝑅)(𝑌‘(𝑥f − (𝑥f𝑗)))))
6760, 61, 62, 66fmptco 6878 . . . . . 6 ((𝜑𝑥𝐷) → ((𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) ∘ (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑥f𝑗))) = (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋‘(𝑥f𝑗))(.r𝑅)(𝑌‘(𝑥f − (𝑥f𝑗))))))
687psrbagf 20626 . . . . . . . . . . . . . . . 16 (𝑥𝐷𝑥:𝐼⟶ℕ0)
6968adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐷) → 𝑥:𝐼⟶ℕ0)
7069adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑥:𝐼⟶ℕ0)
7170ffvelrnda 6838 . . . . . . . . . . . . 13 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑧𝐼) → (𝑥𝑧) ∈ ℕ0)
72 breq1 5037 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑗 → (𝑔r𝑥𝑗r𝑥))
7372elrab 3630 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↔ (𝑗𝐷𝑗r𝑥))
7458, 73sylib 221 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑗𝐷𝑗r𝑥))
7574simpld 498 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑗𝐷)
767psrbagf 20626 . . . . . . . . . . . . . . 15 (𝑗𝐷𝑗:𝐼⟶ℕ0)
7775, 76syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑗:𝐼⟶ℕ0)
7877ffvelrnda 6838 . . . . . . . . . . . . 13 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑧𝐼) → (𝑗𝑧) ∈ ℕ0)
79 nn0cn 11913 . . . . . . . . . . . . . 14 ((𝑥𝑧) ∈ ℕ0 → (𝑥𝑧) ∈ ℂ)
80 nn0cn 11913 . . . . . . . . . . . . . 14 ((𝑗𝑧) ∈ ℕ0 → (𝑗𝑧) ∈ ℂ)
81 nncan 10922 . . . . . . . . . . . . . 14 (((𝑥𝑧) ∈ ℂ ∧ (𝑗𝑧) ∈ ℂ) → ((𝑥𝑧) − ((𝑥𝑧) − (𝑗𝑧))) = (𝑗𝑧))
8279, 80, 81syl2an 598 . . . . . . . . . . . . 13 (((𝑥𝑧) ∈ ℕ0 ∧ (𝑗𝑧) ∈ ℕ0) → ((𝑥𝑧) − ((𝑥𝑧) − (𝑗𝑧))) = (𝑗𝑧))
8371, 78, 82syl2anc 587 . . . . . . . . . . . 12 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑧𝐼) → ((𝑥𝑧) − ((𝑥𝑧) − (𝑗𝑧))) = (𝑗𝑧))
8483mpteq2dva 5129 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑧𝐼 ↦ ((𝑥𝑧) − ((𝑥𝑧) − (𝑗𝑧)))) = (𝑧𝐼 ↦ (𝑗𝑧)))
85 psrring.i . . . . . . . . . . . . 13 (𝜑𝐼𝑉)
8685ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝐼𝑉)
87 ovex 7178 . . . . . . . . . . . . 13 ((𝑥𝑧) − (𝑗𝑧)) ∈ V
8887a1i 11 . . . . . . . . . . . 12 ((((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) ∧ 𝑧𝐼) → ((𝑥𝑧) − (𝑗𝑧)) ∈ V)
8970feqmptd 6718 . . . . . . . . . . . 12 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑥 = (𝑧𝐼 ↦ (𝑥𝑧)))
9077feqmptd 6718 . . . . . . . . . . . . 13 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑗 = (𝑧𝐼 ↦ (𝑗𝑧)))
9186, 71, 78, 89, 90offval2 7419 . . . . . . . . . . . 12 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑥f𝑗) = (𝑧𝐼 ↦ ((𝑥𝑧) − (𝑗𝑧))))
9286, 71, 88, 89, 91offval2 7419 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑥f − (𝑥f𝑗)) = (𝑧𝐼 ↦ ((𝑥𝑧) − ((𝑥𝑧) − (𝑗𝑧)))))
9384, 92, 903eqtr4d 2843 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑥f − (𝑥f𝑗)) = 𝑗)
9493fveq2d 6659 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑌‘(𝑥f − (𝑥f𝑗))) = (𝑌𝑗))
9594oveq2d 7161 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑋‘(𝑥f𝑗))(.r𝑅)(𝑌‘(𝑥f − (𝑥f𝑗)))) = ((𝑋‘(𝑥f𝑗))(.r𝑅)(𝑌𝑗)))
96 psrcom.c . . . . . . . . . 10 (𝜑𝑅 ∈ CRing)
9796ad2antrr 725 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑅 ∈ CRing)
9814ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑋:𝐷⟶(Base‘𝑅))
9974simprd 499 . . . . . . . . . . . 12 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑗r𝑥)
1007psrbagcon 20638 . . . . . . . . . . . 12 ((𝑥𝐷𝑗:𝐼⟶ℕ0𝑗r𝑥) → ((𝑥f𝑗) ∈ 𝐷 ∧ (𝑥f𝑗) ∘r𝑥))
10157, 77, 99, 100syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑥f𝑗) ∈ 𝐷 ∧ (𝑥f𝑗) ∘r𝑥))
102101simpld 498 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑥f𝑗) ∈ 𝐷)
10398, 102ffvelrnd 6839 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑋‘(𝑥f𝑗)) ∈ (Base‘𝑅))
10423ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → 𝑌:𝐷⟶(Base‘𝑅))
105104, 75ffvelrnd 6839 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → (𝑌𝑗) ∈ (Base‘𝑅))
1061, 33crngcom 19329 . . . . . . . . 9 ((𝑅 ∈ CRing ∧ (𝑋‘(𝑥f𝑗)) ∈ (Base‘𝑅) ∧ (𝑌𝑗) ∈ (Base‘𝑅)) → ((𝑋‘(𝑥f𝑗))(.r𝑅)(𝑌𝑗)) = ((𝑌𝑗)(.r𝑅)(𝑋‘(𝑥f𝑗))))
10797, 103, 105, 106syl3anc 1368 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑋‘(𝑥f𝑗))(.r𝑅)(𝑌𝑗)) = ((𝑌𝑗)(.r𝑅)(𝑋‘(𝑥f𝑗))))
10895, 107eqtrd 2833 . . . . . . 7 (((𝜑𝑥𝐷) ∧ 𝑗 ∈ {𝑔𝐷𝑔r𝑥}) → ((𝑋‘(𝑥f𝑗))(.r𝑅)(𝑌‘(𝑥f − (𝑥f𝑗)))) = ((𝑌𝑗)(.r𝑅)(𝑋‘(𝑥f𝑗))))
109108mpteq2dva 5129 . . . . . 6 ((𝜑𝑥𝐷) → (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋‘(𝑥f𝑗))(.r𝑅)(𝑌‘(𝑥f − (𝑥f𝑗))))) = (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑌𝑗)(.r𝑅)(𝑋‘(𝑥f𝑗)))))
11067, 109eqtrd 2833 . . . . 5 ((𝜑𝑥𝐷) → ((𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) ∘ (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑥f𝑗))) = (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑌𝑗)(.r𝑅)(𝑋‘(𝑥f𝑗)))))
111110oveq2d 7161 . . . 4 ((𝜑𝑥𝐷) → (𝑅 Σg ((𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))) ∘ (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ (𝑥f𝑗)))) = (𝑅 Σg (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑌𝑗)(.r𝑅)(𝑋‘(𝑥f𝑗))))))
11256, 111eqtrd 2833 . . 3 ((𝜑𝑥𝐷) → (𝑅 Σg (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘))))) = (𝑅 Σg (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑌𝑗)(.r𝑅)(𝑋‘(𝑥f𝑗))))))
113112mpteq2dva 5129 . 2 (𝜑 → (𝑥𝐷 ↦ (𝑅 Σg (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))))) = (𝑥𝐷 ↦ (𝑅 Σg (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑌𝑗)(.r𝑅)(𝑋‘(𝑥f𝑗)))))))
114 psrass.t . . 3 × = (.r𝑆)
11511, 12, 33, 114, 7, 13, 22psrmulfval 20659 . 2 (𝜑 → (𝑋 × 𝑌) = (𝑥𝐷 ↦ (𝑅 Σg (𝑘 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑋𝑘)(.r𝑅)(𝑌‘(𝑥f𝑘)))))))
11611, 12, 33, 114, 7, 22, 13psrmulfval 20659 . 2 (𝜑 → (𝑌 × 𝑋) = (𝑥𝐷 ↦ (𝑅 Σg (𝑗 ∈ {𝑔𝐷𝑔r𝑥} ↦ ((𝑌𝑗)(.r𝑅)(𝑋‘(𝑥f𝑗)))))))
117113, 115, 1163eqtr4d 2843 1 (𝜑 → (𝑋 × 𝑌) = (𝑌 × 𝑋))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {crab 3110  Vcvv 3442   ⊆ wss 3883   class class class wbr 5034   ↦ cmpt 5114  ◡ccnv 5522  dom cdm 5523   “ cima 5526   ∘ ccom 5527  Fun wfun 6326  ⟶wf 6328  –1-1-onto→wf1o 6331  ‘cfv 6332  (class class class)co 7145   ∘f cof 7398   ∘r cofr 7399   supp csupp 7826   ↑m cmap 8407  Fincfn 8510   finSupp cfsupp 8835  ℂcc 10542   ≤ cle 10683   − cmin 10877  ℕcn 11643  ℕ0cn0 11903  Basecbs 16495  .rcmulr 16578  0gc0g 16725   Σg cgsu 16726  CMndccmn 18919  Ringcrg 19311  CRingccrg 19312   mPwSer cmps 20612 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-cnex 10600  ax-resscn 10601  ax-1cn 10602  ax-icn 10603  ax-addcl 10604  ax-addrcl 10605  ax-mulcl 10606  ax-mulrcl 10607  ax-mulcom 10608  ax-addass 10609  ax-mulass 10610  ax-distr 10611  ax-i2m1 10612  ax-1ne0 10613  ax-1rid 10614  ax-rnegex 10615  ax-rrecex 10616  ax-cnre 10617  ax-pre-lttri 10618  ax-pre-lttrn 10619  ax-pre-ltadd 10620  ax-pre-mulgt0 10621 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 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-isom 6341  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7400  df-ofr 7401  df-om 7574  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-2o 8104  df-oadd 8107  df-er 8290  df-map 8409  df-pm 8410  df-ixp 8463  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-fsupp 8836  df-oi 8976  df-card 9370  df-pnf 10684  df-mnf 10685  df-xr 10686  df-ltxr 10687  df-le 10688  df-sub 10879  df-neg 10880  df-nn 11644  df-2 11706  df-3 11707  df-4 11708  df-5 11709  df-6 11710  df-7 11711  df-8 11712  df-9 11713  df-n0 11904  df-z 11990  df-uz 12252  df-fz 12906  df-fzo 13049  df-seq 13385  df-hash 13707  df-struct 16497  df-ndx 16498  df-slot 16499  df-base 16501  df-sets 16502  df-plusg 16590  df-mulr 16591  df-sca 16593  df-vsca 16594  df-tset 16596  df-0g 16727  df-gsum 16728  df-mgm 17864  df-sgrp 17913  df-mnd 17924  df-grp 18118  df-minusg 18119  df-cntz 18460  df-cmn 18921  df-abl 18922  df-mgp 19254  df-ur 19266  df-ring 19313  df-cring 19314  df-psr 20617 This theorem is referenced by:  psrcrng  20687
 Copyright terms: Public domain W3C validator