Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mzpcompact2lem Structured version   Visualization version   GIF version

Theorem mzpcompact2lem 40768
Description: Lemma for mzpcompact2 40769. (Contributed by Stefan O'Rear, 9-Oct-2014.)
Hypothesis
Ref Expression
mzpcompact2lem.i ๐ต โˆˆ V
Assertion
Ref Expression
mzpcompact2lem (๐ด โˆˆ (mzPolyโ€˜๐ต) โ†’ โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐ด = (๐‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘ โ†พ ๐‘Ž)))))
Distinct variable groups:   ๐ด,๐‘Ž,๐‘   ๐ต,๐‘Ž,๐‘,๐‘
Allowed substitution hint:   ๐ด(๐‘)

Proof of Theorem mzpcompact2lem
Dummy variables ๐‘‘ ๐‘’ ๐‘“ ๐‘” โ„Ž ๐‘– ๐‘— ๐‘˜ ๐‘™ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tru 1543 . . 3 โŠค
2 0fin 8992 . . . . . 6 โˆ… โˆˆ Fin
3 0ex 5240 . . . . . . . 8 โˆ… โˆˆ V
4 mzpconst 40752 . . . . . . . 8 ((โˆ… โˆˆ V โˆง ๐‘“ โˆˆ โ„ค) โ†’ ((โ„ค โ†‘m โˆ…) ร— {๐‘“}) โˆˆ (mzPolyโ€˜โˆ…))
53, 4mpan 688 . . . . . . 7 (๐‘“ โˆˆ โ„ค โ†’ ((โ„ค โ†‘m โˆ…) ร— {๐‘“}) โˆˆ (mzPolyโ€˜โˆ…))
6 0ss 4336 . . . . . . . 8 โˆ… โŠ† ๐ต
76a1i 11 . . . . . . 7 (๐‘“ โˆˆ โ„ค โ†’ โˆ… โŠ† ๐ต)
8 fconstmpt 5660 . . . . . . . 8 ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ๐‘“)
9 simpr 486 . . . . . . . . . . 11 ((๐‘“ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต))
10 elmapssres 8686 . . . . . . . . . . 11 ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โˆง โˆ… โŠ† ๐ต) โ†’ (๐‘‘ โ†พ โˆ…) โˆˆ (โ„ค โ†‘m โˆ…))
119, 6, 10sylancl 587 . . . . . . . . . 10 ((๐‘“ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ (๐‘‘ โ†พ โˆ…) โˆˆ (โ„ค โ†‘m โˆ…))
12 vex 3441 . . . . . . . . . . 11 ๐‘“ โˆˆ V
1312fvconst2 7111 . . . . . . . . . 10 ((๐‘‘ โ†พ โˆ…) โˆˆ (โ„ค โ†‘m โˆ…) โ†’ (((โ„ค โ†‘m โˆ…) ร— {๐‘“})โ€˜(๐‘‘ โ†พ โˆ…)) = ๐‘“)
1411, 13syl 17 . . . . . . . . 9 ((๐‘“ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ (((โ„ค โ†‘m โˆ…) ร— {๐‘“})โ€˜(๐‘‘ โ†พ โˆ…)) = ๐‘“)
1514mpteq2dva 5181 . . . . . . . 8 (๐‘“ โˆˆ โ„ค โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (((โ„ค โ†‘m โˆ…) ร— {๐‘“})โ€˜(๐‘‘ โ†พ โˆ…))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ๐‘“))
168, 15eqtr4id 2795 . . . . . . 7 (๐‘“ โˆˆ โ„ค โ†’ ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (((โ„ค โ†‘m โˆ…) ร— {๐‘“})โ€˜(๐‘‘ โ†พ โˆ…))))
17 fveq1 6803 . . . . . . . . . . 11 (๐‘ = ((โ„ค โ†‘m โˆ…) ร— {๐‘“}) โ†’ (๐‘โ€˜(๐‘‘ โ†พ โˆ…)) = (((โ„ค โ†‘m โˆ…) ร— {๐‘“})โ€˜(๐‘‘ โ†พ โˆ…)))
1817mpteq2dv 5183 . . . . . . . . . 10 (๐‘ = ((โ„ค โ†‘m โˆ…) ร— {๐‘“}) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โˆ…))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (((โ„ค โ†‘m โˆ…) ร— {๐‘“})โ€˜(๐‘‘ โ†พ โˆ…))))
1918eqeq2d 2747 . . . . . . . . 9 (๐‘ = ((โ„ค โ†‘m โˆ…) ร— {๐‘“}) โ†’ (((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โˆ…))) โ†” ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (((โ„ค โ†‘m โˆ…) ร— {๐‘“})โ€˜(๐‘‘ โ†พ โˆ…)))))
2019anbi2d 630 . . . . . . . 8 (๐‘ = ((โ„ค โ†‘m โˆ…) ร— {๐‘“}) โ†’ ((โˆ… โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โˆ…)))) โ†” (โˆ… โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (((โ„ค โ†‘m โˆ…) ร— {๐‘“})โ€˜(๐‘‘ โ†พ โˆ…))))))
2120rspcev 3566 . . . . . . 7 ((((โ„ค โ†‘m โˆ…) ร— {๐‘“}) โˆˆ (mzPolyโ€˜โˆ…) โˆง (โˆ… โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (((โ„ค โ†‘m โˆ…) ร— {๐‘“})โ€˜(๐‘‘ โ†พ โˆ…))))) โ†’ โˆƒ๐‘ โˆˆ (mzPolyโ€˜โˆ…)(โˆ… โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โˆ…)))))
225, 7, 16, 21syl12anc 835 . . . . . 6 (๐‘“ โˆˆ โ„ค โ†’ โˆƒ๐‘ โˆˆ (mzPolyโ€˜โˆ…)(โˆ… โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โˆ…)))))
23 fveq2 6804 . . . . . . . 8 (๐‘Ž = โˆ… โ†’ (mzPolyโ€˜๐‘Ž) = (mzPolyโ€˜โˆ…))
24 sseq1 3951 . . . . . . . . 9 (๐‘Ž = โˆ… โ†’ (๐‘Ž โŠ† ๐ต โ†” โˆ… โŠ† ๐ต))
25 reseq2 5898 . . . . . . . . . . . 12 (๐‘Ž = โˆ… โ†’ (๐‘‘ โ†พ ๐‘Ž) = (๐‘‘ โ†พ โˆ…))
2625fveq2d 6808 . . . . . . . . . . 11 (๐‘Ž = โˆ… โ†’ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)) = (๐‘โ€˜(๐‘‘ โ†พ โˆ…)))
2726mpteq2dv 5183 . . . . . . . . . 10 (๐‘Ž = โˆ… โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โˆ…))))
2827eqeq2d 2747 . . . . . . . . 9 (๐‘Ž = โˆ… โ†’ (((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โˆ…)))))
2924, 28anbi12d 632 . . . . . . . 8 (๐‘Ž = โˆ… โ†’ ((๐‘Ž โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (โˆ… โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โˆ…))))))
3023, 29rexeqbidv 3356 . . . . . . 7 (๐‘Ž = โˆ… โ†’ (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘ โˆˆ (mzPolyโ€˜โˆ…)(โˆ… โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โˆ…))))))
3130rspcev 3566 . . . . . 6 ((โˆ… โˆˆ Fin โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜โˆ…)(โˆ… โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โˆ…))))) โ†’ โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
322, 22, 31sylancr 588 . . . . 5 (๐‘“ โˆˆ โ„ค โ†’ โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
3332adantl 483 . . . 4 ((โŠค โˆง ๐‘“ โˆˆ โ„ค) โ†’ โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
34 snfi 8869 . . . . . 6 {๐‘“} โˆˆ Fin
35 snex 5363 . . . . . . . . 9 {๐‘“} โˆˆ V
36 vsnid 4602 . . . . . . . . 9 ๐‘“ โˆˆ {๐‘“}
37 mzpproj 40754 . . . . . . . . 9 (({๐‘“} โˆˆ V โˆง ๐‘“ โˆˆ {๐‘“}) โ†’ (๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“)) โˆˆ (mzPolyโ€˜{๐‘“}))
3835, 36, 37mp2an 690 . . . . . . . 8 (๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“)) โˆˆ (mzPolyโ€˜{๐‘“})
3938a1i 11 . . . . . . 7 (๐‘“ โˆˆ ๐ต โ†’ (๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“)) โˆˆ (mzPolyโ€˜{๐‘“}))
40 snssi 4747 . . . . . . 7 (๐‘“ โˆˆ ๐ต โ†’ {๐‘“} โŠ† ๐ต)
41 fveq1 6803 . . . . . . . . 9 (๐‘” = ๐‘‘ โ†’ (๐‘”โ€˜๐‘“) = (๐‘‘โ€˜๐‘“))
4241cbvmptv 5194 . . . . . . . 8 (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘‘โ€˜๐‘“))
43 simpr 486 . . . . . . . . . . . 12 ((๐‘“ โˆˆ ๐ต โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต))
44 simpl 484 . . . . . . . . . . . . 13 ((๐‘“ โˆˆ ๐ต โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ ๐‘“ โˆˆ ๐ต)
4544snssd 4748 . . . . . . . . . . . 12 ((๐‘“ โˆˆ ๐ต โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ {๐‘“} โŠ† ๐ต)
46 elmapssres 8686 . . . . . . . . . . . 12 ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โˆง {๐‘“} โŠ† ๐ต) โ†’ (๐‘‘ โ†พ {๐‘“}) โˆˆ (โ„ค โ†‘m {๐‘“}))
4743, 45, 46syl2anc 585 . . . . . . . . . . 11 ((๐‘“ โˆˆ ๐ต โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ (๐‘‘ โ†พ {๐‘“}) โˆˆ (โ„ค โ†‘m {๐‘“}))
48 fveq1 6803 . . . . . . . . . . . 12 (๐‘” = (๐‘‘ โ†พ {๐‘“}) โ†’ (๐‘”โ€˜๐‘“) = ((๐‘‘ โ†พ {๐‘“})โ€˜๐‘“))
49 eqid 2736 . . . . . . . . . . . 12 (๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“))
50 fvex 6817 . . . . . . . . . . . 12 ((๐‘‘ โ†พ {๐‘“})โ€˜๐‘“) โˆˆ V
5148, 49, 50fvmpt 6907 . . . . . . . . . . 11 ((๐‘‘ โ†พ {๐‘“}) โˆˆ (โ„ค โ†‘m {๐‘“}) โ†’ ((๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“))โ€˜(๐‘‘ โ†พ {๐‘“})) = ((๐‘‘ โ†พ {๐‘“})โ€˜๐‘“))
5247, 51syl 17 . . . . . . . . . 10 ((๐‘“ โˆˆ ๐ต โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ ((๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“))โ€˜(๐‘‘ โ†พ {๐‘“})) = ((๐‘‘ โ†พ {๐‘“})โ€˜๐‘“))
53 fvres 6823 . . . . . . . . . . 11 (๐‘“ โˆˆ {๐‘“} โ†’ ((๐‘‘ โ†พ {๐‘“})โ€˜๐‘“) = (๐‘‘โ€˜๐‘“))
5436, 53ax-mp 5 . . . . . . . . . 10 ((๐‘‘ โ†พ {๐‘“})โ€˜๐‘“) = (๐‘‘โ€˜๐‘“)
5552, 54eqtr2di 2793 . . . . . . . . 9 ((๐‘“ โˆˆ ๐ต โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ (๐‘‘โ€˜๐‘“) = ((๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“))โ€˜(๐‘‘ โ†พ {๐‘“})))
5655mpteq2dva 5181 . . . . . . . 8 (๐‘“ โˆˆ ๐ต โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘‘โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“))โ€˜(๐‘‘ โ†พ {๐‘“}))))
5742, 56eqtrid 2788 . . . . . . 7 (๐‘“ โˆˆ ๐ต โ†’ (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“))โ€˜(๐‘‘ โ†พ {๐‘“}))))
58 fveq1 6803 . . . . . . . . . . 11 (๐‘ = (๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“)) โ†’ (๐‘โ€˜(๐‘‘ โ†พ {๐‘“})) = ((๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“))โ€˜(๐‘‘ โ†พ {๐‘“})))
5958mpteq2dv 5183 . . . . . . . . . 10 (๐‘ = (๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“)) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ {๐‘“}))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“))โ€˜(๐‘‘ โ†พ {๐‘“}))))
6059eqeq2d 2747 . . . . . . . . 9 (๐‘ = (๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“)) โ†’ ((๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ {๐‘“}))) โ†” (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“))โ€˜(๐‘‘ โ†พ {๐‘“})))))
6160anbi2d 630 . . . . . . . 8 (๐‘ = (๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“)) โ†’ (({๐‘“} โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ {๐‘“})))) โ†” ({๐‘“} โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“))โ€˜(๐‘‘ โ†พ {๐‘“}))))))
6261rspcev 3566 . . . . . . 7 (((๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“)) โˆˆ (mzPolyโ€˜{๐‘“}) โˆง ({๐‘“} โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘” โˆˆ (โ„ค โ†‘m {๐‘“}) โ†ฆ (๐‘”โ€˜๐‘“))โ€˜(๐‘‘ โ†พ {๐‘“}))))) โ†’ โˆƒ๐‘ โˆˆ (mzPolyโ€˜{๐‘“})({๐‘“} โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ {๐‘“})))))
6339, 40, 57, 62syl12anc 835 . . . . . 6 (๐‘“ โˆˆ ๐ต โ†’ โˆƒ๐‘ โˆˆ (mzPolyโ€˜{๐‘“})({๐‘“} โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ {๐‘“})))))
64 fveq2 6804 . . . . . . . 8 (๐‘Ž = {๐‘“} โ†’ (mzPolyโ€˜๐‘Ž) = (mzPolyโ€˜{๐‘“}))
65 sseq1 3951 . . . . . . . . 9 (๐‘Ž = {๐‘“} โ†’ (๐‘Ž โŠ† ๐ต โ†” {๐‘“} โŠ† ๐ต))
66 reseq2 5898 . . . . . . . . . . . 12 (๐‘Ž = {๐‘“} โ†’ (๐‘‘ โ†พ ๐‘Ž) = (๐‘‘ โ†พ {๐‘“}))
6766fveq2d 6808 . . . . . . . . . . 11 (๐‘Ž = {๐‘“} โ†’ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)) = (๐‘โ€˜(๐‘‘ โ†พ {๐‘“})))
6867mpteq2dv 5183 . . . . . . . . . 10 (๐‘Ž = {๐‘“} โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ {๐‘“}))))
6968eqeq2d 2747 . . . . . . . . 9 (๐‘Ž = {๐‘“} โ†’ ((๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ {๐‘“})))))
7065, 69anbi12d 632 . . . . . . . 8 (๐‘Ž = {๐‘“} โ†’ ((๐‘Ž โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” ({๐‘“} โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ {๐‘“}))))))
7164, 70rexeqbidv 3356 . . . . . . 7 (๐‘Ž = {๐‘“} โ†’ (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘ โˆˆ (mzPolyโ€˜{๐‘“})({๐‘“} โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ {๐‘“}))))))
7271rspcev 3566 . . . . . 6 (({๐‘“} โˆˆ Fin โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜{๐‘“})({๐‘“} โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ {๐‘“}))))) โ†’ โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
7334, 63, 72sylancr 588 . . . . 5 (๐‘“ โˆˆ ๐ต โ†’ โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
7473adantl 483 . . . 4 ((โŠค โˆง ๐‘“ โˆˆ ๐ต) โ†’ โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
75 simplll 773 . . . . . . . . . . . . . . . . . 18 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ โ„Ž โˆˆ Fin)
76 simprll 777 . . . . . . . . . . . . . . . . . 18 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ ๐‘— โˆˆ Fin)
77 unfi 8993 . . . . . . . . . . . . . . . . . 18 ((โ„Ž โˆˆ Fin โˆง ๐‘— โˆˆ Fin) โ†’ (โ„Ž โˆช ๐‘—) โˆˆ Fin)
7875, 76, 77syl2anc 585 . . . . . . . . . . . . . . . . 17 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (โ„Ž โˆช ๐‘—) โˆˆ Fin)
79 vex 3441 . . . . . . . . . . . . . . . . . . . . . 22 โ„Ž โˆˆ V
80 vex 3441 . . . . . . . . . . . . . . . . . . . . . 22 ๐‘— โˆˆ V
8179, 80unex 7628 . . . . . . . . . . . . . . . . . . . . 21 (โ„Ž โˆช ๐‘—) โˆˆ V
8281a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (โ„Ž โˆช ๐‘—) โˆˆ V)
83 ssun1 4112 . . . . . . . . . . . . . . . . . . . . 21 โ„Ž โŠ† (โ„Ž โˆช ๐‘—)
8483a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ โ„Ž โŠ† (โ„Ž โˆช ๐‘—))
85 simpllr 774 . . . . . . . . . . . . . . . . . . . 20 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ ๐‘– โˆˆ (mzPolyโ€˜โ„Ž))
86 mzpresrename 40767 . . . . . . . . . . . . . . . . . . . 20 (((โ„Ž โˆช ๐‘—) โˆˆ V โˆง โ„Ž โŠ† (โ„Ž โˆช ๐‘—) โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โ†’ (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ (๐‘–โ€˜(๐‘™ โ†พ โ„Ž))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—)))
8782, 84, 85, 86syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ (๐‘–โ€˜(๐‘™ โ†พ โ„Ž))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—)))
88 ssun2 4113 . . . . . . . . . . . . . . . . . . . . 21 ๐‘— โŠ† (โ„Ž โˆช ๐‘—)
8988a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ ๐‘— โŠ† (โ„Ž โˆช ๐‘—))
90 simprlr 778 . . . . . . . . . . . . . . . . . . . 20 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—))
91 mzpresrename 40767 . . . . . . . . . . . . . . . . . . . 20 (((โ„Ž โˆช ๐‘—) โˆˆ V โˆง ๐‘— โŠ† (โ„Ž โˆช ๐‘—) โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โ†’ (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—)))
9282, 89, 90, 91syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—)))
93 mzpaddmpt 40758 . . . . . . . . . . . . . . . . . . 19 (((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ (๐‘–โ€˜(๐‘™ โ†พ โ„Ž))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—)) โˆง (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—))) โ†’ (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—)))
9487, 92, 93syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—)))
95 simplr 767 . . . . . . . . . . . . . . . . . . 19 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ โ„Ž โŠ† ๐ต)
96 simprr 771 . . . . . . . . . . . . . . . . . . 19 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ ๐‘— โŠ† ๐ต)
9795, 96unssd 4126 . . . . . . . . . . . . . . . . . 18 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (โ„Ž โˆช ๐‘—) โŠ† ๐ต)
98 ovex 7340 . . . . . . . . . . . . . . . . . . . . 21 (โ„ค โ†‘m ๐ต) โˆˆ V
9998a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (โ„ค โ†‘m ๐ต) โˆˆ V)
100 mzpcompact2lem.i . . . . . . . . . . . . . . . . . . . . . . 23 ๐ต โˆˆ V
101100a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ ๐ต โˆˆ V)
102 mzpresrename 40767 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ต โˆˆ V โˆง โ„Ž โŠ† ๐ต โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆˆ (mzPolyโ€˜๐ต))
103101, 95, 85, 102syl3anc 1371 . . . . . . . . . . . . . . . . . . . . 21 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆˆ (mzPolyโ€˜๐ต))
104 mzpf 40753 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆˆ (mzPolyโ€˜๐ต) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))):(โ„ค โ†‘m ๐ต)โŸถโ„ค)
105 ffn 6630 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))):(โ„ค โ†‘m ๐ต)โŸถโ„ค โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) Fn (โ„ค โ†‘m ๐ต))
106103, 104, 1053syl 18 . . . . . . . . . . . . . . . . . . . 20 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) Fn (โ„ค โ†‘m ๐ต))
107 mzpresrename 40767 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ต โˆˆ V โˆง ๐‘— โŠ† ๐ต โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))) โˆˆ (mzPolyโ€˜๐ต))
108101, 96, 90, 107syl3anc 1371 . . . . . . . . . . . . . . . . . . . . 21 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))) โˆˆ (mzPolyโ€˜๐ต))
109 mzpf 40753 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))) โˆˆ (mzPolyโ€˜๐ต) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))):(โ„ค โ†‘m ๐ต)โŸถโ„ค)
110 ffn 6630 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))):(โ„ค โ†‘m ๐ต)โŸถโ„ค โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))) Fn (โ„ค โ†‘m ๐ต))
111108, 109, 1103syl 18 . . . . . . . . . . . . . . . . . . . 20 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))) Fn (โ„ค โ†‘m ๐ต))
112 ofmpteq 7587 . . . . . . . . . . . . . . . . . . . 20 (((โ„ค โ†‘m ๐ต) โˆˆ V โˆง (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) Fn (โ„ค โ†‘m ๐ต) โˆง (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))) Fn (โ„ค โ†‘m ๐ต)) โ†’ ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))
11399, 106, 111, 112syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))
114 elmapi 8668 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†’ ๐‘‘:๐ตโŸถโ„ค)
115 fssres 6670 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘‘:๐ตโŸถโ„ค โˆง (โ„Ž โˆช ๐‘—) โŠ† ๐ต) โ†’ (๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)):(โ„Ž โˆช ๐‘—)โŸถโ„ค)
116114, 97, 115syl2anr 598 . . . . . . . . . . . . . . . . . . . . . . 23 (((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ (๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)):(โ„Ž โˆช ๐‘—)โŸถโ„ค)
117 zex 12378 . . . . . . . . . . . . . . . . . . . . . . . 24 โ„ค โˆˆ V
118117, 81elmap 8690 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†” (๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)):(โ„Ž โˆช ๐‘—)โŸถโ„ค)
119116, 118sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 (((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ (๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)))
120 reseq1 5897 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘™ = (๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†’ (๐‘™ โ†พ โ„Ž) = ((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž))
121120fveq2d 6808 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘™ = (๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†’ (๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) = (๐‘–โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž)))
122 reseq1 5897 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘™ = (๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†’ (๐‘™ โ†พ ๐‘—) = ((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—))
123122fveq2d 6808 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘™ = (๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†’ (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)) = (๐‘˜โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—)))
124121, 123oveq12d 7325 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘™ = (๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†’ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))) = ((๐‘–โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž)) + (๐‘˜โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—))))
125 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) = (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))
126 ovex 7340 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘–โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž)) + (๐‘˜โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—))) โˆˆ V
127124, 125, 126fvmpt 6907 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†’ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))) = ((๐‘–โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž)) + (๐‘˜โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—))))
128119, 127syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))) = ((๐‘–โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž)) + (๐‘˜โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—))))
129 resabs1 5933 . . . . . . . . . . . . . . . . . . . . . . . 24 (โ„Ž โŠ† (โ„Ž โˆช ๐‘—) โ†’ ((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž) = (๐‘‘ โ†พ โ„Ž))
13083, 129ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž) = (๐‘‘ โ†พ โ„Ž)
131130fveq2i 6807 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘–โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž)) = (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))
132 resabs1 5933 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘— โŠ† (โ„Ž โˆช ๐‘—) โ†’ ((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—) = (๐‘‘ โ†พ ๐‘—))
13388, 132ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—) = (๐‘‘ โ†พ ๐‘—)
134133fveq2i 6807 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘˜โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—)) = (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))
135131, 134oveq12i 7319 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘–โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž)) + (๐‘˜โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—))) = ((๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))
136128, 135eqtr2di 2793 . . . . . . . . . . . . . . . . . . . 20 (((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ ((๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))) = ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))
137136mpteq2dva 5181 . . . . . . . . . . . . . . . . . . 19 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))
138113, 137eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))
139 fveq1 6803 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ = (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โ†’ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))) = ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))
140139mpteq2dv 5183 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ = (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))
141140eqeq2d 2747 . . . . . . . . . . . . . . . . . . . 20 (๐‘ = (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โ†’ (((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))) โ†” ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))))
142141anbi2d 630 . . . . . . . . . . . . . . . . . . 19 (๐‘ = (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โ†’ (((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))) โ†” ((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))))
143142rspcev 3566 . . . . . . . . . . . . . . . . . 18 (((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—)) โˆง ((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) + (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))) โ†’ โˆƒ๐‘ โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—))((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))))
14494, 97, 138, 143syl12anc 835 . . . . . . . . . . . . . . . . 17 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ โˆƒ๐‘ โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—))((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))))
145 mzpmulmpt 40759 . . . . . . . . . . . . . . . . . . 19 (((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ (๐‘–โ€˜(๐‘™ โ†พ โ„Ž))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—)) โˆง (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—))) โ†’ (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—)))
14687, 92, 145syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—)))
147 ofmpteq 7587 . . . . . . . . . . . . . . . . . . . 20 (((โ„ค โ†‘m ๐ต) โˆˆ V โˆง (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) Fn (โ„ค โ†‘m ๐ต) โˆง (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))) Fn (โ„ค โ†‘m ๐ต)) โ†’ ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))
14899, 106, 111, 147syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))
149121, 123oveq12d 7325 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘™ = (๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†’ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))) = ((๐‘–โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž)) ยท (๐‘˜โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—))))
150 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) = (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))
151 ovex 7340 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘–โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž)) ยท (๐‘˜โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—))) โˆˆ V
152149, 150, 151fvmpt 6907 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†’ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))) = ((๐‘–โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž)) ยท (๐‘˜โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—))))
153119, 152syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))) = ((๐‘–โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž)) ยท (๐‘˜โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—))))
154131, 134oveq12i 7319 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘–โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ โ„Ž)) ยท (๐‘˜โ€˜((๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)) โ†พ ๐‘—))) = ((๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))
155153, 154eqtr2di 2793 . . . . . . . . . . . . . . . . . . . 20 (((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โˆง ๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต)) โ†’ ((๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))) = ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))
156155mpteq2dva 5181 . . . . . . . . . . . . . . . . . . 19 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))
157148, 156eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))
158 fveq1 6803 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ = (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โ†’ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))) = ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))
159158mpteq2dv 5183 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ = (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))
160159eqeq2d 2747 . . . . . . . . . . . . . . . . . . . 20 (๐‘ = (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โ†’ (((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))) โ†” ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))))
161160anbi2d 630 . . . . . . . . . . . . . . . . . . 19 (๐‘ = (๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โ†’ (((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))) โ†” ((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))))
162161rspcev 3566 . . . . . . . . . . . . . . . . . 18 (((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—)))) โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—)) โˆง ((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ ((๐‘™ โˆˆ (โ„ค โ†‘m (โ„Ž โˆช ๐‘—)) โ†ฆ ((๐‘–โ€˜(๐‘™ โ†พ โ„Ž)) ยท (๐‘˜โ€˜(๐‘™ โ†พ ๐‘—))))โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))) โ†’ โˆƒ๐‘ โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—))((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))))
163146, 97, 157, 162syl12anc 835 . . . . . . . . . . . . . . . . 17 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ โˆƒ๐‘ โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—))((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))))
164 fveq2 6804 . . . . . . . . . . . . . . . . . . . 20 (๐‘Ž = (โ„Ž โˆช ๐‘—) โ†’ (mzPolyโ€˜๐‘Ž) = (mzPolyโ€˜(โ„Ž โˆช ๐‘—)))
165 sseq1 3951 . . . . . . . . . . . . . . . . . . . . 21 (๐‘Ž = (โ„Ž โˆช ๐‘—) โ†’ (๐‘Ž โŠ† ๐ต โ†” (โ„Ž โˆช ๐‘—) โŠ† ๐ต))
166 reseq2 5898 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘Ž = (โ„Ž โˆช ๐‘—) โ†’ (๐‘‘ โ†พ ๐‘Ž) = (๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))
167166fveq2d 6808 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘Ž = (โ„Ž โˆช ๐‘—) โ†’ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)) = (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))
168167mpteq2dv 5183 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘Ž = (โ„Ž โˆช ๐‘—) โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))
169168eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . 21 (๐‘Ž = (โ„Ž โˆช ๐‘—) โ†’ (((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))))
170165, 169anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (๐‘Ž = (โ„Ž โˆช ๐‘—) โ†’ ((๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” ((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))))
171164, 170rexeqbidv 3356 . . . . . . . . . . . . . . . . . . 19 (๐‘Ž = (โ„Ž โˆช ๐‘—) โ†’ (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘ โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—))((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))))
172168eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . 21 (๐‘Ž = (โ„Ž โˆช ๐‘—) โ†’ (((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))))
173165, 172anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (๐‘Ž = (โ„Ž โˆช ๐‘—) โ†’ ((๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” ((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))))
174164, 173rexeqbidv 3356 . . . . . . . . . . . . . . . . . . 19 (๐‘Ž = (โ„Ž โˆช ๐‘—) โ†’ (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘ โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—))((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—)))))))
175171, 174anbi12d 632 . . . . . . . . . . . . . . . . . 18 (๐‘Ž = (โ„Ž โˆช ๐‘—) โ†’ ((โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))) โ†” (โˆƒ๐‘ โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—))((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—))((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))))))
176175rspcev 3566 . . . . . . . . . . . . . . . . 17 (((โ„Ž โˆช ๐‘—) โˆˆ Fin โˆง (โˆƒ๐‘ โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—))((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜(โ„Ž โˆช ๐‘—))((โ„Ž โˆช ๐‘—) โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ (โ„Ž โˆช ๐‘—))))))) โ†’ โˆƒ๐‘Ž โˆˆ Fin (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
17778, 144, 163, 176syl12anc 835 . . . . . . . . . . . . . . . 16 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง โ„Ž โŠ† ๐ต) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ โˆƒ๐‘Ž โˆˆ Fin (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
178177adantlrr 719 . . . . . . . . . . . . . . 15 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง ๐‘— โŠ† ๐ต)) โ†’ โˆƒ๐‘Ž โˆˆ Fin (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
179178adantrrr 723 . . . . . . . . . . . . . 14 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ โˆƒ๐‘Ž โˆˆ Fin (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
180 simplrr 776 . . . . . . . . . . . . . . . . . . . 20 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))
181 simprrr 780 . . . . . . . . . . . . . . . . . . . 20 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))))
182180, 181oveq12d 7325 . . . . . . . . . . . . . . . . . . 19 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ (๐‘“ โˆ˜f + ๐‘”) = ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))
183182eqeq1d 2738 . . . . . . . . . . . . . . . . . 18 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ ((๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
184183anbi2d 630 . . . . . . . . . . . . . . . . 17 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ ((๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
185184rexbidv 3172 . . . . . . . . . . . . . . . 16 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
186180, 181oveq12d 7325 . . . . . . . . . . . . . . . . . . 19 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ (๐‘“ โˆ˜f ยท ๐‘”) = ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))
187186eqeq1d 2738 . . . . . . . . . . . . . . . . . 18 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ ((๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
188187anbi2d 630 . . . . . . . . . . . . . . . . 17 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ ((๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
189188rexbidv 3172 . . . . . . . . . . . . . . . 16 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
190185, 189anbi12d 632 . . . . . . . . . . . . . . 15 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ ((โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))) โ†” (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))))
191190rexbidv 3172 . . . . . . . . . . . . . 14 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ (โˆƒ๐‘Ž โˆˆ Fin (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))) โ†” โˆƒ๐‘Ž โˆˆ Fin (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f + (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))) โˆ˜f ยท (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))))
192179, 191mpbird 257 . . . . . . . . . . . . 13 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ โˆƒ๐‘Ž โˆˆ Fin (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
193 r19.40 3119 . . . . . . . . . . . . 13 (โˆƒ๐‘Ž โˆˆ Fin (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
194192, 193syl 17 . . . . . . . . . . . 12 ((((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โˆง (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
195194exp32 422 . . . . . . . . . . 11 (((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โ†’ ((๐‘— โˆˆ Fin โˆง ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)) โ†’ ((๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))))
196195rexlimdvv 3201 . . . . . . . . . 10 (((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โˆง (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โ†’ (โˆƒ๐‘— โˆˆ Fin โˆƒ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))))
197196ex 414 . . . . . . . . 9 ((โ„Ž โˆˆ Fin โˆง ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)) โ†’ ((โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)))) โ†’ (โˆƒ๐‘— โˆˆ Fin โˆƒ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))))
198197rexlimivv 3193 . . . . . . . 8 (โˆƒโ„Ž โˆˆ Fin โˆƒ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)(โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)))) โ†’ (โˆƒ๐‘— โˆˆ Fin โˆƒ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))))
199198imp 408 . . . . . . 7 ((โˆƒโ„Ž โˆˆ Fin โˆƒ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)(โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)))) โˆง โˆƒ๐‘— โˆˆ Fin โˆƒ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))))) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
200199ad2ant2l 744 . . . . . 6 (((๐‘“:(โ„ค โ†‘m ๐ต)โŸถโ„ค โˆง โˆƒโ„Ž โˆˆ Fin โˆƒ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)(โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง (๐‘”:(โ„ค โ†‘m ๐ต)โŸถโ„ค โˆง โˆƒ๐‘— โˆˆ Fin โˆƒ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
2012003adant1 1130 . . . . 5 ((โŠค โˆง (๐‘“:(โ„ค โ†‘m ๐ต)โŸถโ„ค โˆง โˆƒโ„Ž โˆˆ Fin โˆƒ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)(โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง (๐‘”:(โ„ค โ†‘m ๐ต)โŸถโ„ค โˆง โˆƒ๐‘— โˆˆ Fin โˆƒ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โˆง โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
202201simpld 496 . . . 4 ((โŠค โˆง (๐‘“:(โ„ค โ†‘m ๐ต)โŸถโ„ค โˆง โˆƒโ„Ž โˆˆ Fin โˆƒ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)(โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง (๐‘”:(โ„ค โ†‘m ๐ต)โŸถโ„ค โˆง โˆƒ๐‘— โˆˆ Fin โˆƒ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
203201simprd 497 . . . 4 ((โŠค โˆง (๐‘“:(โ„ค โ†‘m ๐ต)โŸถโ„ค โˆง โˆƒโ„Ž โˆˆ Fin โˆƒ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)(โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))) โˆง (๐‘”:(โ„ค โ†‘m ๐ต)โŸถโ„ค โˆง โˆƒ๐‘— โˆˆ Fin โˆƒ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))) โ†’ โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
204 eqeq1 2740 . . . . . 6 (๐‘’ = ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) โ†’ (๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
205204anbi2d 630 . . . . 5 (๐‘’ = ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) โ†’ ((๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (๐‘Ž โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
2062052rexbidv 3210 . . . 4 (๐‘’ = ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ((โ„ค โ†‘m ๐ต) ร— {๐‘“}) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
207 eqeq1 2740 . . . . . 6 (๐‘’ = (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) โ†’ (๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
208207anbi2d 630 . . . . 5 (๐‘’ = (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) โ†’ ((๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (๐‘Ž โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
2092082rexbidv 3210 . . . 4 (๐‘’ = (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘” โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘”โ€˜๐‘“)) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
210 eqeq1 2740 . . . . . . 7 (๐‘’ = ๐‘“ โ†’ (๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
211210anbi2d 630 . . . . . 6 (๐‘’ = ๐‘“ โ†’ ((๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (๐‘Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
2122112rexbidv 3210 . . . . 5 (๐‘’ = ๐‘“ โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
213 fveq2 6804 . . . . . . . 8 (๐‘Ž = โ„Ž โ†’ (mzPolyโ€˜๐‘Ž) = (mzPolyโ€˜โ„Ž))
214 sseq1 3951 . . . . . . . . 9 (๐‘Ž = โ„Ž โ†’ (๐‘Ž โŠ† ๐ต โ†” โ„Ž โŠ† ๐ต))
215 reseq2 5898 . . . . . . . . . . . 12 (๐‘Ž = โ„Ž โ†’ (๐‘‘ โ†พ ๐‘Ž) = (๐‘‘ โ†พ โ„Ž))
216215fveq2d 6808 . . . . . . . . . . 11 (๐‘Ž = โ„Ž โ†’ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)) = (๐‘โ€˜(๐‘‘ โ†พ โ„Ž)))
217216mpteq2dv 5183 . . . . . . . . . 10 (๐‘Ž = โ„Ž โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โ„Ž))))
218217eqeq2d 2747 . . . . . . . . 9 (๐‘Ž = โ„Ž โ†’ (๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โ„Ž)))))
219214, 218anbi12d 632 . . . . . . . 8 (๐‘Ž = โ„Ž โ†’ ((๐‘Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โ„Ž))))))
220213, 219rexeqbidv 3356 . . . . . . 7 (๐‘Ž = โ„Ž โ†’ (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘ โˆˆ (mzPolyโ€˜โ„Ž)(โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โ„Ž))))))
221 fveq1 6803 . . . . . . . . . . 11 (๐‘ = ๐‘– โ†’ (๐‘โ€˜(๐‘‘ โ†พ โ„Ž)) = (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)))
222221mpteq2dv 5183 . . . . . . . . . 10 (๐‘ = ๐‘– โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โ„Ž))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))
223222eqeq2d 2747 . . . . . . . . 9 (๐‘ = ๐‘– โ†’ (๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โ„Ž))) โ†” ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)))))
224223anbi2d 630 . . . . . . . 8 (๐‘ = ๐‘– โ†’ ((โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โ„Ž)))) โ†” (โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))))
225224cbvrexvw 3223 . . . . . . 7 (โˆƒ๐‘ โˆˆ (mzPolyโ€˜โ„Ž)(โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ โ„Ž)))) โ†” โˆƒ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)(โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)))))
226220, 225bitrdi 287 . . . . . 6 (๐‘Ž = โ„Ž โ†’ (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)(โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))))
227226cbvrexvw 3223 . . . . 5 (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒโ„Ž โˆˆ Fin โˆƒ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)(โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž)))))
228212, 227bitrdi 287 . . . 4 (๐‘’ = ๐‘“ โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒโ„Ž โˆˆ Fin โˆƒ๐‘– โˆˆ (mzPolyโ€˜โ„Ž)(โ„Ž โŠ† ๐ต โˆง ๐‘“ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘–โ€˜(๐‘‘ โ†พ โ„Ž))))))
229 eqeq1 2740 . . . . . . 7 (๐‘’ = ๐‘” โ†’ (๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
230229anbi2d 630 . . . . . 6 (๐‘’ = ๐‘” โ†’ ((๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (๐‘Ž โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
2312302rexbidv 3210 . . . . 5 (๐‘’ = ๐‘” โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
232 fveq2 6804 . . . . . . . 8 (๐‘Ž = ๐‘— โ†’ (mzPolyโ€˜๐‘Ž) = (mzPolyโ€˜๐‘—))
233 sseq1 3951 . . . . . . . . 9 (๐‘Ž = ๐‘— โ†’ (๐‘Ž โŠ† ๐ต โ†” ๐‘— โŠ† ๐ต))
234 reseq2 5898 . . . . . . . . . . . 12 (๐‘Ž = ๐‘— โ†’ (๐‘‘ โ†พ ๐‘Ž) = (๐‘‘ โ†พ ๐‘—))
235234fveq2d 6808 . . . . . . . . . . 11 (๐‘Ž = ๐‘— โ†’ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)) = (๐‘โ€˜(๐‘‘ โ†พ ๐‘—)))
236235mpteq2dv 5183 . . . . . . . . . 10 (๐‘Ž = ๐‘— โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘—))))
237236eqeq2d 2747 . . . . . . . . 9 (๐‘Ž = ๐‘— โ†’ (๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘—)))))
238233, 237anbi12d 632 . . . . . . . 8 (๐‘Ž = ๐‘— โ†’ ((๐‘Ž โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘—))))))
239232, 238rexeqbidv 3356 . . . . . . 7 (๐‘Ž = ๐‘— โ†’ (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘—))))))
240 fveq1 6803 . . . . . . . . . . 11 (๐‘ = ๐‘˜ โ†’ (๐‘โ€˜(๐‘‘ โ†พ ๐‘—)) = (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))
241240mpteq2dv 5183 . . . . . . . . . 10 (๐‘ = ๐‘˜ โ†’ (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘—))) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))))
242241eqeq2d 2747 . . . . . . . . 9 (๐‘ = ๐‘˜ โ†’ (๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘—))) โ†” ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))
243242anbi2d 630 . . . . . . . 8 (๐‘ = ๐‘˜ โ†’ ((๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘—)))) โ†” (๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))))))
244243cbvrexvw 3223 . . . . . . 7 (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘—)))) โ†” โˆƒ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))
245239, 244bitrdi 287 . . . . . 6 (๐‘Ž = ๐‘— โ†’ (โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))))))
246245cbvrexvw 3223 . . . . 5 (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘— โˆˆ Fin โˆƒ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—)))))
247231, 246bitrdi 287 . . . 4 (๐‘’ = ๐‘” โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘— โˆˆ Fin โˆƒ๐‘˜ โˆˆ (mzPolyโ€˜๐‘—)(๐‘— โŠ† ๐ต โˆง ๐‘” = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘˜โ€˜(๐‘‘ โ†พ ๐‘—))))))
248 eqeq1 2740 . . . . . 6 (๐‘’ = (๐‘“ โˆ˜f + ๐‘”) โ†’ (๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
249248anbi2d 630 . . . . 5 (๐‘’ = (๐‘“ โˆ˜f + ๐‘”) โ†’ ((๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
2502492rexbidv 3210 . . . 4 (๐‘’ = (๐‘“ โˆ˜f + ๐‘”) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f + ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
251 eqeq1 2740 . . . . . 6 (๐‘’ = (๐‘“ โˆ˜f ยท ๐‘”) โ†’ (๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
252251anbi2d 630 . . . . 5 (๐‘’ = (๐‘“ โˆ˜f ยท ๐‘”) โ†’ ((๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
2532522rexbidv 3210 . . . 4 (๐‘’ = (๐‘“ โˆ˜f ยท ๐‘”) โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง (๐‘“ โˆ˜f ยท ๐‘”) = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
254 eqeq1 2740 . . . . . 6 (๐‘’ = ๐ด โ†’ (๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” ๐ด = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
255254anbi2d 630 . . . . 5 (๐‘’ = ๐ด โ†’ ((๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (๐‘Ž โŠ† ๐ต โˆง ๐ด = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
2562552rexbidv 3210 . . . 4 (๐‘’ = ๐ด โ†’ (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐‘’ = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐ด = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))))))
25733, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256mzpindd 40763 . . 3 ((โŠค โˆง ๐ด โˆˆ (mzPolyโ€˜๐ต)) โ†’ โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐ด = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
2581, 257mpan 688 . 2 (๐ด โˆˆ (mzPolyโ€˜๐ต) โ†’ โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐ด = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))))
259 reseq1 5897 . . . . . . 7 (๐‘‘ = ๐‘ โ†’ (๐‘‘ โ†พ ๐‘Ž) = (๐‘ โ†พ ๐‘Ž))
260259fveq2d 6808 . . . . . 6 (๐‘‘ = ๐‘ โ†’ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)) = (๐‘โ€˜(๐‘ โ†พ ๐‘Ž)))
261260cbvmptv 5194 . . . . 5 (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) = (๐‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘ โ†พ ๐‘Ž)))
262261eqeq2i 2749 . . . 4 (๐ด = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž))) โ†” ๐ด = (๐‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘ โ†พ ๐‘Ž))))
263262anbi2i 624 . . 3 ((๐‘Ž โŠ† ๐ต โˆง ๐ด = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” (๐‘Ž โŠ† ๐ต โˆง ๐ด = (๐‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘ โ†พ ๐‘Ž)))))
2642632rexbii 3125 . 2 (โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐ด = (๐‘‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘‘ โ†พ ๐‘Ž)))) โ†” โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐ด = (๐‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘ โ†พ ๐‘Ž)))))
265258, 264sylib 217 1 (๐ด โˆˆ (mzPolyโ€˜๐ต) โ†’ โˆƒ๐‘Ž โˆˆ Fin โˆƒ๐‘ โˆˆ (mzPolyโ€˜๐‘Ž)(๐‘Ž โŠ† ๐ต โˆง ๐ด = (๐‘ โˆˆ (โ„ค โ†‘m ๐ต) โ†ฆ (๐‘โ€˜(๐‘ โ†พ ๐‘Ž)))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   โˆง w3a 1087   = wceq 1539  โŠคwtru 1540   โˆˆ wcel 2104  โˆƒwrex 3071  Vcvv 3437   โˆช cun 3890   โŠ† wss 3892  โˆ…c0 4262  {csn 4565   โ†ฆ cmpt 5164   ร— cxp 5598   โ†พ cres 5602   Fn wfn 6453  โŸถwf 6454  โ€˜cfv 6458  (class class class)co 7307   โˆ˜f cof 7563   โ†‘m cmap 8646  Fincfn 8764   + caddc 10924   ยท cmul 10926  โ„คcz 12369  mzPolycmzp 40739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-cnex 10977  ax-resscn 10978  ax-1cn 10979  ax-icn 10980  ax-addcl 10981  ax-addrcl 10982  ax-mulcl 10983  ax-mulrcl 10984  ax-mulcom 10985  ax-addass 10986  ax-mulass 10987  ax-distr 10988  ax-i2m1 10989  ax-1ne0 10990  ax-1rid 10991  ax-rnegex 10992  ax-rrecex 10993  ax-cnre 10994  ax-pre-lttri 10995  ax-pre-lttrn 10996  ax-pre-ltadd 10997  ax-pre-mulgt0 10998
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3305  df-rab 3306  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-int 4887  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-of 7565  df-om 7745  df-1st 7863  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-1o 8328  df-er 8529  df-map 8648  df-en 8765  df-dom 8766  df-sdom 8767  df-fin 8768  df-pnf 11061  df-mnf 11062  df-xr 11063  df-ltxr 11064  df-le 11065  df-sub 11257  df-neg 11258  df-nn 12024  df-n0 12284  df-z 12370  df-mzpcl 40740  df-mzp 40741
This theorem is referenced by:  mzpcompact2  40769
  Copyright terms: Public domain W3C validator