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

Theorem psrlidm 20674
 Description: The identity element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by AV, 8-Jul-2019.)
Hypotheses
Ref Expression
psrring.s 𝑆 = (𝐼 mPwSer 𝑅)
psrring.i (𝜑𝐼𝑉)
psrring.r (𝜑𝑅 ∈ Ring)
psr1cl.d 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
psr1cl.z 0 = (0g𝑅)
psr1cl.o 1 = (1r𝑅)
psr1cl.u 𝑈 = (𝑥𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))
psr1cl.b 𝐵 = (Base‘𝑆)
psrlidm.t · = (.r𝑆)
psrlidm.x (𝜑𝑋𝐵)
Assertion
Ref Expression
psrlidm (𝜑 → (𝑈 · 𝑋) = 𝑋)
Distinct variable groups:   𝑥,𝑓, 0   𝑓,𝐼,𝑥   𝑥,𝐵   𝑅,𝑓,𝑥   𝑥,𝐷   𝑓,𝑋,𝑥   𝜑,𝑥   𝑥,𝑉   𝑥, ·   𝑥,𝑆   𝑥, 1
Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑓)   𝐷(𝑓)   𝑆(𝑓)   · (𝑓)   𝑈(𝑥,𝑓)   1 (𝑓)   𝑉(𝑓)

Proof of Theorem psrlidm
Dummy variables 𝑦 𝑧 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 psrring.s . . . 4 𝑆 = (𝐼 mPwSer 𝑅)
2 eqid 2798 . . . 4 (Base‘𝑅) = (Base‘𝑅)
3 psr1cl.d . . . 4 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
4 psr1cl.b . . . 4 𝐵 = (Base‘𝑆)
5 psrlidm.t . . . . 5 · = (.r𝑆)
6 psrring.r . . . . 5 (𝜑𝑅 ∈ Ring)
7 psrring.i . . . . . 6 (𝜑𝐼𝑉)
8 psr1cl.z . . . . . 6 0 = (0g𝑅)
9 psr1cl.o . . . . . 6 1 = (1r𝑅)
10 psr1cl.u . . . . . 6 𝑈 = (𝑥𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))
111, 7, 6, 3, 8, 9, 10, 4psr1cl 20673 . . . . 5 (𝜑𝑈𝐵)
12 psrlidm.x . . . . 5 (𝜑𝑋𝐵)
131, 4, 5, 6, 11, 12psrmulcl 20659 . . . 4 (𝜑 → (𝑈 · 𝑋) ∈ 𝐵)
141, 2, 3, 4, 13psrelbas 20650 . . 3 (𝜑 → (𝑈 · 𝑋):𝐷⟶(Base‘𝑅))
1514ffnd 6493 . 2 (𝜑 → (𝑈 · 𝑋) Fn 𝐷)
161, 2, 3, 4, 12psrelbas 20650 . . 3 (𝜑𝑋:𝐷⟶(Base‘𝑅))
1716ffnd 6493 . 2 (𝜑𝑋 Fn 𝐷)
18 eqid 2798 . . . 4 (.r𝑅) = (.r𝑅)
1911adantr 484 . . . 4 ((𝜑𝑦𝐷) → 𝑈𝐵)
2012adantr 484 . . . 4 ((𝜑𝑦𝐷) → 𝑋𝐵)
21 simpr 488 . . . 4 ((𝜑𝑦𝐷) → 𝑦𝐷)
221, 4, 18, 5, 3, 19, 20, 21psrmulval 20657 . . 3 ((𝜑𝑦𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑅 Σg (𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧))))))
23 breq1 5036 . . . . . . . 8 (𝑔 = (𝐼 × {0}) → (𝑔r𝑦 ↔ (𝐼 × {0}) ∘r𝑦))
24 fconstmpt 5581 . . . . . . . . . 10 (𝐼 × {0}) = (𝑥𝐼 ↦ 0)
253fczpsrbag 20628 . . . . . . . . . . 11 (𝐼𝑉 → (𝑥𝐼 ↦ 0) ∈ 𝐷)
267, 25syl 17 . . . . . . . . . 10 (𝜑 → (𝑥𝐼 ↦ 0) ∈ 𝐷)
2724, 26eqeltrid 2894 . . . . . . . . 9 (𝜑 → (𝐼 × {0}) ∈ 𝐷)
2827adantr 484 . . . . . . . 8 ((𝜑𝑦𝐷) → (𝐼 × {0}) ∈ 𝐷)
293psrbagf 20623 . . . . . . . . . . . . 13 (𝑦𝐷𝑦:𝐼⟶ℕ0)
3029adantl 485 . . . . . . . . . . . 12 ((𝜑𝑦𝐷) → 𝑦:𝐼⟶ℕ0)
3130ffvelrnda 6835 . . . . . . . . . . 11 (((𝜑𝑦𝐷) ∧ 𝑥𝐼) → (𝑦𝑥) ∈ ℕ0)
3231nn0ge0d 11963 . . . . . . . . . 10 (((𝜑𝑦𝐷) ∧ 𝑥𝐼) → 0 ≤ (𝑦𝑥))
3332ralrimiva 3149 . . . . . . . . 9 ((𝜑𝑦𝐷) → ∀𝑥𝐼 0 ≤ (𝑦𝑥))
34 0nn0 11915 . . . . . . . . . . . 12 0 ∈ ℕ0
3534fconst6 6548 . . . . . . . . . . 11 (𝐼 × {0}):𝐼⟶ℕ0
36 ffn 6492 . . . . . . . . . . 11 ((𝐼 × {0}):𝐼⟶ℕ0 → (𝐼 × {0}) Fn 𝐼)
3735, 36mp1i 13 . . . . . . . . . 10 ((𝜑𝑦𝐷) → (𝐼 × {0}) Fn 𝐼)
3830ffnd 6493 . . . . . . . . . 10 ((𝜑𝑦𝐷) → 𝑦 Fn 𝐼)
397adantr 484 . . . . . . . . . 10 ((𝜑𝑦𝐷) → 𝐼𝑉)
40 inidm 4147 . . . . . . . . . 10 (𝐼𝐼) = 𝐼
4134a1i 11 . . . . . . . . . . 11 ((𝜑𝑦𝐷) → 0 ∈ ℕ0)
42 fvconst2g 6948 . . . . . . . . . . 11 ((0 ∈ ℕ0𝑥𝐼) → ((𝐼 × {0})‘𝑥) = 0)
4341, 42sylan 583 . . . . . . . . . 10 (((𝜑𝑦𝐷) ∧ 𝑥𝐼) → ((𝐼 × {0})‘𝑥) = 0)
44 eqidd 2799 . . . . . . . . . 10 (((𝜑𝑦𝐷) ∧ 𝑥𝐼) → (𝑦𝑥) = (𝑦𝑥))
4537, 38, 39, 39, 40, 43, 44ofrfval 7406 . . . . . . . . 9 ((𝜑𝑦𝐷) → ((𝐼 × {0}) ∘r𝑦 ↔ ∀𝑥𝐼 0 ≤ (𝑦𝑥)))
4633, 45mpbird 260 . . . . . . . 8 ((𝜑𝑦𝐷) → (𝐼 × {0}) ∘r𝑦)
4723, 28, 46elrabd 3631 . . . . . . 7 ((𝜑𝑦𝐷) → (𝐼 × {0}) ∈ {𝑔𝐷𝑔r𝑦})
4847snssd 4704 . . . . . 6 ((𝜑𝑦𝐷) → {(𝐼 × {0})} ⊆ {𝑔𝐷𝑔r𝑦})
4948resmptd 5878 . . . . 5 ((𝜑𝑦𝐷) → ((𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))) ↾ {(𝐼 × {0})}) = (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))))
5049oveq2d 7158 . . . 4 ((𝜑𝑦𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧))))))
51 ringcmn 19345 . . . . . . 7 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
526, 51syl 17 . . . . . 6 (𝜑𝑅 ∈ CMnd)
5352adantr 484 . . . . 5 ((𝜑𝑦𝐷) → 𝑅 ∈ CMnd)
54 ovex 7175 . . . . . . 7 (ℕ0m 𝐼) ∈ V
553, 54rab2ex 5205 . . . . . 6 {𝑔𝐷𝑔r𝑦} ∈ V
5655a1i 11 . . . . 5 ((𝜑𝑦𝐷) → {𝑔𝐷𝑔r𝑦} ∈ V)
576ad2antrr 725 . . . . . . 7 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → 𝑅 ∈ Ring)
58 simpr 488 . . . . . . . . . 10 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → 𝑧 ∈ {𝑔𝐷𝑔r𝑦})
59 breq1 5036 . . . . . . . . . . 11 (𝑔 = 𝑧 → (𝑔r𝑦𝑧r𝑦))
6059elrab 3629 . . . . . . . . . 10 (𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↔ (𝑧𝐷𝑧r𝑦))
6158, 60sylib 221 . . . . . . . . 9 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → (𝑧𝐷𝑧r𝑦))
6261simpld 498 . . . . . . . 8 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → 𝑧𝐷)
631, 2, 3, 4, 19psrelbas 20650 . . . . . . . . 9 ((𝜑𝑦𝐷) → 𝑈:𝐷⟶(Base‘𝑅))
6463ffvelrnda 6835 . . . . . . . 8 (((𝜑𝑦𝐷) ∧ 𝑧𝐷) → (𝑈𝑧) ∈ (Base‘𝑅))
6562, 64syldan 594 . . . . . . 7 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → (𝑈𝑧) ∈ (Base‘𝑅))
6616ad2antrr 725 . . . . . . . 8 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → 𝑋:𝐷⟶(Base‘𝑅))
6721adantr 484 . . . . . . . . . 10 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → 𝑦𝐷)
683psrbagf 20623 . . . . . . . . . . 11 (𝑧𝐷𝑧:𝐼⟶ℕ0)
6962, 68syl 17 . . . . . . . . . 10 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → 𝑧:𝐼⟶ℕ0)
7061simprd 499 . . . . . . . . . 10 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → 𝑧r𝑦)
713psrbagcon 20635 . . . . . . . . . 10 ((𝑦𝐷𝑧:𝐼⟶ℕ0𝑧r𝑦) → ((𝑦f𝑧) ∈ 𝐷 ∧ (𝑦f𝑧) ∘r𝑦))
7267, 69, 70, 71syl3anc 1368 . . . . . . . . 9 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → ((𝑦f𝑧) ∈ 𝐷 ∧ (𝑦f𝑧) ∘r𝑦))
7372simpld 498 . . . . . . . 8 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → (𝑦f𝑧) ∈ 𝐷)
7466, 73ffvelrnd 6836 . . . . . . 7 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → (𝑋‘(𝑦f𝑧)) ∈ (Base‘𝑅))
752, 18ringcl 19325 . . . . . . 7 ((𝑅 ∈ Ring ∧ (𝑈𝑧) ∈ (Base‘𝑅) ∧ (𝑋‘(𝑦f𝑧)) ∈ (Base‘𝑅)) → ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧))) ∈ (Base‘𝑅))
7657, 65, 74, 75syl3anc 1368 . . . . . 6 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ {𝑔𝐷𝑔r𝑦}) → ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧))) ∈ (Base‘𝑅))
7776fmpttd 6863 . . . . 5 ((𝜑𝑦𝐷) → (𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))):{𝑔𝐷𝑔r𝑦}⟶(Base‘𝑅))
78 eldifi 4056 . . . . . . . . . . . 12 (𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})}) → 𝑧 ∈ {𝑔𝐷𝑔r𝑦})
7978, 61sylan2 595 . . . . . . . . . . 11 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})})) → (𝑧𝐷𝑧r𝑦))
8079simpld 498 . . . . . . . . . 10 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})})) → 𝑧𝐷)
81 eqeq1 2802 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑥 = (𝐼 × {0}) ↔ 𝑧 = (𝐼 × {0})))
8281ifbid 4449 . . . . . . . . . . 11 (𝑥 = 𝑧 → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
839fvexi 6666 . . . . . . . . . . . 12 1 ∈ V
848fvexi 6666 . . . . . . . . . . . 12 0 ∈ V
8583, 84ifex 4475 . . . . . . . . . . 11 if(𝑧 = (𝐼 × {0}), 1 , 0 ) ∈ V
8682, 10, 85fvmpt 6752 . . . . . . . . . 10 (𝑧𝐷 → (𝑈𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
8780, 86syl 17 . . . . . . . . 9 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})})) → (𝑈𝑧) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
88 eldifn 4057 . . . . . . . . . . . 12 (𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})}) → ¬ 𝑧 ∈ {(𝐼 × {0})})
8988adantl 485 . . . . . . . . . . 11 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 ∈ {(𝐼 × {0})})
90 velsn 4543 . . . . . . . . . . 11 (𝑧 ∈ {(𝐼 × {0})} ↔ 𝑧 = (𝐼 × {0}))
9189, 90sylnib 331 . . . . . . . . . 10 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})})) → ¬ 𝑧 = (𝐼 × {0}))
9291iffalsed 4438 . . . . . . . . 9 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})})) → if(𝑧 = (𝐼 × {0}), 1 , 0 ) = 0 )
9387, 92eqtrd 2833 . . . . . . . 8 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})})) → (𝑈𝑧) = 0 )
9493oveq1d 7157 . . . . . . 7 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})})) → ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧))) = ( 0 (.r𝑅)(𝑋‘(𝑦f𝑧))))
956ad2antrr 725 . . . . . . . 8 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})})) → 𝑅 ∈ Ring)
9678, 74sylan2 595 . . . . . . . 8 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})})) → (𝑋‘(𝑦f𝑧)) ∈ (Base‘𝑅))
972, 18, 8ringlz 19351 . . . . . . . 8 ((𝑅 ∈ Ring ∧ (𝑋‘(𝑦f𝑧)) ∈ (Base‘𝑅)) → ( 0 (.r𝑅)(𝑋‘(𝑦f𝑧))) = 0 )
9895, 96, 97syl2anc 587 . . . . . . 7 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})})) → ( 0 (.r𝑅)(𝑋‘(𝑦f𝑧))) = 0 )
9994, 98eqtrd 2833 . . . . . 6 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ({𝑔𝐷𝑔r𝑦} ∖ {(𝐼 × {0})})) → ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧))) = 0 )
10099, 56suppss2 7862 . . . . 5 ((𝜑𝑦𝐷) → ((𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})})
1013, 54rabex2 5204 . . . . . . . 8 𝐷 ∈ V
102101mptrabex 6972 . . . . . . 7 (𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))) ∈ V
103102a1i 11 . . . . . 6 ((𝜑𝑦𝐷) → (𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))) ∈ V)
104 funmpt 6367 . . . . . . 7 Fun (𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧))))
105104a1i 11 . . . . . 6 ((𝜑𝑦𝐷) → Fun (𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))))
10684a1i 11 . . . . . 6 ((𝜑𝑦𝐷) → 0 ∈ V)
107 snfi 8592 . . . . . . 7 {(𝐼 × {0})} ∈ Fin
108107a1i 11 . . . . . 6 ((𝜑𝑦𝐷) → {(𝐼 × {0})} ∈ Fin)
109 suppssfifsupp 8847 . . . . . 6 ((((𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))) ∈ V ∧ Fun (𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))) ∧ 0 ∈ V) ∧ ({(𝐼 × {0})} ∈ Fin ∧ ((𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))) supp 0 ) ⊆ {(𝐼 × {0})})) → (𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))) finSupp 0 )
110103, 105, 106, 108, 100, 109syl32anc 1375 . . . . 5 ((𝜑𝑦𝐷) → (𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))) finSupp 0 )
1112, 8, 53, 56, 77, 100, 110gsumres 19044 . . . 4 ((𝜑𝑦𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧)))) ↾ {(𝐼 × {0})})) = (𝑅 Σg (𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧))))))
1126adantr 484 . . . . . 6 ((𝜑𝑦𝐷) → 𝑅 ∈ Ring)
113 ringmnd 19318 . . . . . 6 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
114112, 113syl 17 . . . . 5 ((𝜑𝑦𝐷) → 𝑅 ∈ Mnd)
115 iftrue 4433 . . . . . . . . . 10 (𝑥 = (𝐼 × {0}) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = 1 )
116115, 10, 83fvmpt 6752 . . . . . . . . 9 ((𝐼 × {0}) ∈ 𝐷 → (𝑈‘(𝐼 × {0})) = 1 )
11728, 116syl 17 . . . . . . . 8 ((𝜑𝑦𝐷) → (𝑈‘(𝐼 × {0})) = 1 )
118 nn0cn 11910 . . . . . . . . . . . 12 (𝑧 ∈ ℕ0𝑧 ∈ ℂ)
119118subid1d 10990 . . . . . . . . . . 11 (𝑧 ∈ ℕ0 → (𝑧 − 0) = 𝑧)
120119adantl 485 . . . . . . . . . 10 (((𝜑𝑦𝐷) ∧ 𝑧 ∈ ℕ0) → (𝑧 − 0) = 𝑧)
12139, 30, 41, 120caofid0r 7428 . . . . . . . . 9 ((𝜑𝑦𝐷) → (𝑦f − (𝐼 × {0})) = 𝑦)
122121fveq2d 6656 . . . . . . . 8 ((𝜑𝑦𝐷) → (𝑋‘(𝑦f − (𝐼 × {0}))) = (𝑋𝑦))
123117, 122oveq12d 7160 . . . . . . 7 ((𝜑𝑦𝐷) → ((𝑈‘(𝐼 × {0}))(.r𝑅)(𝑋‘(𝑦f − (𝐼 × {0})))) = ( 1 (.r𝑅)(𝑋𝑦)))
12416ffvelrnda 6835 . . . . . . . 8 ((𝜑𝑦𝐷) → (𝑋𝑦) ∈ (Base‘𝑅))
1252, 18, 9ringlidm 19335 . . . . . . . 8 ((𝑅 ∈ Ring ∧ (𝑋𝑦) ∈ (Base‘𝑅)) → ( 1 (.r𝑅)(𝑋𝑦)) = (𝑋𝑦))
126112, 124, 125syl2anc 587 . . . . . . 7 ((𝜑𝑦𝐷) → ( 1 (.r𝑅)(𝑋𝑦)) = (𝑋𝑦))
127123, 126eqtrd 2833 . . . . . 6 ((𝜑𝑦𝐷) → ((𝑈‘(𝐼 × {0}))(.r𝑅)(𝑋‘(𝑦f − (𝐼 × {0})))) = (𝑋𝑦))
128127, 124eqeltrd 2890 . . . . 5 ((𝜑𝑦𝐷) → ((𝑈‘(𝐼 × {0}))(.r𝑅)(𝑋‘(𝑦f − (𝐼 × {0})))) ∈ (Base‘𝑅))
129 fveq2 6652 . . . . . . 7 (𝑧 = (𝐼 × {0}) → (𝑈𝑧) = (𝑈‘(𝐼 × {0})))
130 oveq2 7150 . . . . . . . 8 (𝑧 = (𝐼 × {0}) → (𝑦f𝑧) = (𝑦f − (𝐼 × {0})))
131130fveq2d 6656 . . . . . . 7 (𝑧 = (𝐼 × {0}) → (𝑋‘(𝑦f𝑧)) = (𝑋‘(𝑦f − (𝐼 × {0}))))
132129, 131oveq12d 7160 . . . . . 6 (𝑧 = (𝐼 × {0}) → ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧))) = ((𝑈‘(𝐼 × {0}))(.r𝑅)(𝑋‘(𝑦f − (𝐼 × {0})))))
1332, 132gsumsn 19085 . . . . 5 ((𝑅 ∈ Mnd ∧ (𝐼 × {0}) ∈ 𝐷 ∧ ((𝑈‘(𝐼 × {0}))(.r𝑅)(𝑋‘(𝑦f − (𝐼 × {0})))) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r𝑅)(𝑋‘(𝑦f − (𝐼 × {0})))))
134114, 28, 128, 133syl3anc 1368 . . . 4 ((𝜑𝑦𝐷) → (𝑅 Σg (𝑧 ∈ {(𝐼 × {0})} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r𝑅)(𝑋‘(𝑦f − (𝐼 × {0})))))
13550, 111, 1343eqtr3d 2841 . . 3 ((𝜑𝑦𝐷) → (𝑅 Σg (𝑧 ∈ {𝑔𝐷𝑔r𝑦} ↦ ((𝑈𝑧)(.r𝑅)(𝑋‘(𝑦f𝑧))))) = ((𝑈‘(𝐼 × {0}))(.r𝑅)(𝑋‘(𝑦f − (𝐼 × {0})))))
13622, 135, 1273eqtrd 2837 . 2 ((𝜑𝑦𝐷) → ((𝑈 · 𝑋)‘𝑦) = (𝑋𝑦))
13715, 17, 136eqfnfvd 6789 1 (𝜑 → (𝑈 · 𝑋) = 𝑋)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  {crab 3110  Vcvv 3441   ∖ cdif 3879   ⊆ wss 3882  ifcif 4427  {csn 4527   class class class wbr 5033   ↦ cmpt 5113   × cxp 5520  ◡ccnv 5521   ↾ cres 5524   “ cima 5525  Fun wfun 6323   Fn wfn 6324  ⟶wf 6325  ‘cfv 6329  (class class class)co 7142   ∘f cof 7395   ∘r cofr 7396   supp csupp 7823   ↑m cmap 8404  Fincfn 8507   finSupp cfsupp 8832  0cc0 10541   ≤ cle 10680   − cmin 10874  ℕcn 11640  ℕ0cn0 11900  Basecbs 16492  .rcmulr 16575  0gc0g 16722   Σg cgsu 16723  Mndcmnd 17920  CMndccmn 18916  1rcur 19262  Ringcrg 19308   mPwSer cmps 20609 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 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7451  ax-cnex 10597  ax-resscn 10598  ax-1cn 10599  ax-icn 10600  ax-addcl 10601  ax-addrcl 10602  ax-mulcl 10603  ax-mulrcl 10604  ax-mulcom 10605  ax-addass 10606  ax-mulass 10607  ax-distr 10608  ax-i2m1 10609  ax-1ne0 10610  ax-1rid 10611  ax-rnegex 10612  ax-rrecex 10613  ax-cnre 10614  ax-pre-lttri 10615  ax-pre-lttrn 10616  ax-pre-ltadd 10617  ax-pre-mulgt0 10618 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 3443  df-sbc 3722  df-csb 3830  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4246  df-if 4428  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-se 5482  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-isom 6338  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-of 7397  df-ofr 7398  df-om 7571  df-1st 7681  df-2nd 7682  df-supp 7824  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-2o 8101  df-oadd 8104  df-er 8287  df-map 8406  df-pm 8407  df-ixp 8460  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-fsupp 8833  df-oi 8973  df-card 9367  df-pnf 10681  df-mnf 10682  df-xr 10683  df-ltxr 10684  df-le 10685  df-sub 10876  df-neg 10877  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-z 11987  df-uz 12249  df-fz 12903  df-fzo 13046  df-seq 13382  df-hash 13704  df-struct 16494  df-ndx 16495  df-slot 16496  df-base 16498  df-sets 16499  df-plusg 16587  df-mulr 16588  df-sca 16590  df-vsca 16591  df-tset 16593  df-0g 16724  df-gsum 16725  df-mgm 17861  df-sgrp 17910  df-mnd 17921  df-grp 18115  df-minusg 18116  df-mulg 18235  df-cntz 18457  df-cmn 18918  df-abl 18919  df-mgp 19251  df-ur 19263  df-ring 19310  df-psr 20614 This theorem is referenced by:  psrring  20682  psr1  20683
 Copyright terms: Public domain W3C validator