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

Theorem mhpmulcl 21555
Description: A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 25460 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024.)
Hypotheses
Ref Expression
mhpmulcl.h ๐ป = (๐ผ mHomP ๐‘…)
mhpmulcl.y ๐‘Œ = (๐ผ mPoly ๐‘…)
mhpmulcl.t ยท = (.rโ€˜๐‘Œ)
mhpmulcl.i (๐œ‘ โ†’ ๐ผ โˆˆ ๐‘‰)
mhpmulcl.r (๐œ‘ โ†’ ๐‘… โˆˆ Ring)
mhpmulcl.m (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0)
mhpmulcl.n (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
mhpmulcl.p (๐œ‘ โ†’ ๐‘ƒ โˆˆ (๐ปโ€˜๐‘€))
mhpmulcl.q (๐œ‘ โ†’ ๐‘„ โˆˆ (๐ปโ€˜๐‘))
Assertion
Ref Expression
mhpmulcl (๐œ‘ โ†’ (๐‘ƒ ยท ๐‘„) โˆˆ (๐ปโ€˜(๐‘€ + ๐‘)))

Proof of Theorem mhpmulcl
Dummy variables ๐‘ ๐‘‘ ๐‘’ ๐‘– ๐‘ฅ ๐‘ โ„Ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mhpmulcl.y . . . . . . . 8 ๐‘Œ = (๐ผ mPoly ๐‘…)
2 eqid 2737 . . . . . . . 8 (Baseโ€˜๐‘Œ) = (Baseโ€˜๐‘Œ)
3 eqid 2737 . . . . . . . 8 (.rโ€˜๐‘…) = (.rโ€˜๐‘…)
4 mhpmulcl.t . . . . . . . 8 ยท = (.rโ€˜๐‘Œ)
5 eqid 2737 . . . . . . . 8 {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} = {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}
6 mhpmulcl.h . . . . . . . . 9 ๐ป = (๐ผ mHomP ๐‘…)
7 mhpmulcl.i . . . . . . . . 9 (๐œ‘ โ†’ ๐ผ โˆˆ ๐‘‰)
8 mhpmulcl.r . . . . . . . . 9 (๐œ‘ โ†’ ๐‘… โˆˆ Ring)
9 mhpmulcl.m . . . . . . . . 9 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0)
10 mhpmulcl.p . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ƒ โˆˆ (๐ปโ€˜๐‘€))
116, 1, 2, 7, 8, 9, 10mhpmpl 21550 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ƒ โˆˆ (Baseโ€˜๐‘Œ))
12 mhpmulcl.n . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
13 mhpmulcl.q . . . . . . . . 9 (๐œ‘ โ†’ ๐‘„ โˆˆ (๐ปโ€˜๐‘))
146, 1, 2, 7, 8, 12, 13mhpmpl 21550 . . . . . . . 8 (๐œ‘ โ†’ ๐‘„ โˆˆ (Baseโ€˜๐‘Œ))
151, 2, 3, 4, 5, 11, 14mplmul 21431 . . . . . . 7 (๐œ‘ โ†’ (๐‘ƒ ยท ๐‘„) = (๐‘‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โ†ฆ (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘‘} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘‘ โˆ˜f โˆ’ ๐‘’)))))))
1615adantr 482 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โ†’ (๐‘ƒ ยท ๐‘„) = (๐‘‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โ†ฆ (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘‘} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘‘ โˆ˜f โˆ’ ๐‘’)))))))
17 breq2 5114 . . . . . . . . . 10 (๐‘‘ = ๐‘ฅ โ†’ (๐‘ โˆ˜r โ‰ค ๐‘‘ โ†” ๐‘ โˆ˜r โ‰ค ๐‘ฅ))
1817rabbidv 3418 . . . . . . . . 9 (๐‘‘ = ๐‘ฅ โ†’ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘‘} = {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ})
19 fvoveq1 7385 . . . . . . . . . 10 (๐‘‘ = ๐‘ฅ โ†’ (๐‘„โ€˜(๐‘‘ โˆ˜f โˆ’ ๐‘’)) = (๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’)))
2019oveq2d 7378 . . . . . . . . 9 (๐‘‘ = ๐‘ฅ โ†’ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘‘ โˆ˜f โˆ’ ๐‘’))) = ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))))
2118, 20mpteq12dv 5201 . . . . . . . 8 (๐‘‘ = ๐‘ฅ โ†’ (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘‘} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘‘ โˆ˜f โˆ’ ๐‘’)))) = (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’)))))
2221oveq2d 7378 . . . . . . 7 (๐‘‘ = ๐‘ฅ โ†’ (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘‘} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘‘ โˆ˜f โˆ’ ๐‘’))))) = (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))))))
2322adantl 483 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ๐‘‘ = ๐‘ฅ) โ†’ (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘‘} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘‘ โˆ˜f โˆ’ ๐‘’))))) = (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))))))
24 simpr 486 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โ†’ ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin})
25 ovexd 7397 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โ†’ (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))))) โˆˆ V)
2616, 23, 24, 25fvmptd 6960 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โ†’ ((๐‘ƒ ยท ๐‘„)โ€˜๐‘ฅ) = (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))))))
2726neeq1d 3004 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โ†’ (((๐‘ƒ ยท ๐‘„)โ€˜๐‘ฅ) โ‰  (0gโ€˜๐‘…) โ†” (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))))) โ‰  (0gโ€˜๐‘…)))
28 simp-4l 782 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ๐œ‘)
29 oveq2 7370 . . . . . . . . . . . . . . . . 17 (๐‘ = ๐‘’ โ†’ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’))
3029eqeq1d 2739 . . . . . . . . . . . . . . . 16 (๐‘ = ๐‘’ โ†’ (((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘€ โ†” ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) = ๐‘€))
3130necon3bbid 2982 . . . . . . . . . . . . . . 15 (๐‘ = ๐‘’ โ†’ (ยฌ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘€ โ†” ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€))
32 simplr 768 . . . . . . . . . . . . . . . 16 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ})
33 elrabi 3644 . . . . . . . . . . . . . . . 16 (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†’ ๐‘’ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin})
3432, 33syl 17 . . . . . . . . . . . . . . 15 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ๐‘’ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin})
35 simpr 486 . . . . . . . . . . . . . . 15 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€)
3631, 34, 35elrabd 3652 . . . . . . . . . . . . . 14 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ยฌ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘€})
37 notrab 4276 . . . . . . . . . . . . . 14 ({โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆ– {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘€}) = {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ยฌ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘€}
3836, 37eleqtrrdi 2849 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ๐‘’ โˆˆ ({โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆ– {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘€}))
39 eqid 2737 . . . . . . . . . . . . . . 15 (Baseโ€˜๐‘…) = (Baseโ€˜๐‘…)
401, 39, 2, 5, 11mplelf 21420 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘ƒ:{โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}โŸถ(Baseโ€˜๐‘…))
41 eqid 2737 . . . . . . . . . . . . . . 15 (0gโ€˜๐‘…) = (0gโ€˜๐‘…)
426, 41, 5, 7, 8, 9, 10mhpdeg 21551 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ƒ supp (0gโ€˜๐‘…)) โŠ† {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘€})
43 ovex 7395 . . . . . . . . . . . . . . . 16 (โ„•0 โ†‘m ๐ผ) โˆˆ V
4443rabex 5294 . . . . . . . . . . . . . . 15 {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆˆ V
4544a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆˆ V)
46 fvexd 6862 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (0gโ€˜๐‘…) โˆˆ V)
4740, 42, 45, 46suppssr 8132 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘’ โˆˆ ({โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆ– {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘€})) โ†’ (๐‘ƒโ€˜๐‘’) = (0gโ€˜๐‘…))
4828, 38, 47syl2anc 585 . . . . . . . . . . . 12 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ (๐‘ƒโ€˜๐‘’) = (0gโ€˜๐‘…))
4948oveq1d 7377 . . . . . . . . . . 11 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))) = ((0gโ€˜๐‘…)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))))
508ad4antr 731 . . . . . . . . . . . 12 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ๐‘… โˆˆ Ring)
5114ad4antr 731 . . . . . . . . . . . . . 14 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ๐‘„ โˆˆ (Baseโ€˜๐‘Œ))
521, 39, 2, 5, 51mplelf 21420 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ๐‘„:{โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}โŸถ(Baseโ€˜๐‘…))
53 simp-4r 783 . . . . . . . . . . . . . . 15 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin})
54 eqid 2737 . . . . . . . . . . . . . . . 16 {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} = {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}
555, 54psrbagconcl 21352 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ})
5653, 32, 55syl2anc 585 . . . . . . . . . . . . . 14 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ})
57 elrabi 3644 . . . . . . . . . . . . . 14 ((๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin})
5856, 57syl 17 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin})
5952, 58ffvelcdmd 7041 . . . . . . . . . . . 12 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ (๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โˆˆ (Baseโ€˜๐‘…))
6039, 3, 41ringlz 20018 . . . . . . . . . . . 12 ((๐‘… โˆˆ Ring โˆง (๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โˆˆ (Baseโ€˜๐‘…)) โ†’ ((0gโ€˜๐‘…)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))) = (0gโ€˜๐‘…))
6150, 59, 60syl2anc 585 . . . . . . . . . . 11 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ((0gโ€˜๐‘…)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))) = (0gโ€˜๐‘…))
6249, 61eqtrd 2777 . . . . . . . . . 10 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€) โ†’ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))) = (0gโ€˜๐‘…))
63 simp-4l 782 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ ๐œ‘)
64 oveq2 7370 . . . . . . . . . . . . . . . . 17 (๐‘ = (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โ†’ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)))
6564eqeq1d 2739 . . . . . . . . . . . . . . . 16 (๐‘ = (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โ†’ (((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘ โ†” ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) = ๐‘))
6665necon3bbid 2982 . . . . . . . . . . . . . . 15 (๐‘ = (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โ†’ (ยฌ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘ โ†” ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘))
67 simp-4r 783 . . . . . . . . . . . . . . . . 17 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin})
68 simplr 768 . . . . . . . . . . . . . . . . 17 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ})
6967, 68, 55syl2anc 585 . . . . . . . . . . . . . . . 16 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ})
7069, 57syl 17 . . . . . . . . . . . . . . 15 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin})
71 simpr 486 . . . . . . . . . . . . . . 15 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘)
7266, 70, 71elrabd 3652 . . . . . . . . . . . . . 14 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ยฌ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘})
73 notrab 4276 . . . . . . . . . . . . . 14 ({โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆ– {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘}) = {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ยฌ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘}
7472, 73eleqtrrdi 2849 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆˆ ({โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆ– {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘}))
751, 39, 2, 5, 14mplelf 21420 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘„:{โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}โŸถ(Baseโ€˜๐‘…))
766, 41, 5, 7, 8, 12, 13mhpdeg 21551 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘„ supp (0gโ€˜๐‘…)) โŠ† {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘})
7775, 76, 45, 46suppssr 8132 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆˆ ({โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆ– {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘) = ๐‘})) โ†’ (๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’)) = (0gโ€˜๐‘…))
7863, 74, 77syl2anc 585 . . . . . . . . . . . 12 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ (๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’)) = (0gโ€˜๐‘…))
7978oveq2d 7378 . . . . . . . . . . 11 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))) = ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(0gโ€˜๐‘…)))
808ad4antr 731 . . . . . . . . . . . 12 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ ๐‘… โˆˆ Ring)
8111ad4antr 731 . . . . . . . . . . . . . 14 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ ๐‘ƒ โˆˆ (Baseโ€˜๐‘Œ))
821, 39, 2, 5, 81mplelf 21420 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ ๐‘ƒ:{โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}โŸถ(Baseโ€˜๐‘…))
8333adantl 483 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ๐‘’ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin})
8483adantr 482 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ ๐‘’ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin})
8582, 84ffvelcdmd 7041 . . . . . . . . . . . 12 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ (๐‘ƒโ€˜๐‘’) โˆˆ (Baseโ€˜๐‘…))
8639, 3, 41ringrz 20019 . . . . . . . . . . . 12 ((๐‘… โˆˆ Ring โˆง (๐‘ƒโ€˜๐‘’) โˆˆ (Baseโ€˜๐‘…)) โ†’ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
8780, 85, 86syl2anc 585 . . . . . . . . . . 11 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
8879, 87eqtrd 2777 . . . . . . . . . 10 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†’ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))) = (0gโ€˜๐‘…))
89 nn0subm 20868 . . . . . . . . . . . . . . . 16 โ„•0 โˆˆ (SubMndโ€˜โ„‚fld)
90 eqid 2737 . . . . . . . . . . . . . . . . 17 (โ„‚fld โ†พs โ„•0) = (โ„‚fld โ†พs โ„•0)
9190submbas 18632 . . . . . . . . . . . . . . . 16 (โ„•0 โˆˆ (SubMndโ€˜โ„‚fld) โ†’ โ„•0 = (Baseโ€˜(โ„‚fld โ†พs โ„•0)))
9289, 91ax-mp 5 . . . . . . . . . . . . . . 15 โ„•0 = (Baseโ€˜(โ„‚fld โ†พs โ„•0))
93 cnfld0 20837 . . . . . . . . . . . . . . . . 17 0 = (0gโ€˜โ„‚fld)
9490, 93subm0 18633 . . . . . . . . . . . . . . . 16 (โ„•0 โˆˆ (SubMndโ€˜โ„‚fld) โ†’ 0 = (0gโ€˜(โ„‚fld โ†พs โ„•0)))
9589, 94ax-mp 5 . . . . . . . . . . . . . . 15 0 = (0gโ€˜(โ„‚fld โ†พs โ„•0))
96 nn0ex 12426 . . . . . . . . . . . . . . . 16 โ„•0 โˆˆ V
97 cnfldadd 20817 . . . . . . . . . . . . . . . . 17 + = (+gโ€˜โ„‚fld)
9890, 97ressplusg 17178 . . . . . . . . . . . . . . . 16 (โ„•0 โˆˆ V โ†’ + = (+gโ€˜(โ„‚fld โ†พs โ„•0)))
9996, 98ax-mp 5 . . . . . . . . . . . . . . 15 + = (+gโ€˜(โ„‚fld โ†พs โ„•0))
100 cnring 20835 . . . . . . . . . . . . . . . . . 18 โ„‚fld โˆˆ Ring
101 ringcmn 20010 . . . . . . . . . . . . . . . . . 18 (โ„‚fld โˆˆ Ring โ†’ โ„‚fld โˆˆ CMnd)
102100, 101ax-mp 5 . . . . . . . . . . . . . . . . 17 โ„‚fld โˆˆ CMnd
10390submcmn 19623 . . . . . . . . . . . . . . . . 17 ((โ„‚fld โˆˆ CMnd โˆง โ„•0 โˆˆ (SubMndโ€˜โ„‚fld)) โ†’ (โ„‚fld โ†พs โ„•0) โˆˆ CMnd)
104102, 89, 103mp2an 691 . . . . . . . . . . . . . . . 16 (โ„‚fld โ†พs โ„•0) โˆˆ CMnd
105104a1i 11 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (โ„‚fld โ†พs โ„•0) โˆˆ CMnd)
1067ad3antrrr 729 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ๐ผ โˆˆ ๐‘‰)
1075psrbagf 21336 . . . . . . . . . . . . . . . 16 (๐‘’ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โ†’ ๐‘’:๐ผโŸถโ„•0)
10883, 107syl 17 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ๐‘’:๐ผโŸถโ„•0)
109 simpllr 775 . . . . . . . . . . . . . . . . . . 19 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin})
1105psrbagf 21336 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โ†’ ๐‘ฅ:๐ผโŸถโ„•0)
111109, 110syl 17 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ๐‘ฅ:๐ผโŸถโ„•0)
112111ffnd 6674 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ๐‘ฅ Fn ๐ผ)
113108ffnd 6674 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ๐‘’ Fn ๐ผ)
114 inidm 4183 . . . . . . . . . . . . . . . . 17 (๐ผ โˆฉ ๐ผ) = ๐ผ
115 eqidd 2738 . . . . . . . . . . . . . . . . 17 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘– โˆˆ ๐ผ) โ†’ (๐‘ฅโ€˜๐‘–) = (๐‘ฅโ€˜๐‘–))
116 eqidd 2738 . . . . . . . . . . . . . . . . 17 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘– โˆˆ ๐ผ) โ†’ (๐‘’โ€˜๐‘–) = (๐‘’โ€˜๐‘–))
117112, 113, 106, 106, 114, 115, 116offval 7631 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’) = (๐‘– โˆˆ ๐ผ โ†ฆ ((๐‘ฅโ€˜๐‘–) โˆ’ (๐‘’โ€˜๐‘–))))
118 simpl 484 . . . . . . . . . . . . . . . . . 18 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘– โˆˆ ๐ผ) โ†’ (((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}))
119 simplr 768 . . . . . . . . . . . . . . . . . . 19 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘– โˆˆ ๐ผ) โ†’ ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ})
120 breq1 5113 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ = ๐‘’ โ†’ (๐‘ โˆ˜r โ‰ค ๐‘ฅ โ†” ๐‘’ โˆ˜r โ‰ค ๐‘ฅ))
121120elrab 3650 . . . . . . . . . . . . . . . . . . . 20 (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†” (๐‘’ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆง ๐‘’ โˆ˜r โ‰ค ๐‘ฅ))
122121simprbi 498 . . . . . . . . . . . . . . . . . . 19 (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†’ ๐‘’ โˆ˜r โ‰ค ๐‘ฅ)
123119, 122syl 17 . . . . . . . . . . . . . . . . . 18 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘– โˆˆ ๐ผ) โ†’ ๐‘’ โˆ˜r โ‰ค ๐‘ฅ)
124 simpr 486 . . . . . . . . . . . . . . . . . 18 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘– โˆˆ ๐ผ) โ†’ ๐‘– โˆˆ ๐ผ)
125113, 112, 106, 106, 114, 116, 115ofrval 7634 . . . . . . . . . . . . . . . . . 18 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘’ โˆ˜r โ‰ค ๐‘ฅ โˆง ๐‘– โˆˆ ๐ผ) โ†’ (๐‘’โ€˜๐‘–) โ‰ค (๐‘ฅโ€˜๐‘–))
126118, 123, 124, 125syl3anc 1372 . . . . . . . . . . . . . . . . 17 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘– โˆˆ ๐ผ) โ†’ (๐‘’โ€˜๐‘–) โ‰ค (๐‘ฅโ€˜๐‘–))
127108ffvelcdmda 7040 . . . . . . . . . . . . . . . . . 18 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘– โˆˆ ๐ผ) โ†’ (๐‘’โ€˜๐‘–) โˆˆ โ„•0)
128111ffvelcdmda 7040 . . . . . . . . . . . . . . . . . 18 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘– โˆˆ ๐ผ) โ†’ (๐‘ฅโ€˜๐‘–) โˆˆ โ„•0)
129 nn0sub 12470 . . . . . . . . . . . . . . . . . 18 (((๐‘’โ€˜๐‘–) โˆˆ โ„•0 โˆง (๐‘ฅโ€˜๐‘–) โˆˆ โ„•0) โ†’ ((๐‘’โ€˜๐‘–) โ‰ค (๐‘ฅโ€˜๐‘–) โ†” ((๐‘ฅโ€˜๐‘–) โˆ’ (๐‘’โ€˜๐‘–)) โˆˆ โ„•0))
130127, 128, 129syl2anc 585 . . . . . . . . . . . . . . . . 17 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘– โˆˆ ๐ผ) โ†’ ((๐‘’โ€˜๐‘–) โ‰ค (๐‘ฅโ€˜๐‘–) โ†” ((๐‘ฅโ€˜๐‘–) โˆ’ (๐‘’โ€˜๐‘–)) โˆˆ โ„•0))
131126, 130mpbid 231 . . . . . . . . . . . . . . . 16 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘– โˆˆ ๐ผ) โ†’ ((๐‘ฅโ€˜๐‘–) โˆ’ (๐‘’โ€˜๐‘–)) โˆˆ โ„•0)
132117, 131fmpt3d 7069 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’):๐ผโŸถโ„•0)
133108ffund 6677 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ Fun ๐‘’)
134 c0ex 11156 . . . . . . . . . . . . . . . . . . . 20 0 โˆˆ V
135106, 134jctir 522 . . . . . . . . . . . . . . . . . . 19 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐ผ โˆˆ ๐‘‰ โˆง 0 โˆˆ V))
136 fsuppeq 8111 . . . . . . . . . . . . . . . . . . 19 ((๐ผ โˆˆ ๐‘‰ โˆง 0 โˆˆ V) โ†’ (๐‘’:๐ผโŸถโ„•0 โ†’ (๐‘’ supp 0) = (โ—ก๐‘’ โ€œ (โ„•0 โˆ– {0}))))
137135, 108, 136sylc 65 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘’ supp 0) = (โ—ก๐‘’ โ€œ (โ„•0 โˆ– {0})))
138 dfn2 12433 . . . . . . . . . . . . . . . . . . 19 โ„• = (โ„•0 โˆ– {0})
139138imaeq2i 6016 . . . . . . . . . . . . . . . . . 18 (โ—ก๐‘’ โ€œ โ„•) = (โ—ก๐‘’ โ€œ (โ„•0 โˆ– {0}))
140137, 139eqtr4di 2795 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘’ supp 0) = (โ—ก๐‘’ โ€œ โ„•))
1415psrbag 21335 . . . . . . . . . . . . . . . . . . . 20 (๐ผ โˆˆ ๐‘‰ โ†’ (๐‘’ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โ†” (๐‘’:๐ผโŸถโ„•0 โˆง (โ—ก๐‘’ โ€œ โ„•) โˆˆ Fin)))
142106, 141syl 17 . . . . . . . . . . . . . . . . . . 19 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘’ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โ†” (๐‘’:๐ผโŸถโ„•0 โˆง (โ—ก๐‘’ โ€œ โ„•) โˆˆ Fin)))
14383, 142mpbid 231 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘’:๐ผโŸถโ„•0 โˆง (โ—ก๐‘’ โ€œ โ„•) โˆˆ Fin))
144143simprd 497 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (โ—ก๐‘’ โ€œ โ„•) โˆˆ Fin)
145140, 144eqeltrd 2838 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘’ supp 0) โˆˆ Fin)
14683elexd 3468 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ๐‘’ โˆˆ V)
147 isfsupp 9316 . . . . . . . . . . . . . . . . 17 ((๐‘’ โˆˆ V โˆง 0 โˆˆ V) โ†’ (๐‘’ finSupp 0 โ†” (Fun ๐‘’ โˆง (๐‘’ supp 0) โˆˆ Fin)))
148146, 134, 147sylancl 587 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘’ finSupp 0 โ†” (Fun ๐‘’ โˆง (๐‘’ supp 0) โˆˆ Fin)))
149133, 145, 148mpbir2and 712 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ๐‘’ finSupp 0)
150112, 113, 106, 106offun 7636 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ Fun (๐‘ฅ โˆ˜f โˆ’ ๐‘’))
1515psrbagfsupp 21338 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โ†’ ๐‘ฅ finSupp 0)
152109, 151syl 17 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ๐‘ฅ finSupp 0)
153152, 149fsuppunfi 9332 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ((๐‘ฅ supp 0) โˆช (๐‘’ supp 0)) โˆˆ Fin)
154 0nn0 12435 . . . . . . . . . . . . . . . . . . 19 0 โˆˆ โ„•0
155154a1i 11 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ 0 โˆˆ โ„•0)
156 0m0e0 12280 . . . . . . . . . . . . . . . . . . 19 (0 โˆ’ 0) = 0
157156a1i 11 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (0 โˆ’ 0) = 0)
158106, 155, 111, 108, 157suppofssd 8139 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ((๐‘ฅ โˆ˜f โˆ’ ๐‘’) supp 0) โŠ† ((๐‘ฅ supp 0) โˆช (๐‘’ supp 0)))
159153, 158ssfid 9218 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ((๐‘ฅ โˆ˜f โˆ’ ๐‘’) supp 0) โˆˆ Fin)
160 ovexd 7397 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆˆ V)
161 isfsupp 9316 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆˆ V โˆง 0 โˆˆ V) โ†’ ((๐‘ฅ โˆ˜f โˆ’ ๐‘’) finSupp 0 โ†” (Fun (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆง ((๐‘ฅ โˆ˜f โˆ’ ๐‘’) supp 0) โˆˆ Fin)))
162160, 134, 161sylancl 587 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ((๐‘ฅ โˆ˜f โˆ’ ๐‘’) finSupp 0 โ†” (Fun (๐‘ฅ โˆ˜f โˆ’ ๐‘’) โˆง ((๐‘ฅ โˆ˜f โˆ’ ๐‘’) supp 0) โˆˆ Fin)))
163150, 159, 162mpbir2and 712 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’) finSupp 0)
16492, 95, 99, 105, 106, 108, 132, 149, 163gsumadd 19707 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘’ โˆ˜f + (๐‘ฅ โˆ˜f โˆ’ ๐‘’))) = (((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) + ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’))))
165108ffvelcdmda 7040 . . . . . . . . . . . . . . . . . . 19 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘ โˆˆ ๐ผ) โ†’ (๐‘’โ€˜๐‘) โˆˆ โ„•0)
166165nn0cnd 12482 . . . . . . . . . . . . . . . . . 18 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘ โˆˆ ๐ผ) โ†’ (๐‘’โ€˜๐‘) โˆˆ โ„‚)
167111ffvelcdmda 7040 . . . . . . . . . . . . . . . . . . 19 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘ โˆˆ ๐ผ) โ†’ (๐‘ฅโ€˜๐‘) โˆˆ โ„•0)
168167nn0cnd 12482 . . . . . . . . . . . . . . . . . 18 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘ โˆˆ ๐ผ) โ†’ (๐‘ฅโ€˜๐‘) โˆˆ โ„‚)
169166, 168pncan3d 11522 . . . . . . . . . . . . . . . . 17 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘ โˆˆ ๐ผ) โ†’ ((๐‘’โ€˜๐‘) + ((๐‘ฅโ€˜๐‘) โˆ’ (๐‘’โ€˜๐‘))) = (๐‘ฅโ€˜๐‘))
170169mpteq2dva 5210 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘ โˆˆ ๐ผ โ†ฆ ((๐‘’โ€˜๐‘) + ((๐‘ฅโ€˜๐‘) โˆ’ (๐‘’โ€˜๐‘)))) = (๐‘ โˆˆ ๐ผ โ†ฆ (๐‘ฅโ€˜๐‘)))
171 fvexd 6862 . . . . . . . . . . . . . . . . 17 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘ โˆˆ ๐ผ) โ†’ (๐‘’โ€˜๐‘) โˆˆ V)
172 ovexd 7397 . . . . . . . . . . . . . . . . 17 (((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โˆง ๐‘ โˆˆ ๐ผ) โ†’ ((๐‘ฅโ€˜๐‘) โˆ’ (๐‘’โ€˜๐‘)) โˆˆ V)
173108feqmptd 6915 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ๐‘’ = (๐‘ โˆˆ ๐ผ โ†ฆ (๐‘’โ€˜๐‘)))
174111feqmptd 6915 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ๐‘ฅ = (๐‘ โˆˆ ๐ผ โ†ฆ (๐‘ฅโ€˜๐‘)))
175106, 167, 165, 174, 173offval2 7642 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘ฅ โˆ˜f โˆ’ ๐‘’) = (๐‘ โˆˆ ๐ผ โ†ฆ ((๐‘ฅโ€˜๐‘) โˆ’ (๐‘’โ€˜๐‘))))
176106, 171, 172, 173, 175offval2 7642 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘’ โˆ˜f + (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) = (๐‘ โˆˆ ๐ผ โ†ฆ ((๐‘’โ€˜๐‘) + ((๐‘ฅโ€˜๐‘) โˆ’ (๐‘’โ€˜๐‘)))))
177170, 176, 1743eqtr4d 2787 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (๐‘’ โˆ˜f + (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) = ๐‘ฅ)
178177oveq2d 7378 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘’ โˆ˜f + (๐‘ฅ โˆ˜f โˆ’ ๐‘’))) = ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ))
179164, 178eqtr3d 2779 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) + ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’))) = ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ))
180 simplr 768 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘))
181179, 180eqnetrd 3012 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) + ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’))) โ‰  (๐‘€ + ๐‘))
182 oveq12 7371 . . . . . . . . . . . . . 14 ((((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) = ๐‘€ โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) = ๐‘) โ†’ (((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) + ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’))) = (๐‘€ + ๐‘))
183182a1i 11 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ((((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) = ๐‘€ โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) = ๐‘) โ†’ (((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) + ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’))) = (๐‘€ + ๐‘)))
184183necon3ad 2957 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ((((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) + ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’))) โ‰  (๐‘€ + ๐‘) โ†’ ยฌ (((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) = ๐‘€ โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) = ๐‘)))
185181, 184mpd 15 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ยฌ (((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) = ๐‘€ โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) = ๐‘))
186 neorian 3040 . . . . . . . . . . 11 ((((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€ โˆจ ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘) โ†” ยฌ (((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) = ๐‘€ โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) = ๐‘))
187185, 186sylibr 233 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ (((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘’) โ‰  ๐‘€ โˆจ ((โ„‚fld โ†พs โ„•0) ฮฃg (๐‘ฅ โˆ˜f โˆ’ ๐‘’)) โ‰  ๐‘))
18862, 88, 187mpjaodan 958 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โˆง ๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ}) โ†’ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))) = (0gโ€˜๐‘…))
189188mpteq2dva 5210 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โ†’ (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’)))) = (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ (0gโ€˜๐‘…)))
190189oveq2d 7378 . . . . . . 7 (((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โ†’ (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))))) = (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ (0gโ€˜๐‘…))))
191 ringmnd 19981 . . . . . . . . . 10 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ Mnd)
1928, 191syl 17 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘… โˆˆ Mnd)
193192ad2antrr 725 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โ†’ ๐‘… โˆˆ Mnd)
19444rabex 5294 . . . . . . . 8 {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โˆˆ V
19541gsumz 18653 . . . . . . . 8 ((๐‘… โˆˆ Mnd โˆง {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โˆˆ V) โ†’ (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ (0gโ€˜๐‘…))) = (0gโ€˜๐‘…))
196193, 194, 195sylancl 587 . . . . . . 7 (((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โ†’ (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ (0gโ€˜๐‘…))) = (0gโ€˜๐‘…))
197190, 196eqtrd 2777 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โˆง ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘)) โ†’ (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))))) = (0gโ€˜๐‘…))
198197ex 414 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โ†’ (((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) โ‰  (๐‘€ + ๐‘) โ†’ (๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))))) = (0gโ€˜๐‘…)))
199198necon1d 2966 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โ†’ ((๐‘… ฮฃg (๐‘’ โˆˆ {๐‘ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ} โ†ฆ ((๐‘ƒโ€˜๐‘’)(.rโ€˜๐‘…)(๐‘„โ€˜(๐‘ฅ โˆ˜f โˆ’ ๐‘’))))) โ‰  (0gโ€˜๐‘…) โ†’ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) = (๐‘€ + ๐‘)))
20027, 199sylbid 239 . . 3 ((๐œ‘ โˆง ๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin}) โ†’ (((๐‘ƒ ยท ๐‘„)โ€˜๐‘ฅ) โ‰  (0gโ€˜๐‘…) โ†’ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) = (๐‘€ + ๐‘)))
201200ralrimiva 3144 . 2 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} (((๐‘ƒ ยท ๐‘„)โ€˜๐‘ฅ) โ‰  (0gโ€˜๐‘…) โ†’ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) = (๐‘€ + ๐‘)))
2029, 12nn0addcld 12484 . . 3 (๐œ‘ โ†’ (๐‘€ + ๐‘) โˆˆ โ„•0)
2031mplring 21440 . . . . 5 ((๐ผ โˆˆ ๐‘‰ โˆง ๐‘… โˆˆ Ring) โ†’ ๐‘Œ โˆˆ Ring)
2047, 8, 203syl2anc 585 . . . 4 (๐œ‘ โ†’ ๐‘Œ โˆˆ Ring)
2052, 4ringcl 19988 . . . 4 ((๐‘Œ โˆˆ Ring โˆง ๐‘ƒ โˆˆ (Baseโ€˜๐‘Œ) โˆง ๐‘„ โˆˆ (Baseโ€˜๐‘Œ)) โ†’ (๐‘ƒ ยท ๐‘„) โˆˆ (Baseโ€˜๐‘Œ))
206204, 11, 14, 205syl3anc 1372 . . 3 (๐œ‘ โ†’ (๐‘ƒ ยท ๐‘„) โˆˆ (Baseโ€˜๐‘Œ))
2076, 1, 2, 41, 5, 7, 8, 202, 206ismhp3 21549 . 2 (๐œ‘ โ†’ ((๐‘ƒ ยท ๐‘„) โˆˆ (๐ปโ€˜(๐‘€ + ๐‘)) โ†” โˆ€๐‘ฅ โˆˆ {โ„Ž โˆˆ (โ„•0 โ†‘m ๐ผ) โˆฃ (โ—กโ„Ž โ€œ โ„•) โˆˆ Fin} (((๐‘ƒ ยท ๐‘„)โ€˜๐‘ฅ) โ‰  (0gโ€˜๐‘…) โ†’ ((โ„‚fld โ†พs โ„•0) ฮฃg ๐‘ฅ) = (๐‘€ + ๐‘))))
208201, 207mpbird 257 1 (๐œ‘ โ†’ (๐‘ƒ ยท ๐‘„) โˆˆ (๐ปโ€˜(๐‘€ + ๐‘)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆ€wral 3065  {crab 3410  Vcvv 3448   โˆ– cdif 3912   โˆช cun 3913  {csn 4591   class class class wbr 5110   โ†ฆ cmpt 5193  โ—กccnv 5637   โ€œ cima 5641  Fun wfun 6495  โŸถwf 6497  โ€˜cfv 6501  (class class class)co 7362   โˆ˜f cof 7620   โˆ˜r cofr 7621   supp csupp 8097   โ†‘m cmap 8772  Fincfn 8890   finSupp cfsupp 9312  0cc0 11058   + caddc 11061   โ‰ค cle 11197   โˆ’ cmin 11392  โ„•cn 12160  โ„•0cn0 12420  Basecbs 17090   โ†พs cress 17119  +gcplusg 17140  .rcmulr 17141  0gc0g 17328   ฮฃg cgsu 17329  Mndcmnd 18563  SubMndcsubmnd 18607  CMndccmn 19569  Ringcrg 19971  โ„‚fldccnfld 20812   mPoly cmpl 21324   mHomP cmhp 21535
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-addf 11137  ax-mulf 11138
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-ofr 7623  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-sup 9385  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-fz 13432  df-fzo 13575  df-seq 13914  df-hash 14238  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-0g 17330  df-gsum 17331  df-prds 17336  df-pws 17338  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-mhm 18608  df-submnd 18609  df-grp 18758  df-minusg 18759  df-mulg 18880  df-subg 18932  df-ghm 19013  df-cntz 19104  df-cmn 19571  df-abl 19572  df-mgp 19904  df-ur 19921  df-ring 19973  df-cring 19974  df-subrg 20236  df-cnfld 20813  df-psr 21327  df-mpl 21329  df-mhp 21539
This theorem is referenced by:  mhppwdeg  21556
  Copyright terms: Public domain W3C validator