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

Theorem fprod2dlem 15868
Description: Lemma for fprod2d 15869- induction step. (Contributed by Scott Fenton, 30-Jan-2018.)
Hypotheses
Ref Expression
fprod2d.1 (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โ†’ ๐ท = ๐ถ)
fprod2d.2 (๐œ‘ โ†’ ๐ด โˆˆ Fin)
fprod2d.3 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐ต โˆˆ Fin)
fprod2d.4 ((๐œ‘ โˆง (๐‘— โˆˆ ๐ด โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ถ โˆˆ โ„‚)
fprod2d.5 (๐œ‘ โ†’ ยฌ ๐‘ฆ โˆˆ ๐‘ฅ)
fprod2d.6 (๐œ‘ โ†’ (๐‘ฅ โˆช {๐‘ฆ}) โŠ† ๐ด)
fprod2d.7 (๐œ“ โ†” โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท)
Assertion
Ref Expression
fprod2dlem ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)๐ท)
Distinct variable groups:   ๐ด,๐‘—,๐‘˜   ๐ต,๐‘˜,๐‘ง   ๐‘ง,๐ถ   ๐ท,๐‘—,๐‘˜   ๐œ‘,๐‘—   ๐‘ฅ,๐‘—   ๐‘ฆ,๐‘—,๐‘ง   ๐œ‘,๐‘˜   ๐‘ฅ,๐‘˜   ๐‘ฆ,๐‘˜,๐‘ง   ๐œ‘,๐‘ง   ๐‘ฅ,๐‘ง   ๐‘ฆ,๐‘ง
Allowed substitution hints:   ๐œ‘(๐‘ฅ,๐‘ฆ)   ๐œ“(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘—,๐‘˜)   ๐ด(๐‘ฅ,๐‘ฆ,๐‘ง)   ๐ต(๐‘ฅ,๐‘ฆ,๐‘—)   ๐ถ(๐‘ฅ,๐‘ฆ,๐‘—,๐‘˜)   ๐ท(๐‘ฅ,๐‘ฆ,๐‘ง)

Proof of Theorem fprod2dlem
Dummy variable ๐‘š is distinct from all other variables.
StepHypRef Expression
1 simpr 486 . . . 4 ((๐œ‘ โˆง ๐œ“) โ†’ ๐œ“)
2 fprod2d.7 . . . 4 (๐œ“ โ†” โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท)
31, 2sylib 217 . . 3 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท)
4 nfcv 2904 . . . . . 6 โ„ฒ๐‘šโˆ๐‘˜ โˆˆ ๐ต ๐ถ
5 nfcsb1v 3881 . . . . . . 7 โ„ฒ๐‘—โฆ‹๐‘š / ๐‘—โฆŒ๐ต
6 nfcsb1v 3881 . . . . . . 7 โ„ฒ๐‘—โฆ‹๐‘š / ๐‘—โฆŒ๐ถ
75, 6nfcprod 15799 . . . . . 6 โ„ฒ๐‘—โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ
8 csbeq1a 3870 . . . . . . 7 (๐‘— = ๐‘š โ†’ ๐ต = โฆ‹๐‘š / ๐‘—โฆŒ๐ต)
9 csbeq1a 3870 . . . . . . . 8 (๐‘— = ๐‘š โ†’ ๐ถ = โฆ‹๐‘š / ๐‘—โฆŒ๐ถ)
109adantr 482 . . . . . . 7 ((๐‘— = ๐‘š โˆง ๐‘˜ โˆˆ ๐ต) โ†’ ๐ถ = โฆ‹๐‘š / ๐‘—โฆŒ๐ถ)
118, 10prodeq12dv 15814 . . . . . 6 (๐‘— = ๐‘š โ†’ โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ)
124, 7, 11cbvprodi 15805 . . . . 5 โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘š โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ
13 fprod2d.6 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ฅ โˆช {๐‘ฆ}) โŠ† ๐ด)
1413unssbd 4149 . . . . . . . 8 (๐œ‘ โ†’ {๐‘ฆ} โŠ† ๐ด)
15 vex 3448 . . . . . . . . 9 ๐‘ฆ โˆˆ V
1615snss 4747 . . . . . . . 8 (๐‘ฆ โˆˆ ๐ด โ†” {๐‘ฆ} โŠ† ๐ด)
1714, 16sylibr 233 . . . . . . 7 (๐œ‘ โ†’ ๐‘ฆ โˆˆ ๐ด)
18 fprod2d.3 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐ต โˆˆ Fin)
1918ralrimiva 3140 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘— โˆˆ ๐ด ๐ต โˆˆ Fin)
20 nfcsb1v 3881 . . . . . . . . . . 11 โ„ฒ๐‘—โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต
2120nfel1 2920 . . . . . . . . . 10 โ„ฒ๐‘—โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin
22 csbeq1a 3870 . . . . . . . . . . 11 (๐‘— = ๐‘ฆ โ†’ ๐ต = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
2322eleq1d 2819 . . . . . . . . . 10 (๐‘— = ๐‘ฆ โ†’ (๐ต โˆˆ Fin โ†” โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin))
2421, 23rspc 3568 . . . . . . . . 9 (๐‘ฆ โˆˆ ๐ด โ†’ (โˆ€๐‘— โˆˆ ๐ด ๐ต โˆˆ Fin โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin))
2517, 19, 24sylc 65 . . . . . . . 8 (๐œ‘ โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin)
26 fprod2d.4 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘— โˆˆ ๐ด โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ถ โˆˆ โ„‚)
2726ralrimivva 3194 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ€๐‘— โˆˆ ๐ด โˆ€๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚)
28 nfcsb1v 3881 . . . . . . . . . . . . 13 โ„ฒ๐‘—โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
2928nfel1 2920 . . . . . . . . . . . 12 โ„ฒ๐‘—โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚
3020, 29nfralw 3293 . . . . . . . . . . 11 โ„ฒ๐‘—โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚
31 csbeq1a 3870 . . . . . . . . . . . . 13 (๐‘— = ๐‘ฆ โ†’ ๐ถ = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
3231eleq1d 2819 . . . . . . . . . . . 12 (๐‘— = ๐‘ฆ โ†’ (๐ถ โˆˆ โ„‚ โ†” โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
3322, 32raleqbidv 3318 . . . . . . . . . . 11 (๐‘— = ๐‘ฆ โ†’ (โˆ€๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚ โ†” โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
3430, 33rspc 3568 . . . . . . . . . 10 (๐‘ฆ โˆˆ ๐ด โ†’ (โˆ€๐‘— โˆˆ ๐ด โˆ€๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚ โ†’ โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
3517, 27, 34sylc 65 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚)
3635r19.21bi 3233 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚)
3725, 36fprodcl 15840 . . . . . . 7 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚)
38 csbeq1 3859 . . . . . . . . 9 (๐‘š = ๐‘ฆ โ†’ โฆ‹๐‘š / ๐‘—โฆŒ๐ต = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
39 csbeq1 3859 . . . . . . . . . 10 (๐‘š = ๐‘ฆ โ†’ โฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4039adantr 482 . . . . . . . . 9 ((๐‘š = ๐‘ฆ โˆง ๐‘˜ โˆˆ โฆ‹๐‘š / ๐‘—โฆŒ๐ต) โ†’ โฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4138, 40prodeq12dv 15814 . . . . . . . 8 (๐‘š = ๐‘ฆ โ†’ โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4241prodsn 15850 . . . . . . 7 ((๐‘ฆ โˆˆ ๐ด โˆง โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚) โ†’ โˆ๐‘š โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4317, 37, 42syl2anc 585 . . . . . 6 (๐œ‘ โ†’ โˆ๐‘š โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
44 nfcv 2904 . . . . . . . 8 โ„ฒ๐‘šโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
45 nfcsb1v 3881 . . . . . . . 8 โ„ฒ๐‘˜โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
46 csbeq1a 3870 . . . . . . . 8 (๐‘˜ = ๐‘š โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4744, 45, 46cbvprodi 15805 . . . . . . 7 โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โˆ๐‘š โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
48 csbeq1 3859 . . . . . . . . 9 (๐‘š = (2nd โ€˜๐‘ง) โ†’ โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
49 snfi 8991 . . . . . . . . . 10 {๐‘ฆ} โˆˆ Fin
50 xpfi 9264 . . . . . . . . . 10 (({๐‘ฆ} โˆˆ Fin โˆง โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin) โ†’ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โˆˆ Fin)
5149, 25, 50sylancr 588 . . . . . . . . 9 (๐œ‘ โ†’ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โˆˆ Fin)
52 2ndconst 8034 . . . . . . . . . 10 (๐‘ฆ โˆˆ ๐ด โ†’ (2nd โ†พ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)):({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)โ€“1-1-ontoโ†’โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
5317, 52syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (2nd โ†พ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)):({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)โ€“1-1-ontoโ†’โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
54 fvres 6862 . . . . . . . . . 10 (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ ((2nd โ†พ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))โ€˜๐‘ง) = (2nd โ€˜๐‘ง))
5554adantl 483 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ ((2nd โ†พ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))โ€˜๐‘ง) = (2nd โ€˜๐‘ง))
5645nfel1 2920 . . . . . . . . . . 11 โ„ฒ๐‘˜โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚
5746eleq1d 2819 . . . . . . . . . . 11 (๐‘˜ = ๐‘š โ†’ (โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚ โ†” โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
5856, 57rspc 3568 . . . . . . . . . 10 (๐‘š โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โ†’ (โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚ โ†’ โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
5935, 58mpan9 508 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚)
6048, 51, 53, 55, 59fprodf1o 15834 . . . . . . . 8 (๐œ‘ โ†’ โˆ๐‘š โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
61 elxp 5657 . . . . . . . . . . . 12 (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†” โˆƒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)))
62 nfv 1918 . . . . . . . . . . . . . . 15 โ„ฒ๐‘— ๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ
63 nfv 1918 . . . . . . . . . . . . . . . 16 โ„ฒ๐‘— ๐‘š โˆˆ {๐‘ฆ}
6420nfcri 2891 . . . . . . . . . . . . . . . 16 โ„ฒ๐‘— ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต
6563, 64nfan 1903 . . . . . . . . . . . . . . 15 โ„ฒ๐‘—(๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
6662, 65nfan 1903 . . . . . . . . . . . . . 14 โ„ฒ๐‘—(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
6766nfex 2318 . . . . . . . . . . . . 13 โ„ฒ๐‘—โˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
68 nfv 1918 . . . . . . . . . . . . 13 โ„ฒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต))
69 opeq1 4831 . . . . . . . . . . . . . . . 16 (๐‘š = ๐‘— โ†’ โŸจ๐‘š, ๐‘˜โŸฉ = โŸจ๐‘—, ๐‘˜โŸฉ)
7069eqeq2d 2744 . . . . . . . . . . . . . . 15 (๐‘š = ๐‘— โ†’ (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โ†” ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ))
71 eleq1w 2817 . . . . . . . . . . . . . . . . . 18 (๐‘š = ๐‘— โ†’ (๐‘š โˆˆ {๐‘ฆ} โ†” ๐‘— โˆˆ {๐‘ฆ}))
72 velsn 4603 . . . . . . . . . . . . . . . . . 18 (๐‘— โˆˆ {๐‘ฆ} โ†” ๐‘— = ๐‘ฆ)
7371, 72bitrdi 287 . . . . . . . . . . . . . . . . 17 (๐‘š = ๐‘— โ†’ (๐‘š โˆˆ {๐‘ฆ} โ†” ๐‘— = ๐‘ฆ))
7473anbi1d 631 . . . . . . . . . . . . . . . 16 (๐‘š = ๐‘— โ†’ ((๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†” (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)))
7522eleq2d 2820 . . . . . . . . . . . . . . . . 17 (๐‘— = ๐‘ฆ โ†’ (๐‘˜ โˆˆ ๐ต โ†” ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
7675pm5.32i 576 . . . . . . . . . . . . . . . 16 ((๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต) โ†” (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
7774, 76bitr4di 289 . . . . . . . . . . . . . . 15 (๐‘š = ๐‘— โ†’ ((๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†” (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)))
7870, 77anbi12d 632 . . . . . . . . . . . . . 14 (๐‘š = ๐‘— โ†’ ((๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†” (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต))))
7978exbidv 1925 . . . . . . . . . . . . 13 (๐‘š = ๐‘— โ†’ (โˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†” โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต))))
8067, 68, 79cbvexv1 2339 . . . . . . . . . . . 12 (โˆƒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†” โˆƒ๐‘—โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)))
8161, 80bitri 275 . . . . . . . . . . 11 (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†” โˆƒ๐‘—โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)))
82 nfv 1918 . . . . . . . . . . . 12 โ„ฒ๐‘—๐œ‘
83 nfcv 2904 . . . . . . . . . . . . . 14 โ„ฒ๐‘—(2nd โ€˜๐‘ง)
8483, 28nfcsbw 3883 . . . . . . . . . . . . 13 โ„ฒ๐‘—โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
8584nfeq2 2921 . . . . . . . . . . . 12 โ„ฒ๐‘— ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
86 nfv 1918 . . . . . . . . . . . . 13 โ„ฒ๐‘˜๐œ‘
87 nfcsb1v 3881 . . . . . . . . . . . . . 14 โ„ฒ๐‘˜โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
8887nfeq2 2921 . . . . . . . . . . . . 13 โ„ฒ๐‘˜ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
89 fprod2d.1 . . . . . . . . . . . . . . . 16 (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โ†’ ๐ท = ๐ถ)
9089ad2antlr 726 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = ๐ถ)
9131ad2antrl 727 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ถ = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
92 fveq2 6843 . . . . . . . . . . . . . . . . . 18 (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โ†’ (2nd โ€˜๐‘ง) = (2nd โ€˜โŸจ๐‘—, ๐‘˜โŸฉ))
93 vex 3448 . . . . . . . . . . . . . . . . . . 19 ๐‘— โˆˆ V
94 vex 3448 . . . . . . . . . . . . . . . . . . 19 ๐‘˜ โˆˆ V
9593, 94op2nd 7931 . . . . . . . . . . . . . . . . . 18 (2nd โ€˜โŸจ๐‘—, ๐‘˜โŸฉ) = ๐‘˜
9692, 95eqtr2di 2790 . . . . . . . . . . . . . . . . 17 (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โ†’ ๐‘˜ = (2nd โ€˜๐‘ง))
9796ad2antlr 726 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐‘˜ = (2nd โ€˜๐‘ง))
98 csbeq1a 3870 . . . . . . . . . . . . . . . 16 (๐‘˜ = (2nd โ€˜๐‘ง) โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
9997, 98syl 17 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
10090, 91, 993eqtrd 2777 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
101100expl 459 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ))
10286, 88, 101exlimd 2212 . . . . . . . . . . . 12 (๐œ‘ โ†’ (โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ))
10382, 85, 102exlimd 2212 . . . . . . . . . . 11 (๐œ‘ โ†’ (โˆƒ๐‘—โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ))
10481, 103biimtrid 241 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ))
105104imp 408 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
106105prodeq2dv 15811 . . . . . . . 8 (๐œ‘ โ†’ โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
10760, 106eqtr4d 2776 . . . . . . 7 (๐œ‘ โ†’ โˆ๐‘š โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
10847, 107eqtrid 2785 . . . . . 6 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
10943, 108eqtrd 2773 . . . . 5 (๐œ‘ โ†’ โˆ๐‘š โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
11012, 109eqtrid 2785 . . . 4 (๐œ‘ โ†’ โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
111110adantr 482 . . 3 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
1123, 111oveq12d 7376 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ (โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ ยท โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ) = (โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท ยท โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท))
113 fprod2d.5 . . . . 5 (๐œ‘ โ†’ ยฌ ๐‘ฆ โˆˆ ๐‘ฅ)
114 disjsn 4673 . . . . 5 ((๐‘ฅ โˆฉ {๐‘ฆ}) = โˆ… โ†” ยฌ ๐‘ฆ โˆˆ ๐‘ฅ)
115113, 114sylibr 233 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆฉ {๐‘ฆ}) = โˆ…)
116 eqidd 2734 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆช {๐‘ฆ}) = (๐‘ฅ โˆช {๐‘ฆ}))
117 fprod2d.2 . . . . 5 (๐œ‘ โ†’ ๐ด โˆˆ Fin)
118117, 13ssfid 9214 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆช {๐‘ฆ}) โˆˆ Fin)
11913sselda 3945 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ ๐‘— โˆˆ ๐ด)
12026anassrs 469 . . . . . 6 (((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โˆง ๐‘˜ โˆˆ ๐ต) โ†’ ๐ถ โˆˆ โ„‚)
12118, 120fprodcl 15840 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ โˆ๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚)
122119, 121syldan 592 . . . 4 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ โˆ๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚)
123115, 116, 118, 122fprodsplit 15854 . . 3 (๐œ‘ โ†’ โˆ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})โˆ๐‘˜ โˆˆ ๐ต ๐ถ = (โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ ยท โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ))
124123adantr 482 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})โˆ๐‘˜ โˆˆ ๐ต ๐ถ = (โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ ยท โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ))
125 eliun 4959 . . . . . . . . . 10 (๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โ†” โˆƒ๐‘— โˆˆ ๐‘ฅ ๐‘ง โˆˆ ({๐‘—} ร— ๐ต))
126 xp1st 7954 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ (1st โ€˜๐‘ง) โˆˆ {๐‘—})
127 elsni 4604 . . . . . . . . . . . . . 14 ((1st โ€˜๐‘ง) โˆˆ {๐‘—} โ†’ (1st โ€˜๐‘ง) = ๐‘—)
128126, 127syl 17 . . . . . . . . . . . . 13 (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ (1st โ€˜๐‘ง) = ๐‘—)
129128eleq1d 2819 . . . . . . . . . . . 12 (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ ((1st โ€˜๐‘ง) โˆˆ ๐‘ฅ โ†” ๐‘— โˆˆ ๐‘ฅ))
130129biimparc 481 . . . . . . . . . . 11 ((๐‘— โˆˆ ๐‘ฅ โˆง ๐‘ง โˆˆ ({๐‘—} ร— ๐ต)) โ†’ (1st โ€˜๐‘ง) โˆˆ ๐‘ฅ)
131130rexlimiva 3141 . . . . . . . . . 10 (โˆƒ๐‘— โˆˆ ๐‘ฅ ๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ (1st โ€˜๐‘ง) โˆˆ ๐‘ฅ)
132125, 131sylbi 216 . . . . . . . . 9 (๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โ†’ (1st โ€˜๐‘ง) โˆˆ ๐‘ฅ)
133 xp1st 7954 . . . . . . . . 9 (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ (1st โ€˜๐‘ง) โˆˆ {๐‘ฆ})
134132, 133anim12i 614 . . . . . . . 8 ((๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆง ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ ((1st โ€˜๐‘ง) โˆˆ ๐‘ฅ โˆง (1st โ€˜๐‘ง) โˆˆ {๐‘ฆ}))
135 elin 3927 . . . . . . . 8 (๐‘ง โˆˆ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†” (๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆง ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)))
136 elin 3927 . . . . . . . 8 ((1st โ€˜๐‘ง) โˆˆ (๐‘ฅ โˆฉ {๐‘ฆ}) โ†” ((1st โ€˜๐‘ง) โˆˆ ๐‘ฅ โˆง (1st โ€˜๐‘ง) โˆˆ {๐‘ฆ}))
137134, 135, 1363imtr4i 292 . . . . . . 7 (๐‘ง โˆˆ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ (1st โ€˜๐‘ง) โˆˆ (๐‘ฅ โˆฉ {๐‘ฆ}))
138115eleq2d 2820 . . . . . . . 8 (๐œ‘ โ†’ ((1st โ€˜๐‘ง) โˆˆ (๐‘ฅ โˆฉ {๐‘ฆ}) โ†” (1st โ€˜๐‘ง) โˆˆ โˆ…))
139 noel 4291 . . . . . . . . 9 ยฌ (1st โ€˜๐‘ง) โˆˆ โˆ…
140139pm2.21i 119 . . . . . . . 8 ((1st โ€˜๐‘ง) โˆˆ โˆ… โ†’ ๐‘ง โˆˆ โˆ…)
141138, 140syl6bi 253 . . . . . . 7 (๐œ‘ โ†’ ((1st โ€˜๐‘ง) โˆˆ (๐‘ฅ โˆฉ {๐‘ฆ}) โ†’ ๐‘ง โˆˆ โˆ…))
142137, 141syl5 34 . . . . . 6 (๐œ‘ โ†’ (๐‘ง โˆˆ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ ๐‘ง โˆˆ โˆ…))
143142ssrdv 3951 . . . . 5 (๐œ‘ โ†’ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โŠ† โˆ…)
144 ss0 4359 . . . . 5 ((โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โŠ† โˆ… โ†’ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) = โˆ…)
145143, 144syl 17 . . . 4 (๐œ‘ โ†’ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) = โˆ…)
146 iunxun 5055 . . . . . 6 โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) = (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช โˆช ๐‘— โˆˆ {๐‘ฆ} ({๐‘—} ร— ๐ต))
147 nfcv 2904 . . . . . . . . 9 โ„ฒ๐‘š({๐‘—} ร— ๐ต)
148 nfcv 2904 . . . . . . . . . 10 โ„ฒ๐‘—{๐‘š}
149148, 5nfxp 5667 . . . . . . . . 9 โ„ฒ๐‘—({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต)
150 sneq 4597 . . . . . . . . . 10 (๐‘— = ๐‘š โ†’ {๐‘—} = {๐‘š})
151150, 8xpeq12d 5665 . . . . . . . . 9 (๐‘— = ๐‘š โ†’ ({๐‘—} ร— ๐ต) = ({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต))
152147, 149, 151cbviun 4997 . . . . . . . 8 โˆช ๐‘— โˆˆ {๐‘ฆ} ({๐‘—} ร— ๐ต) = โˆช ๐‘š โˆˆ {๐‘ฆ} ({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต)
153 sneq 4597 . . . . . . . . . 10 (๐‘š = ๐‘ฆ โ†’ {๐‘š} = {๐‘ฆ})
154153, 38xpeq12d 5665 . . . . . . . . 9 (๐‘š = ๐‘ฆ โ†’ ({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต) = ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
15515, 154iunxsn 5052 . . . . . . . 8 โˆช ๐‘š โˆˆ {๐‘ฆ} ({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต) = ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
156152, 155eqtri 2761 . . . . . . 7 โˆช ๐‘— โˆˆ {๐‘ฆ} ({๐‘—} ร— ๐ต) = ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
157156uneq2i 4121 . . . . . 6 (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช โˆช ๐‘— โˆˆ {๐‘ฆ} ({๐‘—} ร— ๐ต)) = (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
158146, 157eqtri 2761 . . . . 5 โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) = (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
159158a1i 11 . . . 4 (๐œ‘ โ†’ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) = (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)))
160 snfi 8991 . . . . . . 7 {๐‘—} โˆˆ Fin
161119, 18syldan 592 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ ๐ต โˆˆ Fin)
162 xpfi 9264 . . . . . . 7 (({๐‘—} โˆˆ Fin โˆง ๐ต โˆˆ Fin) โ†’ ({๐‘—} ร— ๐ต) โˆˆ Fin)
163160, 161, 162sylancr 588 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ ({๐‘—} ร— ๐ต) โˆˆ Fin)
164163ralrimiva 3140 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โˆˆ Fin)
165 iunfi 9287 . . . . 5 (((๐‘ฅ โˆช {๐‘ฆ}) โˆˆ Fin โˆง โˆ€๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โˆˆ Fin) โ†’ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โˆˆ Fin)
166118, 164, 165syl2anc 585 . . . 4 (๐œ‘ โ†’ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โˆˆ Fin)
167 eliun 4959 . . . . . 6 (๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โ†” โˆƒ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})๐‘ง โˆˆ ({๐‘—} ร— ๐ต))
168 elxp 5657 . . . . . . . 8 (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†” โˆƒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต)))
169 simprl 770 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ)
170 simprrl 780 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘š โˆˆ {๐‘—})
171 elsni 4604 . . . . . . . . . . . . . . 15 (๐‘š โˆˆ {๐‘—} โ†’ ๐‘š = ๐‘—)
172170, 171syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘š = ๐‘—)
173172opeq1d 4837 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ โŸจ๐‘š, ๐‘˜โŸฉ = โŸจ๐‘—, ๐‘˜โŸฉ)
174169, 173eqtrd 2773 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ)
175174, 89syl 17 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐ท = ๐ถ)
176 simpll 766 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐œ‘)
177119adantr 482 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘— โˆˆ ๐ด)
178 simprrr 781 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘˜ โˆˆ ๐ต)
179176, 177, 178, 26syl12anc 836 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐ถ โˆˆ โ„‚)
180175, 179eqeltrd 2834 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐ท โˆˆ โ„‚)
181180ex 414 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ ((๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท โˆˆ โ„‚))
182181exlimdvv 1938 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ (โˆƒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท โˆˆ โ„‚))
183168, 182biimtrid 241 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ ๐ท โˆˆ โ„‚))
184183rexlimdva 3149 . . . . . 6 (๐œ‘ โ†’ (โˆƒ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ ๐ท โˆˆ โ„‚))
185167, 184biimtrid 241 . . . . 5 (๐œ‘ โ†’ (๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โ†’ ๐ท โˆˆ โ„‚))
186185imp 408 . . . 4 ((๐œ‘ โˆง ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)) โ†’ ๐ท โˆˆ โ„‚)
187145, 159, 166, 186fprodsplit 15854 . . 3 (๐œ‘ โ†’ โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)๐ท = (โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท ยท โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท))
188187adantr 482 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)๐ท = (โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท ยท โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท))
189112, 124, 1883eqtr4d 2783 1 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)๐ท)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542  โˆƒwex 1782   โˆˆ wcel 2107  โˆ€wral 3061  โˆƒwrex 3070  โฆ‹csb 3856   โˆช cun 3909   โˆฉ cin 3910   โŠ† wss 3911  โˆ…c0 4283  {csn 4587  โŸจcop 4593  โˆช ciun 4955   ร— cxp 5632   โ†พ cres 5636  โ€“1-1-ontoโ†’wf1o 6496  โ€˜cfv 6497  (class class class)co 7358  1st c1st 7920  2nd c2nd 7921  Fincfn 8886  โ„‚cc 11054   ยท cmul 11061  โˆcprod 15793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-er 8651  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-sup 9383  df-oi 9451  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-n0 12419  df-z 12505  df-uz 12769  df-rp 12921  df-fz 13431  df-fzo 13574  df-seq 13913  df-exp 13974  df-hash 14237  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-clim 15376  df-prod 15794
This theorem is referenced by:  fprod2d  15869
  Copyright terms: Public domain W3C validator