Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvmptfprodlem Structured version   Visualization version   GIF version

Theorem dvmptfprodlem 45255
Description: Induction step for dvmptfprod 45256. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
dvmptfprodlem.xph โ„ฒ๐‘ฅ๐œ‘
dvmptfprodlem.iph โ„ฒ๐‘–๐œ‘
dvmptfprodlem.jph โ„ฒ๐‘—๐œ‘
dvmptfprodlem.if โ„ฒ๐‘–๐น
dvmptfprodlem.jg โ„ฒ๐‘—๐บ
dvmptfprodlem.a ((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚)
dvmptfprodlem.d (๐œ‘ โ†’ ๐ท โˆˆ Fin)
dvmptfprodlem.e (๐œ‘ โ†’ ๐ธ โˆˆ V)
dvmptfprodlem.db (๐œ‘ โ†’ ยฌ ๐ธ โˆˆ ๐ท)
dvmptfprodlem.ss (๐œ‘ โ†’ (๐ท โˆช {๐ธ}) โІ ๐ผ)
dvmptfprodlem.s (๐œ‘ โ†’ ๐‘† โˆˆ {โ„, โ„‚})
dvmptfprodlem.c (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ ๐ถ โˆˆ โ„‚)
dvmptfprodlem.dvp (๐œ‘ โ†’ (๐‘† D (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ โˆ๐‘– โˆˆ ๐ท ๐ด)) = (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด)))
dvmptfprodlem.14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐บ โˆˆ โ„‚)
dvmptfprodlem.dvf (๐œ‘ โ†’ (๐‘† D (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐น)) = (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐บ))
dvmptfprodlem.f (๐‘– = ๐ธ โ†’ ๐ด = ๐น)
dvmptfprodlem.cg (๐‘— = ๐ธ โ†’ ๐ถ = ๐บ)
Assertion
Ref Expression
dvmptfprodlem (๐œ‘ โ†’ (๐‘† D (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ โˆ๐‘– โˆˆ (๐ท โˆช {๐ธ})๐ด)) = (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ฮฃ๐‘— โˆˆ (๐ท โˆช {๐ธ})(๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด)))
Distinct variable groups:   ๐ด,๐‘—   ๐ท,๐‘–,๐‘—,๐‘ฅ   ๐‘–,๐ธ,๐‘—,๐‘ฅ   ๐‘—,๐น   ๐‘–,๐ผ   ๐‘–,๐‘‹,๐‘—,๐‘ฅ
Allowed substitution hints:   ๐œ‘(๐‘ฅ,๐‘–,๐‘—)   ๐ด(๐‘ฅ,๐‘–)   ๐ถ(๐‘ฅ,๐‘–,๐‘—)   ๐‘†(๐‘ฅ,๐‘–,๐‘—)   ๐น(๐‘ฅ,๐‘–)   ๐บ(๐‘ฅ,๐‘–,๐‘—)   ๐ผ(๐‘ฅ,๐‘—)

Proof of Theorem dvmptfprodlem
StepHypRef Expression
1 dvmptfprodlem.xph . . . 4 โ„ฒ๐‘ฅ๐œ‘
2 dvmptfprodlem.iph . . . . . . 7 โ„ฒ๐‘–๐œ‘
3 nfcv 2898 . . . . . . . 8 โ„ฒ๐‘–๐‘ฅ
4 nfcv 2898 . . . . . . . 8 โ„ฒ๐‘–๐‘‹
53, 4nfel 2912 . . . . . . 7 โ„ฒ๐‘– ๐‘ฅ โˆˆ ๐‘‹
62, 5nfan 1895 . . . . . 6 โ„ฒ๐‘–(๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹)
7 dvmptfprodlem.if . . . . . . 7 โ„ฒ๐‘–๐น
87a1i 11 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ โ„ฒ๐‘–๐น)
9 dvmptfprodlem.d . . . . . . . 8 (๐œ‘ โ†’ ๐ท โˆˆ Fin)
10 snfi 9060 . . . . . . . . 9 {๐ธ} โˆˆ Fin
1110a1i 11 . . . . . . . 8 (๐œ‘ โ†’ {๐ธ} โˆˆ Fin)
12 unfi 9188 . . . . . . . 8 ((๐ท โˆˆ Fin โˆง {๐ธ} โˆˆ Fin) โ†’ (๐ท โˆช {๐ธ}) โˆˆ Fin)
139, 11, 12syl2anc 583 . . . . . . 7 (๐œ‘ โ†’ (๐ท โˆช {๐ธ}) โˆˆ Fin)
1413adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ (๐ท โˆช {๐ธ}) โˆˆ Fin)
15 simpll 766 . . . . . . 7 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ (๐ท โˆช {๐ธ})) โ†’ ๐œ‘)
16 dvmptfprodlem.ss . . . . . . . . 9 (๐œ‘ โ†’ (๐ท โˆช {๐ธ}) โІ ๐ผ)
1716sselda 3978 . . . . . . . 8 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ท โˆช {๐ธ})) โ†’ ๐‘– โˆˆ ๐ผ)
1817adantlr 714 . . . . . . 7 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ (๐ท โˆช {๐ธ})) โ†’ ๐‘– โˆˆ ๐ผ)
19 simplr 768 . . . . . . 7 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ (๐ท โˆช {๐ธ})) โ†’ ๐‘ฅ โˆˆ ๐‘‹)
20 dvmptfprodlem.a . . . . . . 7 ((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚)
2115, 18, 19, 20syl3anc 1369 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ (๐ท โˆช {๐ธ})) โ†’ ๐ด โˆˆ โ„‚)
22 dvmptfprodlem.e . . . . . . . . 9 (๐œ‘ โ†’ ๐ธ โˆˆ V)
23 snidg 4658 . . . . . . . . 9 (๐ธ โˆˆ V โ†’ ๐ธ โˆˆ {๐ธ})
2422, 23syl 17 . . . . . . . 8 (๐œ‘ โ†’ ๐ธ โˆˆ {๐ธ})
25 elun2 4173 . . . . . . . 8 (๐ธ โˆˆ {๐ธ} โ†’ ๐ธ โˆˆ (๐ท โˆช {๐ธ}))
2624, 25syl 17 . . . . . . 7 (๐œ‘ โ†’ ๐ธ โˆˆ (๐ท โˆช {๐ธ}))
2726adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ธ โˆˆ (๐ท โˆช {๐ธ}))
28 dvmptfprodlem.f . . . . . . 7 (๐‘– = ๐ธ โ†’ ๐ด = ๐น)
2928adantl 481 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– = ๐ธ) โ†’ ๐ด = ๐น)
306, 8, 14, 21, 27, 29fprodsplit1f 15958 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ โˆ๐‘– โˆˆ (๐ท โˆช {๐ธ})๐ด = (๐น ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด))
31 difundir 4276 . . . . . . . . . 10 ((๐ท โˆช {๐ธ}) โˆ– {๐ธ}) = ((๐ท โˆ– {๐ธ}) โˆช ({๐ธ} โˆ– {๐ธ}))
3231a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ}) = ((๐ท โˆ– {๐ธ}) โˆช ({๐ธ} โˆ– {๐ธ})))
33 dvmptfprodlem.db . . . . . . . . . . 11 (๐œ‘ โ†’ ยฌ ๐ธ โˆˆ ๐ท)
34 difsn 4797 . . . . . . . . . . 11 (ยฌ ๐ธ โˆˆ ๐ท โ†’ (๐ท โˆ– {๐ธ}) = ๐ท)
3533, 34syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ท โˆ– {๐ธ}) = ๐ท)
36 difid 4366 . . . . . . . . . . 11 ({๐ธ} โˆ– {๐ธ}) = โˆ…
3736a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ ({๐ธ} โˆ– {๐ธ}) = โˆ…)
3835, 37uneq12d 4160 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ท โˆ– {๐ธ}) โˆช ({๐ธ} โˆ– {๐ธ})) = (๐ท โˆช โˆ…))
39 un0 4386 . . . . . . . . . 10 (๐ท โˆช โˆ…) = ๐ท
4039a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ (๐ท โˆช โˆ…) = ๐ท)
4132, 38, 403eqtrd 2771 . . . . . . . 8 (๐œ‘ โ†’ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ}) = ๐ท)
4241prodeq1d 15889 . . . . . . 7 (๐œ‘ โ†’ โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด = โˆ๐‘– โˆˆ ๐ท ๐ด)
4342oveq2d 7430 . . . . . 6 (๐œ‘ โ†’ (๐น ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด) = (๐น ยท โˆ๐‘– โˆˆ ๐ท ๐ด))
4443adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ (๐น ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด) = (๐น ยท โˆ๐‘– โˆˆ ๐ท ๐ด))
4530, 44eqtrd 2767 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ โˆ๐‘– โˆˆ (๐ท โˆช {๐ธ})๐ด = (๐น ยท โˆ๐‘– โˆˆ ๐ท ๐ด))
461, 45mpteq2da 5240 . . 3 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ โˆ๐‘– โˆˆ (๐ท โˆช {๐ธ})๐ด) = (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ (๐น ยท โˆ๐‘– โˆˆ ๐ท ๐ด)))
4746oveq2d 7430 . 2 (๐œ‘ โ†’ (๐‘† D (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ โˆ๐‘– โˆˆ (๐ท โˆช {๐ธ})๐ด)) = (๐‘† D (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ (๐น ยท โˆ๐‘– โˆˆ ๐ท ๐ด))))
48 dvmptfprodlem.s . . 3 (๐œ‘ โ†’ ๐‘† โˆˆ {โ„, โ„‚})
4916, 26sseldd 3979 . . . . 5 (๐œ‘ โ†’ ๐ธ โˆˆ ๐ผ)
5049adantr 480 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ธ โˆˆ ๐ผ)
51 simpl 482 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐œ‘)
52 simpr 484 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐‘ฅ โˆˆ ๐‘‹)
5351, 50, 523jca 1126 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ (๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹))
54 nfcv 2898 . . . . 5 โ„ฒ๐‘–๐ธ
55 nfv 1910 . . . . . . 7 โ„ฒ๐‘– ๐ธ โˆˆ ๐ผ
562, 55, 5nf3an 1897 . . . . . 6 โ„ฒ๐‘–(๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹)
57 nfcv 2898 . . . . . . 7 โ„ฒ๐‘–โ„‚
587, 57nfel 2912 . . . . . 6 โ„ฒ๐‘– ๐น โˆˆ โ„‚
5956, 58nfim 1892 . . . . 5 โ„ฒ๐‘–((๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐น โˆˆ โ„‚)
60 ancom 460 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– = ๐ธ) โ†” (๐‘– = ๐ธ โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹)))
6160imbi1i 349 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– = ๐ธ) โ†’ ๐ด = ๐น) โ†” ((๐‘– = ๐ธ โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹)) โ†’ ๐ด = ๐น))
62 eqcom 2734 . . . . . . . . . . . . 13 (๐ด = ๐น โ†” ๐น = ๐ด)
6362imbi2i 336 . . . . . . . . . . . 12 (((๐‘– = ๐ธ โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹)) โ†’ ๐ด = ๐น) โ†” ((๐‘– = ๐ธ โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹)) โ†’ ๐น = ๐ด))
6461, 63bitri 275 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– = ๐ธ) โ†’ ๐ด = ๐น) โ†” ((๐‘– = ๐ธ โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹)) โ†’ ๐น = ๐ด))
6529, 64mpbi 229 . . . . . . . . . 10 ((๐‘– = ๐ธ โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹)) โ†’ ๐น = ๐ด)
66653adantr2 1168 . . . . . . . . 9 ((๐‘– = ๐ธ โˆง (๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹)) โ†’ ๐น = ๐ด)
67663adant2 1129 . . . . . . . 8 ((๐‘– = ๐ธ โˆง ((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚) โˆง (๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹)) โ†’ ๐น = ๐ด)
68 simp3 1136 . . . . . . . . 9 ((๐‘– = ๐ธ โˆง ((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚) โˆง (๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹)) โ†’ (๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹))
69 eleq1 2816 . . . . . . . . . . . . 13 (๐‘– = ๐ธ โ†’ (๐‘– โˆˆ ๐ผ โ†” ๐ธ โˆˆ ๐ผ))
70693anbi2d 1438 . . . . . . . . . . . 12 (๐‘– = ๐ธ โ†’ ((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†” (๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹)))
7170imbi1d 341 . . . . . . . . . . 11 (๐‘– = ๐ธ โ†’ (((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚) โ†” ((๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚)))
7271biimpa 476 . . . . . . . . . 10 ((๐‘– = ๐ธ โˆง ((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚)) โ†’ ((๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚))
73723adant3 1130 . . . . . . . . 9 ((๐‘– = ๐ธ โˆง ((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚) โˆง (๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹)) โ†’ ((๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚))
7468, 73mpd 15 . . . . . . . 8 ((๐‘– = ๐ธ โˆง ((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚) โˆง (๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹)) โ†’ ๐ด โˆˆ โ„‚)
7567, 74eqeltrd 2828 . . . . . . 7 ((๐‘– = ๐ธ โˆง ((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚) โˆง (๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹)) โ†’ ๐น โˆˆ โ„‚)
76753exp 1117 . . . . . 6 (๐‘– = ๐ธ โ†’ (((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚) โ†’ ((๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐น โˆˆ โ„‚)))
77202a1i 12 . . . . . 6 (๐‘– = ๐ธ โ†’ (((๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐น โˆˆ โ„‚) โ†’ ((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚)))
7876, 77impbid 211 . . . . 5 (๐‘– = ๐ธ โ†’ (((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ โ„‚) โ†” ((๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐น โˆˆ โ„‚)))
7954, 59, 78, 20vtoclgf 3553 . . . 4 (๐ธ โˆˆ ๐ผ โ†’ ((๐œ‘ โˆง ๐ธ โˆˆ ๐ผ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐น โˆˆ โ„‚))
8050, 53, 79sylc 65 . . 3 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐น โˆˆ โ„‚)
81 dvmptfprodlem.14 . . 3 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐บ โˆˆ โ„‚)
82 dvmptfprodlem.dvf . . 3 (๐œ‘ โ†’ (๐‘† D (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐น)) = (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ๐บ))
8351, 9syl 17 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ท โˆˆ Fin)
8451adantr 480 . . . . 5 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ ๐ท) โ†’ ๐œ‘)
8516adantr 480 . . . . . . 7 ((๐œ‘ โˆง ๐‘– โˆˆ ๐ท) โ†’ (๐ท โˆช {๐ธ}) โІ ๐ผ)
86 elun1 4172 . . . . . . . 8 (๐‘– โˆˆ ๐ท โ†’ ๐‘– โˆˆ (๐ท โˆช {๐ธ}))
8786adantl 481 . . . . . . 7 ((๐œ‘ โˆง ๐‘– โˆˆ ๐ท) โ†’ ๐‘– โˆˆ (๐ท โˆช {๐ธ}))
8885, 87sseldd 3979 . . . . . 6 ((๐œ‘ โˆง ๐‘– โˆˆ ๐ท) โ†’ ๐‘– โˆˆ ๐ผ)
8988adantlr 714 . . . . 5 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ ๐ท) โ†’ ๐‘– โˆˆ ๐ผ)
9052adantr 480 . . . . 5 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ ๐ท) โ†’ ๐‘ฅ โˆˆ ๐‘‹)
9184, 89, 90, 20syl3anc 1369 . . . 4 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ ๐ท) โ†’ ๐ด โˆˆ โ„‚)
926, 83, 91fprodclf 15960 . . 3 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ โˆ๐‘– โˆˆ ๐ท ๐ด โˆˆ โ„‚)
93 dvmptfprodlem.jph . . . . 5 โ„ฒ๐‘—๐œ‘
94 nfv 1910 . . . . 5 โ„ฒ๐‘— ๐‘ฅ โˆˆ ๐‘‹
9593, 94nfan 1895 . . . 4 โ„ฒ๐‘—(๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹)
96 dvmptfprodlem.c . . . . 5 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ ๐ถ โˆˆ โ„‚)
97 diffi 9195 . . . . . . . . 9 (๐ท โˆˆ Fin โ†’ (๐ท โˆ– {๐‘—}) โˆˆ Fin)
989, 97syl 17 . . . . . . . 8 (๐œ‘ โ†’ (๐ท โˆ– {๐‘—}) โˆˆ Fin)
9998adantr 480 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ (๐ท โˆ– {๐‘—}) โˆˆ Fin)
100 eldifi 4122 . . . . . . . . 9 (๐‘– โˆˆ (๐ท โˆ– {๐‘—}) โ†’ ๐‘– โˆˆ ๐ท)
101100adantl 481 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ (๐ท โˆ– {๐‘—})) โ†’ ๐‘– โˆˆ ๐ท)
102101, 91syldan 590 . . . . . . 7 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ (๐ท โˆ– {๐‘—})) โ†’ ๐ด โˆˆ โ„‚)
1036, 99, 102fprodclf 15960 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด โˆˆ โ„‚)
104103adantr 480 . . . . 5 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด โˆˆ โ„‚)
10596, 104mulcld 11256 . . . 4 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) โˆˆ โ„‚)
10695, 83, 105fsumclf 15708 . . 3 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) โˆˆ โ„‚)
107 dvmptfprodlem.dvp . . 3 (๐œ‘ โ†’ (๐‘† D (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ โˆ๐‘– โˆˆ ๐ท ๐ด)) = (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด)))
1081, 48, 80, 81, 82, 92, 106, 107dvmptmulf 45248 . 2 (๐œ‘ โ†’ (๐‘† D (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ (๐น ยท โˆ๐‘– โˆˆ ๐ท ๐ด))) = (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ((๐บ ยท โˆ๐‘– โˆˆ ๐ท ๐ด) + (ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น))))
109 dvmptfprodlem.jg . . . . . 6 โ„ฒ๐‘—๐บ
110 nfcv 2898 . . . . . 6 โ„ฒ๐‘— ยท
111 nfcv 2898 . . . . . 6 โ„ฒ๐‘—โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด
112109, 110, 111nfov 7444 . . . . 5 โ„ฒ๐‘—(๐บ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด)
11351, 22syl 17 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ธ โˆˆ V)
11451, 33syl 17 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ยฌ ๐ธ โˆˆ ๐ท)
115 diffi 9195 . . . . . . . . . 10 ((๐ท โˆช {๐ธ}) โˆˆ Fin โ†’ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—}) โˆˆ Fin)
11613, 115syl 17 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—}) โˆˆ Fin)
117116adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—}) โˆˆ Fin)
118 eldifi 4122 . . . . . . . . . 10 (๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—}) โ†’ ๐‘– โˆˆ (๐ท โˆช {๐ธ}))
119118adantl 481 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})) โ†’ ๐‘– โˆˆ (๐ท โˆช {๐ธ}))
120119, 21syldan 590 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})) โ†’ ๐ด โˆˆ โ„‚)
1216, 117, 120fprodclf 15960 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด โˆˆ โ„‚)
122121adantr 480 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด โˆˆ โ„‚)
12396, 122mulcld 11256 . . . . 5 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด) โˆˆ โ„‚)
124 dvmptfprodlem.cg . . . . . 6 (๐‘— = ๐ธ โ†’ ๐ถ = ๐บ)
125 sneq 4634 . . . . . . . 8 (๐‘— = ๐ธ โ†’ {๐‘—} = {๐ธ})
126125difeq2d 4118 . . . . . . 7 (๐‘— = ๐ธ โ†’ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—}) = ((๐ท โˆช {๐ธ}) โˆ– {๐ธ}))
127126prodeq1d 15889 . . . . . 6 (๐‘— = ๐ธ โ†’ โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด = โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด)
128124, 127oveq12d 7432 . . . . 5 (๐‘— = ๐ธ โ†’ (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด) = (๐บ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด))
12941, 9eqeltrd 2828 . . . . . . . 8 (๐œ‘ โ†’ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ}) โˆˆ Fin)
130129adantr 480 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ}) โˆˆ Fin)
13151adantr 480 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})) โ†’ ๐œ‘)
13216adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})) โ†’ (๐ท โˆช {๐ธ}) โІ ๐ผ)
133 eldifi 4122 . . . . . . . . . . 11 (๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ}) โ†’ ๐‘– โˆˆ (๐ท โˆช {๐ธ}))
134133adantl 481 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})) โ†’ ๐‘– โˆˆ (๐ท โˆช {๐ธ}))
135132, 134sseldd 3979 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})) โ†’ ๐‘– โˆˆ ๐ผ)
136135adantlr 714 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})) โ†’ ๐‘– โˆˆ ๐ผ)
13752adantr 480 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})) โ†’ ๐‘ฅ โˆˆ ๐‘‹)
138131, 136, 137, 20syl3anc 1369 . . . . . . 7 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})) โ†’ ๐ด โˆˆ โ„‚)
1396, 130, 138fprodclf 15960 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด โˆˆ โ„‚)
14081, 139mulcld 11256 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ (๐บ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด) โˆˆ โ„‚)
14195, 112, 83, 113, 114, 123, 128, 140fsumsplitsn 15714 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ฮฃ๐‘— โˆˆ (๐ท โˆช {๐ธ})(๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด) = (ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด) + (๐บ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด)))
142 difundir 4276 . . . . . . . . . . . . . . . . 17 ((๐ท โˆช {๐ธ}) โˆ– {๐‘—}) = ((๐ท โˆ– {๐‘—}) โˆช ({๐ธ} โˆ– {๐‘—}))
143142a1i 11 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โ†’ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—}) = ((๐ท โˆ– {๐‘—}) โˆช ({๐ธ} โˆ– {๐‘—})))
144 nfv 1910 . . . . . . . . . . . . . . . . . . . . 21 โ„ฒ๐‘ฅ ๐‘— โˆˆ ๐ท
1451, 144nfan 1895 . . . . . . . . . . . . . . . . . . . 20 โ„ฒ๐‘ฅ(๐œ‘ โˆง ๐‘— โˆˆ ๐ท)
146 elsni 4641 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ฅ โˆˆ {๐ธ} โ†’ ๐‘ฅ = ๐ธ)
147146eqcomd 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ฅ โˆˆ {๐ธ} โ†’ ๐ธ = ๐‘ฅ)
148147adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฅ โˆˆ {๐ธ} โˆง ๐‘ฅ = ๐‘—) โ†’ ๐ธ = ๐‘ฅ)
149 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฅ โˆˆ {๐ธ} โˆง ๐‘ฅ = ๐‘—) โ†’ ๐‘ฅ = ๐‘—)
150 eqidd 2728 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฅ โˆˆ {๐ธ} โˆง ๐‘ฅ = ๐‘—) โ†’ ๐‘— = ๐‘—)
151148, 149, 1503eqtrd 2771 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฅ โˆˆ {๐ธ} โˆง ๐‘ฅ = ๐‘—) โ†’ ๐ธ = ๐‘—)
152151adantll 713 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โˆง ๐‘ฅ โˆˆ {๐ธ}) โˆง ๐‘ฅ = ๐‘—) โ†’ ๐ธ = ๐‘—)
153 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โˆง ๐‘ฅ โˆˆ {๐ธ}) โˆง ๐‘ฅ = ๐‘—) โ†’ ๐‘— โˆˆ ๐ท)
154152, 153eqeltrd 2828 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โˆง ๐‘ฅ โˆˆ {๐ธ}) โˆง ๐‘ฅ = ๐‘—) โ†’ ๐ธ โˆˆ ๐ท)
15533ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โˆง ๐‘ฅ โˆˆ {๐ธ}) โˆง ๐‘ฅ = ๐‘—) โ†’ ยฌ ๐ธ โˆˆ ๐ท)
156154, 155pm2.65da 816 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โˆง ๐‘ฅ โˆˆ {๐ธ}) โ†’ ยฌ ๐‘ฅ = ๐‘—)
157 velsn 4640 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ {๐‘—} โ†” ๐‘ฅ = ๐‘—)
158156, 157sylnibr 329 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โˆง ๐‘ฅ โˆˆ {๐ธ}) โ†’ ยฌ ๐‘ฅ โˆˆ {๐‘—})
159158ex 412 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โ†’ (๐‘ฅ โˆˆ {๐ธ} โ†’ ยฌ ๐‘ฅ โˆˆ {๐‘—}))
160145, 159ralrimi 3249 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โ†’ โˆ€๐‘ฅ โˆˆ {๐ธ} ยฌ ๐‘ฅ โˆˆ {๐‘—})
161 disj 4443 . . . . . . . . . . . . . . . . . . 19 (({๐ธ} โˆฉ {๐‘—}) = โˆ… โ†” โˆ€๐‘ฅ โˆˆ {๐ธ} ยฌ ๐‘ฅ โˆˆ {๐‘—})
162160, 161sylibr 233 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โ†’ ({๐ธ} โˆฉ {๐‘—}) = โˆ…)
163 disjdif2 4475 . . . . . . . . . . . . . . . . . 18 (({๐ธ} โˆฉ {๐‘—}) = โˆ… โ†’ ({๐ธ} โˆ– {๐‘—}) = {๐ธ})
164162, 163syl 17 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โ†’ ({๐ธ} โˆ– {๐‘—}) = {๐ธ})
165164uneq2d 4159 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โ†’ ((๐ท โˆ– {๐‘—}) โˆช ({๐ธ} โˆ– {๐‘—})) = ((๐ท โˆ– {๐‘—}) โˆช {๐ธ}))
166143, 165eqtrd 2767 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โ†’ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—}) = ((๐ท โˆ– {๐‘—}) โˆช {๐ธ}))
167166prodeq1d 15889 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ท) โ†’ โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด = โˆ๐‘– โˆˆ ((๐ท โˆ– {๐‘—}) โˆช {๐ธ})๐ด)
168167adantlr 714 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด = โˆ๐‘– โˆˆ ((๐ท โˆ– {๐‘—}) โˆช {๐ธ})๐ด)
169 nfv 1910 . . . . . . . . . . . . . . 15 โ„ฒ๐‘– ๐‘— โˆˆ ๐ท
1706, 169nfan 1895 . . . . . . . . . . . . . 14 โ„ฒ๐‘–((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท)
17199adantr 480 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ (๐ท โˆ– {๐‘—}) โˆˆ Fin)
17251adantr 480 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ ๐œ‘)
173172, 22syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ ๐ธ โˆˆ V)
174 id 22 . . . . . . . . . . . . . . . . . 18 (ยฌ ๐ธ โˆˆ ๐ท โ†’ ยฌ ๐ธ โˆˆ ๐ท)
175174intnanrd 489 . . . . . . . . . . . . . . . . . 18 (ยฌ ๐ธ โˆˆ ๐ท โ†’ ยฌ (๐ธ โˆˆ ๐ท โˆง ยฌ ๐ธ โˆˆ {๐‘—}))
176174, 175syl 17 . . . . . . . . . . . . . . . . 17 (ยฌ ๐ธ โˆˆ ๐ท โ†’ ยฌ (๐ธ โˆˆ ๐ท โˆง ยฌ ๐ธ โˆˆ {๐‘—}))
177 eldif 3954 . . . . . . . . . . . . . . . . 17 (๐ธ โˆˆ (๐ท โˆ– {๐‘—}) โ†” (๐ธ โˆˆ ๐ท โˆง ยฌ ๐ธ โˆˆ {๐‘—}))
178176, 177sylnibr 329 . . . . . . . . . . . . . . . 16 (ยฌ ๐ธ โˆˆ ๐ท โ†’ ยฌ ๐ธ โˆˆ (๐ท โˆ– {๐‘—}))
17933, 178syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ยฌ ๐ธ โˆˆ (๐ท โˆ– {๐‘—}))
180172, 179syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ ยฌ ๐ธ โˆˆ (๐ท โˆ– {๐‘—}))
181102adantlr 714 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โˆง ๐‘– โˆˆ (๐ท โˆ– {๐‘—})) โ†’ ๐ด โˆˆ โ„‚)
18280adantr 480 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ ๐น โˆˆ โ„‚)
183170, 7, 171, 173, 180, 181, 28, 182fprodsplitsn 15957 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ โˆ๐‘– โˆˆ ((๐ท โˆ– {๐‘—}) โˆช {๐ธ})๐ด = (โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด ยท ๐น))
184 eqidd 2728 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ (โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด ยท ๐น) = (โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด ยท ๐น))
185168, 183, 1843eqtrd 2771 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด = (โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด ยท ๐น))
186185oveq2d 7430 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด) = (๐ถ ยท (โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด ยท ๐น)))
18796, 104, 182mulassd 11259 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ ((๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น) = (๐ถ ยท (โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด ยท ๐น)))
188187eqcomd 2733 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ (๐ถ ยท (โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด ยท ๐น)) = ((๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น))
189186, 188eqtrd 2767 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โˆง ๐‘— โˆˆ ๐ท) โ†’ (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด) = ((๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น))
190189ex 412 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ (๐‘— โˆˆ ๐ท โ†’ (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด) = ((๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น)))
19195, 190ralrimi 3249 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ โˆ€๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด) = ((๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น))
192191sumeq2d 15672 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด) = ฮฃ๐‘— โˆˆ ๐ท ((๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น))
19395, 83, 80, 105fsummulc1f 44882 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ (ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น) = ฮฃ๐‘— โˆˆ ๐ท ((๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น))
194193eqcomd 2733 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ฮฃ๐‘— โˆˆ ๐ท ((๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น) = (ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น))
195 eqidd 2728 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ (ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น) = (ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น))
196192, 194, 1953eqtrd 2771 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด) = (ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น))
197106, 80mulcld 11256 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ (ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น) โˆˆ โ„‚)
198196, 197eqeltrd 2828 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด) โˆˆ โ„‚)
199198, 140addcomd 11438 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ (ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด) + (๐บ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด)) = ((๐บ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด) + ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด)))
20042oveq2d 7430 . . . . . 6 (๐œ‘ โ†’ (๐บ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด) = (๐บ ยท โˆ๐‘– โˆˆ ๐ท ๐ด))
201200adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ (๐บ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด) = (๐บ ยท โˆ๐‘– โˆˆ ๐ท ๐ด))
202201, 196oveq12d 7432 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ((๐บ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐ธ})๐ด) + ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด)) = ((๐บ ยท โˆ๐‘– โˆˆ ๐ท ๐ด) + (ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น)))
203141, 199, 2023eqtrrd 2772 . . 3 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ((๐บ ยท โˆ๐‘– โˆˆ ๐ท ๐ด) + (ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น)) = ฮฃ๐‘— โˆˆ (๐ท โˆช {๐ธ})(๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด))
2041, 203mpteq2da 5240 . 2 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ((๐บ ยท โˆ๐‘– โˆˆ ๐ท ๐ด) + (ฮฃ๐‘— โˆˆ ๐ท (๐ถ ยท โˆ๐‘– โˆˆ (๐ท โˆ– {๐‘—})๐ด) ยท ๐น))) = (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ฮฃ๐‘— โˆˆ (๐ท โˆช {๐ธ})(๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด)))
20547, 108, 2043eqtrd 2771 1 (๐œ‘ โ†’ (๐‘† D (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ โˆ๐‘– โˆˆ (๐ท โˆช {๐ธ})๐ด)) = (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ฮฃ๐‘— โˆˆ (๐ท โˆช {๐ธ})(๐ถ ยท โˆ๐‘– โˆˆ ((๐ท โˆช {๐ธ}) โˆ– {๐‘—})๐ด)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 395   โˆง w3a 1085   = wceq 1534  โ„ฒwnf 1778   โˆˆ wcel 2099  โ„ฒwnfc 2878  โˆ€wral 3056  Vcvv 3469   โˆ– cdif 3941   โˆช cun 3942   โˆฉ cin 3943   โІ wss 3944  โˆ…c0 4318  {csn 4624  {cpr 4626   โ†ฆ cmpt 5225  (class class class)co 7414  Fincfn 8955  โ„‚cc 11128  โ„cr 11129   + caddc 11133   ยท cmul 11135  ฮฃcsu 15656  โˆcprod 15873   D cdv 25779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208  ax-addf 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-fi 9426  df-sup 9457  df-inf 9458  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-z 12581  df-dec 12700  df-uz 12845  df-q 12955  df-rp 12999  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-icc 13355  df-fz 13509  df-fzo 13652  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-clim 15456  df-sum 15657  df-prod 15874  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-hom 17248  df-cco 17249  df-rest 17395  df-topn 17396  df-0g 17414  df-gsum 17415  df-topgen 17416  df-pt 17417  df-prds 17420  df-xrs 17475  df-qtop 17480  df-imas 17481  df-xps 17483  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-submnd 18732  df-mulg 19015  df-cntz 19259  df-cmn 19728  df-psmet 21258  df-xmet 21259  df-met 21260  df-bl 21261  df-mopn 21262  df-fbas 21263  df-fg 21264  df-cnfld 21267  df-top 22783  df-topon 22800  df-topsp 22822  df-bases 22836  df-cld 22910  df-ntr 22911  df-cls 22912  df-nei 22989  df-lp 23027  df-perf 23028  df-cn 23118  df-cnp 23119  df-haus 23206  df-tx 23453  df-hmeo 23646  df-fil 23737  df-fm 23829  df-flim 23830  df-flf 23831  df-xms 24213  df-ms 24214  df-tms 24215  df-cncf 24785  df-limc 25782  df-dv 25783
This theorem is referenced by:  dvmptfprod  45256
  Copyright terms: Public domain W3C validator