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

Theorem mplsubrglem 20998
Description: Lemma for mplsubrg 20999. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by AV, 18-Jul-2019.)
Hypotheses
Ref Expression
mplsubg.s 𝑆 = (𝐼 mPwSer 𝑅)
mplsubg.p 𝑃 = (𝐼 mPoly 𝑅)
mplsubg.u 𝑈 = (Base‘𝑃)
mplsubg.i (𝜑𝐼𝑊)
mpllss.r (𝜑𝑅 ∈ Ring)
mplsubrglem.d 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
mplsubrglem.z 0 = (0g𝑅)
mplsubrglem.p 𝐴 = ( ∘f + “ ((𝑋 supp 0 ) × (𝑌 supp 0 )))
mplsubrglem.t · = (.r𝑅)
mplsubrglem.x (𝜑𝑋𝑈)
mplsubrglem.y (𝜑𝑌𝑈)
Assertion
Ref Expression
mplsubrglem (𝜑 → (𝑋(.r𝑆)𝑌) ∈ 𝑈)
Distinct variable groups:   𝑓,𝐼   𝑅,𝑓   𝑆,𝑓   𝑓,𝑋   𝑓,𝑌   0 ,𝑓
Allowed substitution hints:   𝜑(𝑓)   𝐴(𝑓)   𝐷(𝑓)   𝑃(𝑓)   · (𝑓)   𝑈(𝑓)   𝑊(𝑓)

Proof of Theorem mplsubrglem
Dummy variables 𝑘 𝑛 𝑥 𝑔 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplsubg.s . . 3 𝑆 = (𝐼 mPwSer 𝑅)
2 eqid 2739 . . 3 (Base‘𝑆) = (Base‘𝑆)
3 eqid 2739 . . 3 (.r𝑆) = (.r𝑆)
4 mpllss.r . . 3 (𝜑𝑅 ∈ Ring)
5 mplsubg.p . . . . 5 𝑃 = (𝐼 mPoly 𝑅)
6 mplsubg.u . . . . 5 𝑈 = (Base‘𝑃)
75, 1, 6, 2mplbasss 20991 . . . 4 𝑈 ⊆ (Base‘𝑆)
8 mplsubrglem.x . . . 4 (𝜑𝑋𝑈)
97, 8sselid 3915 . . 3 (𝜑𝑋 ∈ (Base‘𝑆))
10 mplsubrglem.y . . . 4 (𝜑𝑌𝑈)
117, 10sselid 3915 . . 3 (𝜑𝑌 ∈ (Base‘𝑆))
121, 2, 3, 4, 9, 11psrmulcl 20945 . 2 (𝜑 → (𝑋(.r𝑆)𝑌) ∈ (Base‘𝑆))
13 ovexd 7270 . . 3 (𝜑 → (𝑋(.r𝑆)𝑌) ∈ V)
141, 2psrelbasfun 20937 . . . 4 ((𝑋(.r𝑆)𝑌) ∈ (Base‘𝑆) → Fun (𝑋(.r𝑆)𝑌))
1512, 14syl 17 . . 3 (𝜑 → Fun (𝑋(.r𝑆)𝑌))
16 mplsubrglem.z . . . . 5 0 = (0g𝑅)
1716fvexi 6753 . . . 4 0 ∈ V
1817a1i 11 . . 3 (𝜑0 ∈ V)
19 mplsubrglem.p . . . . 5 𝐴 = ( ∘f + “ ((𝑋 supp 0 ) × (𝑌 supp 0 )))
20 df-ima 5582 . . . . 5 ( ∘f + “ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) = ran ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))
2119, 20eqtri 2767 . . . 4 𝐴 = ran ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))
225, 1, 2, 16, 6mplelbas 20987 . . . . . . . 8 (𝑋𝑈 ↔ (𝑋 ∈ (Base‘𝑆) ∧ 𝑋 finSupp 0 ))
2322simprbi 500 . . . . . . 7 (𝑋𝑈𝑋 finSupp 0 )
248, 23syl 17 . . . . . 6 (𝜑𝑋 finSupp 0 )
255, 1, 2, 16, 6mplelbas 20987 . . . . . . . 8 (𝑌𝑈 ↔ (𝑌 ∈ (Base‘𝑆) ∧ 𝑌 finSupp 0 ))
2625simprbi 500 . . . . . . 7 (𝑌𝑈𝑌 finSupp 0 )
2710, 26syl 17 . . . . . 6 (𝜑𝑌 finSupp 0 )
28 fsuppxpfi 9032 . . . . . 6 ((𝑋 finSupp 0𝑌 finSupp 0 ) → ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∈ Fin)
2924, 27, 28syl2anc 587 . . . . 5 (𝜑 → ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∈ Fin)
30 ofmres 7779 . . . . . . 7 ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) = (𝑓 ∈ (𝑋 supp 0 ), 𝑔 ∈ (𝑌 supp 0 ) ↦ (𝑓f + 𝑔))
31 ovex 7268 . . . . . . 7 (𝑓f + 𝑔) ∈ V
3230, 31fnmpoi 7862 . . . . . 6 ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 ))
33 dffn4 6661 . . . . . 6 (( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) ↔ ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))):((𝑋 supp 0 ) × (𝑌 supp 0 ))–onto→ran ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))))
3432, 33mpbi 233 . . . . 5 ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))):((𝑋 supp 0 ) × (𝑌 supp 0 ))–onto→ran ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))
35 fofi 8992 . . . . 5 ((((𝑋 supp 0 ) × (𝑌 supp 0 )) ∈ Fin ∧ ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))):((𝑋 supp 0 ) × (𝑌 supp 0 ))–onto→ran ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))) → ran ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) ∈ Fin)
3629, 34, 35sylancl 589 . . . 4 (𝜑 → ran ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) ∈ Fin)
3721, 36eqeltrid 2844 . . 3 (𝜑𝐴 ∈ Fin)
38 eqid 2739 . . . . 5 (Base‘𝑅) = (Base‘𝑅)
39 mplsubrglem.d . . . . 5 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
401, 38, 39, 2, 12psrelbas 20936 . . . 4 (𝜑 → (𝑋(.r𝑆)𝑌):𝐷⟶(Base‘𝑅))
41 mplsubrglem.t . . . . . 6 · = (.r𝑅)
429adantr 484 . . . . . 6 ((𝜑𝑘 ∈ (𝐷𝐴)) → 𝑋 ∈ (Base‘𝑆))
4311adantr 484 . . . . . 6 ((𝜑𝑘 ∈ (𝐷𝐴)) → 𝑌 ∈ (Base‘𝑆))
44 eldifi 4058 . . . . . . 7 (𝑘 ∈ (𝐷𝐴) → 𝑘𝐷)
4544adantl 485 . . . . . 6 ((𝜑𝑘 ∈ (𝐷𝐴)) → 𝑘𝐷)
461, 2, 41, 3, 39, 42, 43, 45psrmulval 20943 . . . . 5 ((𝜑𝑘 ∈ (𝐷𝐴)) → ((𝑋(.r𝑆)𝑌)‘𝑘) = (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥) · (𝑌‘(𝑘f𝑥))))))
474ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑅 ∈ Ring)
485, 38, 6, 39, 10mplelf 20992 . . . . . . . . . . . 12 (𝜑𝑌:𝐷⟶(Base‘𝑅))
4948ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑌:𝐷⟶(Base‘𝑅))
50 ssrab2 4010 . . . . . . . . . . . 12 {𝑦𝐷𝑦r𝑘} ⊆ 𝐷
5145adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑘𝐷)
52 simpr 488 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑥 ∈ {𝑦𝐷𝑦r𝑘})
53 eqid 2739 . . . . . . . . . . . . . 14 {𝑦𝐷𝑦r𝑘} = {𝑦𝐷𝑦r𝑘}
5439, 53psrbagconcl 20925 . . . . . . . . . . . . 13 ((𝑘𝐷𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑘f𝑥) ∈ {𝑦𝐷𝑦r𝑘})
5551, 52, 54syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑘f𝑥) ∈ {𝑦𝐷𝑦r𝑘})
5650, 55sselid 3915 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑘f𝑥) ∈ 𝐷)
5749, 56ffvelrnd 6927 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑌‘(𝑘f𝑥)) ∈ (Base‘𝑅))
5838, 41, 16ringlz 19638 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ (𝑌‘(𝑘f𝑥)) ∈ (Base‘𝑅)) → ( 0 · (𝑌‘(𝑘f𝑥))) = 0 )
5947, 57, 58syl2anc 587 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ( 0 · (𝑌‘(𝑘f𝑥))) = 0 )
60 oveq1 7242 . . . . . . . . . 10 ((𝑋𝑥) = 0 → ((𝑋𝑥) · (𝑌‘(𝑘f𝑥))) = ( 0 · (𝑌‘(𝑘f𝑥))))
6160eqeq1d 2741 . . . . . . . . 9 ((𝑋𝑥) = 0 → (((𝑋𝑥) · (𝑌‘(𝑘f𝑥))) = 0 ↔ ( 0 · (𝑌‘(𝑘f𝑥))) = 0 ))
6259, 61syl5ibrcom 250 . . . . . . . 8 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑋𝑥) = 0 → ((𝑋𝑥) · (𝑌‘(𝑘f𝑥))) = 0 ))
635, 38, 6, 39, 8mplelf 20992 . . . . . . . . . . . 12 (𝜑𝑋:𝐷⟶(Base‘𝑅))
6463ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑋:𝐷⟶(Base‘𝑅))
6550, 52sselid 3915 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑥𝐷)
6664, 65ffvelrnd 6927 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑋𝑥) ∈ (Base‘𝑅))
6738, 41, 16ringrz 19639 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ (𝑋𝑥) ∈ (Base‘𝑅)) → ((𝑋𝑥) · 0 ) = 0 )
6847, 66, 67syl2anc 587 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑋𝑥) · 0 ) = 0 )
69 oveq2 7243 . . . . . . . . . 10 ((𝑌‘(𝑘f𝑥)) = 0 → ((𝑋𝑥) · (𝑌‘(𝑘f𝑥))) = ((𝑋𝑥) · 0 ))
7069eqeq1d 2741 . . . . . . . . 9 ((𝑌‘(𝑘f𝑥)) = 0 → (((𝑋𝑥) · (𝑌‘(𝑘f𝑥))) = 0 ↔ ((𝑋𝑥) · 0 ) = 0 ))
7168, 70syl5ibrcom 250 . . . . . . . 8 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑌‘(𝑘f𝑥)) = 0 → ((𝑋𝑥) · (𝑌‘(𝑘f𝑥))) = 0 ))
7239psrbagf 20909 . . . . . . . . . . . . . . . . . 18 (𝑥𝐷𝑥:𝐼⟶ℕ0)
7365, 72syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑥:𝐼⟶ℕ0)
7473ffvelrnda 6926 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) ∧ 𝑛𝐼) → (𝑥𝑛) ∈ ℕ0)
7539psrbagf 20909 . . . . . . . . . . . . . . . . . 18 (𝑘𝐷𝑘:𝐼⟶ℕ0)
7651, 75syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑘:𝐼⟶ℕ0)
7776ffvelrnda 6926 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) ∧ 𝑛𝐼) → (𝑘𝑛) ∈ ℕ0)
78 nn0cn 12130 . . . . . . . . . . . . . . . . 17 ((𝑥𝑛) ∈ ℕ0 → (𝑥𝑛) ∈ ℂ)
79 nn0cn 12130 . . . . . . . . . . . . . . . . 17 ((𝑘𝑛) ∈ ℕ0 → (𝑘𝑛) ∈ ℂ)
80 pncan3 11116 . . . . . . . . . . . . . . . . 17 (((𝑥𝑛) ∈ ℂ ∧ (𝑘𝑛) ∈ ℂ) → ((𝑥𝑛) + ((𝑘𝑛) − (𝑥𝑛))) = (𝑘𝑛))
8178, 79, 80syl2an 599 . . . . . . . . . . . . . . . 16 (((𝑥𝑛) ∈ ℕ0 ∧ (𝑘𝑛) ∈ ℕ0) → ((𝑥𝑛) + ((𝑘𝑛) − (𝑥𝑛))) = (𝑘𝑛))
8274, 77, 81syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) ∧ 𝑛𝐼) → ((𝑥𝑛) + ((𝑘𝑛) − (𝑥𝑛))) = (𝑘𝑛))
8382mpteq2dva 5167 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑛𝐼 ↦ ((𝑥𝑛) + ((𝑘𝑛) − (𝑥𝑛)))) = (𝑛𝐼 ↦ (𝑘𝑛)))
84 mplsubg.i . . . . . . . . . . . . . . . 16 (𝜑𝐼𝑊)
8584ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝐼𝑊)
86 ovexd 7270 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) ∧ 𝑛𝐼) → ((𝑘𝑛) − (𝑥𝑛)) ∈ V)
8773feqmptd 6802 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑥 = (𝑛𝐼 ↦ (𝑥𝑛)))
8876feqmptd 6802 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑘 = (𝑛𝐼 ↦ (𝑘𝑛)))
8985, 77, 74, 88, 87offval2 7510 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑘f𝑥) = (𝑛𝐼 ↦ ((𝑘𝑛) − (𝑥𝑛))))
9085, 74, 86, 87, 89offval2 7510 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑥f + (𝑘f𝑥)) = (𝑛𝐼 ↦ ((𝑥𝑛) + ((𝑘𝑛) − (𝑥𝑛)))))
9183, 90, 883eqtr4d 2789 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑥f + (𝑘f𝑥)) = 𝑘)
92 simplr 769 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝑘 ∈ (𝐷𝐴))
9391, 92eqeltrd 2840 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑥f + (𝑘f𝑥)) ∈ (𝐷𝐴))
9493eldifbd 3896 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ¬ (𝑥f + (𝑘f𝑥)) ∈ 𝐴)
95 ovres 7396 . . . . . . . . . . . 12 ((𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘f𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))(𝑘f𝑥)) = (𝑥f + (𝑘f𝑥)))
96 fnovrn 7405 . . . . . . . . . . . . . 14 ((( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∧ 𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘f𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))(𝑘f𝑥)) ∈ ran ( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))))
9796, 21eleqtrrdi 2851 . . . . . . . . . . . . 13 ((( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) Fn ((𝑋 supp 0 ) × (𝑌 supp 0 )) ∧ 𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘f𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))(𝑘f𝑥)) ∈ 𝐴)
9832, 97mp3an1 1450 . . . . . . . . . . . 12 ((𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘f𝑥) ∈ (𝑌 supp 0 )) → (𝑥( ∘f + ↾ ((𝑋 supp 0 ) × (𝑌 supp 0 )))(𝑘f𝑥)) ∈ 𝐴)
9995, 98eqeltrrd 2841 . . . . . . . . . . 11 ((𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘f𝑥) ∈ (𝑌 supp 0 )) → (𝑥f + (𝑘f𝑥)) ∈ 𝐴)
10094, 99nsyl 142 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ¬ (𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘f𝑥) ∈ (𝑌 supp 0 )))
101 ianor 982 . . . . . . . . . 10 (¬ (𝑥 ∈ (𝑋 supp 0 ) ∧ (𝑘f𝑥) ∈ (𝑌 supp 0 )) ↔ (¬ 𝑥 ∈ (𝑋 supp 0 ) ∨ ¬ (𝑘f𝑥) ∈ (𝑌 supp 0 )))
102100, 101sylib 221 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (¬ 𝑥 ∈ (𝑋 supp 0 ) ∨ ¬ (𝑘f𝑥) ∈ (𝑌 supp 0 )))
103 eldif 3893 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ (𝑥𝐷 ∧ ¬ 𝑥 ∈ (𝑋 supp 0 )))
104103baib 539 . . . . . . . . . . . 12 (𝑥𝐷 → (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ ¬ 𝑥 ∈ (𝑋 supp 0 )))
10565, 104syl 17 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ ¬ 𝑥 ∈ (𝑋 supp 0 )))
106 ssidd 3941 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑋 supp 0 ) ⊆ (𝑋 supp 0 ))
107 ovex 7268 . . . . . . . . . . . . . . 15 (ℕ0m 𝐼) ∈ V
10839, 107rabex2 5244 . . . . . . . . . . . . . 14 𝐷 ∈ V
109108a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 𝐷 ∈ V)
11017a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → 0 ∈ V)
11164, 106, 109, 110suppssr 7962 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) ∧ 𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋𝑥) = 0 )
112111ex 416 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑥 ∈ (𝐷 ∖ (𝑋 supp 0 )) → (𝑋𝑥) = 0 ))
113105, 112sylbird 263 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (¬ 𝑥 ∈ (𝑋 supp 0 ) → (𝑋𝑥) = 0 ))
114 eldif 3893 . . . . . . . . . . . . 13 ((𝑘f𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) ↔ ((𝑘f𝑥) ∈ 𝐷 ∧ ¬ (𝑘f𝑥) ∈ (𝑌 supp 0 )))
115114baib 539 . . . . . . . . . . . 12 ((𝑘f𝑥) ∈ 𝐷 → ((𝑘f𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) ↔ ¬ (𝑘f𝑥) ∈ (𝑌 supp 0 )))
11656, 115syl 17 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑘f𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) ↔ ¬ (𝑘f𝑥) ∈ (𝑌 supp 0 )))
117 ssidd 3941 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (𝑌 supp 0 ) ⊆ (𝑌 supp 0 ))
11849, 117, 109, 110suppssr 7962 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) ∧ (𝑘f𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 ))) → (𝑌‘(𝑘f𝑥)) = 0 )
119118ex 416 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑘f𝑥) ∈ (𝐷 ∖ (𝑌 supp 0 )) → (𝑌‘(𝑘f𝑥)) = 0 ))
120116, 119sylbird 263 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → (¬ (𝑘f𝑥) ∈ (𝑌 supp 0 ) → (𝑌‘(𝑘f𝑥)) = 0 ))
121113, 120orim12d 965 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((¬ 𝑥 ∈ (𝑋 supp 0 ) ∨ ¬ (𝑘f𝑥) ∈ (𝑌 supp 0 )) → ((𝑋𝑥) = 0 ∨ (𝑌‘(𝑘f𝑥)) = 0 )))
122102, 121mpd 15 . . . . . . . 8 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑋𝑥) = 0 ∨ (𝑌‘(𝑘f𝑥)) = 0 ))
12362, 71, 122mpjaod 860 . . . . . . 7 (((𝜑𝑘 ∈ (𝐷𝐴)) ∧ 𝑥 ∈ {𝑦𝐷𝑦r𝑘}) → ((𝑋𝑥) · (𝑌‘(𝑘f𝑥))) = 0 )
124123mpteq2dva 5167 . . . . . 6 ((𝜑𝑘 ∈ (𝐷𝐴)) → (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥) · (𝑌‘(𝑘f𝑥)))) = (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ 0 ))
125124oveq2d 7251 . . . . 5 ((𝜑𝑘 ∈ (𝐷𝐴)) → (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ ((𝑋𝑥) · (𝑌‘(𝑘f𝑥))))) = (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ 0 )))
1264adantr 484 . . . . . . 7 ((𝜑𝑘 ∈ (𝐷𝐴)) → 𝑅 ∈ Ring)
127 ringmnd 19605 . . . . . . 7 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
128126, 127syl 17 . . . . . 6 ((𝜑𝑘 ∈ (𝐷𝐴)) → 𝑅 ∈ Mnd)
12939psrbaglefi 20923 . . . . . . 7 (𝑘𝐷 → {𝑦𝐷𝑦r𝑘} ∈ Fin)
13045, 129syl 17 . . . . . 6 ((𝜑𝑘 ∈ (𝐷𝐴)) → {𝑦𝐷𝑦r𝑘} ∈ Fin)
13116gsumz 18295 . . . . . 6 ((𝑅 ∈ Mnd ∧ {𝑦𝐷𝑦r𝑘} ∈ Fin) → (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ 0 )) = 0 )
132128, 130, 131syl2anc 587 . . . . 5 ((𝜑𝑘 ∈ (𝐷𝐴)) → (𝑅 Σg (𝑥 ∈ {𝑦𝐷𝑦r𝑘} ↦ 0 )) = 0 )
13346, 125, 1323eqtrd 2783 . . . 4 ((𝜑𝑘 ∈ (𝐷𝐴)) → ((𝑋(.r𝑆)𝑌)‘𝑘) = 0 )
13440, 133suppss 7960 . . 3 (𝜑 → ((𝑋(.r𝑆)𝑌) supp 0 ) ⊆ 𝐴)
135 suppssfifsupp 9030 . . 3 ((((𝑋(.r𝑆)𝑌) ∈ V ∧ Fun (𝑋(.r𝑆)𝑌) ∧ 0 ∈ V) ∧ (𝐴 ∈ Fin ∧ ((𝑋(.r𝑆)𝑌) supp 0 ) ⊆ 𝐴)) → (𝑋(.r𝑆)𝑌) finSupp 0 )
13613, 15, 18, 37, 134, 135syl32anc 1380 . 2 (𝜑 → (𝑋(.r𝑆)𝑌) finSupp 0 )
1375, 1, 2, 16, 6mplelbas 20987 . 2 ((𝑋(.r𝑆)𝑌) ∈ 𝑈 ↔ ((𝑋(.r𝑆)𝑌) ∈ (Base‘𝑆) ∧ (𝑋(.r𝑆)𝑌) finSupp 0 ))
13812, 136, 137sylanbrc 586 1 (𝜑 → (𝑋(.r𝑆)𝑌) ∈ 𝑈)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847  w3a 1089   = wceq 1543  wcel 2112  {crab 3068  Vcvv 3423  cdif 3880  wss 3883   class class class wbr 5070  cmpt 5152   × cxp 5567  ccnv 5568  ran crn 5570  cres 5571  cima 5572  Fun wfun 6395   Fn wfn 6396  wf 6397  ontowfo 6399  cfv 6401  (class class class)co 7235  f cof 7489  r cofr 7490   supp csupp 7927  m cmap 8532  Fincfn 8650   finSupp cfsupp 9015  cc 10757   + caddc 10762  cle 10898  cmin 11092  cn 11860  0cn0 12120  Basecbs 16793  .rcmulr 16836  0gc0g 16977   Σg cgsu 16978  Mndcmnd 18206  Ringcrg 19595   mPwSer cmps 20895   mPoly cmpl 20897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5196  ax-sep 5209  ax-nul 5216  ax-pow 5275  ax-pr 5339  ax-un 7545  ax-cnex 10815  ax-resscn 10816  ax-1cn 10817  ax-icn 10818  ax-addcl 10819  ax-addrcl 10820  ax-mulcl 10821  ax-mulrcl 10822  ax-mulcom 10823  ax-addass 10824  ax-mulass 10825  ax-distr 10826  ax-i2m1 10827  ax-1ne0 10828  ax-1rid 10829  ax-rnegex 10830  ax-rrecex 10831  ax-cnre 10832  ax-pre-lttri 10833  ax-pre-lttrn 10834  ax-pre-ltadd 10835  ax-pre-mulgt0 10836
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5179  df-id 5472  df-eprel 5478  df-po 5486  df-so 5487  df-fr 5527  df-se 5528  df-we 5529  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-rn 5580  df-res 5581  df-ima 5582  df-pred 6179  df-ord 6237  df-on 6238  df-lim 6239  df-suc 6240  df-iota 6359  df-fun 6403  df-fn 6404  df-f 6405  df-f1 6406  df-fo 6407  df-f1o 6408  df-fv 6409  df-isom 6410  df-riota 7192  df-ov 7238  df-oprab 7239  df-mpo 7240  df-of 7491  df-ofr 7492  df-om 7667  df-1st 7783  df-2nd 7784  df-supp 7928  df-wrecs 8071  df-recs 8132  df-rdg 8170  df-1o 8226  df-er 8415  df-map 8534  df-pm 8535  df-ixp 8603  df-en 8651  df-dom 8652  df-sdom 8653  df-fin 8654  df-fsupp 9016  df-oi 9156  df-card 9585  df-pnf 10899  df-mnf 10900  df-xr 10901  df-ltxr 10902  df-le 10903  df-sub 11094  df-neg 11095  df-nn 11861  df-2 11923  df-3 11924  df-4 11925  df-5 11926  df-6 11927  df-7 11928  df-8 11929  df-9 11930  df-n0 12121  df-z 12207  df-uz 12469  df-fz 13126  df-fzo 13269  df-seq 13607  df-hash 13930  df-struct 16733  df-sets 16750  df-slot 16768  df-ndx 16778  df-base 16794  df-ress 16818  df-plusg 16848  df-mulr 16849  df-sca 16851  df-vsca 16852  df-tset 16854  df-0g 16979  df-gsum 16980  df-mgm 18147  df-sgrp 18196  df-mnd 18207  df-grp 18401  df-minusg 18402  df-cntz 18744  df-cmn 19205  df-abl 19206  df-mgp 19538  df-ur 19550  df-ring 19597  df-psr 20900  df-mpl 20902
This theorem is referenced by:  mplsubrg  20999
  Copyright terms: Public domain W3C validator