Metamath Proof Explorer

Theorem mhpmulcl

Description: A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024)

Ref Expression
Hypotheses 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 mhpmulcl ( ๐œ‘ โ†’ ( ๐‘ƒ ยท ๐‘„ ) โˆˆ ( ๐ป โ€˜ ( ๐‘€ + ๐‘ ) ) )

Proof

Step Hyp Ref Expression
1 mhpmulcl.h โŠข ๐ป = ( ๐ผ mHomP ๐‘… )
2 mhpmulcl.y โŠข ๐‘Œ = ( ๐ผ mPoly ๐‘… )
3 mhpmulcl.t โŠข ยท = ( .r โ€˜ ๐‘Œ )
4 mhpmulcl.i โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ ๐‘‰ )
5 mhpmulcl.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
6 mhpmulcl.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0 )
7 mhpmulcl.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„•0 )
8 mhpmulcl.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ ( ๐ป โ€˜ ๐‘€ ) )
9 mhpmulcl.q โŠข ( ๐œ‘ โ†’ ๐‘„ โˆˆ ( ๐ป โ€˜ ๐‘ ) )
10 eqid โŠข ( Base โ€˜ ๐‘Œ ) = ( Base โ€˜ ๐‘Œ )
11 eqid โŠข ( .r โ€˜ ๐‘… ) = ( .r โ€˜ ๐‘… )
12 eqid โŠข { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } = { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin }
13 1 2 10 4 5 6 8 mhpmpl โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ ( Base โ€˜ ๐‘Œ ) )
14 1 2 10 4 5 7 9 mhpmpl โŠข ( ๐œ‘ โ†’ ๐‘„ โˆˆ ( Base โ€˜ ๐‘Œ ) )
15 2 10 11 3 12 13 14 mplmul โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ ยท ๐‘„ ) = ( ๐‘‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โ†ฆ ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘‘ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘‘ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) ) )
16 15 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โ†’ ( ๐‘ƒ ยท ๐‘„ ) = ( ๐‘‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โ†ฆ ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘‘ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘‘ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) ) )
17 breq2 โŠข ( ๐‘‘ = ๐‘ฅ โ†’ ( ๐‘ โˆ˜r โ‰ค ๐‘‘ โ†” ๐‘ โˆ˜r โ‰ค ๐‘ฅ ) )
18 17 rabbidv โŠข ( ๐‘‘ = ๐‘ฅ โ†’ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘‘ } = { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } )
19 fvoveq1 โŠข ( ๐‘‘ = ๐‘ฅ โ†’ ( ๐‘„ โ€˜ ( ๐‘‘ โˆ˜f โˆ’ ๐‘’ ) ) = ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) )
20 19 oveq2d โŠข ( ๐‘‘ = ๐‘ฅ โ†’ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘‘ โˆ˜f โˆ’ ๐‘’ ) ) ) = ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) )
21 18 20 mpteq12dv โŠข ( ๐‘‘ = ๐‘ฅ โ†’ ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘‘ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘‘ โˆ˜f โˆ’ ๐‘’ ) ) ) ) = ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) ) )
22 21 oveq2d โŠข ( ๐‘‘ = ๐‘ฅ โ†’ ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘‘ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘‘ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) = ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) )
23 22 adantl โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ๐‘‘ = ๐‘ฅ ) โ†’ ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘‘ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘‘ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) = ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) )
24 simpr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โ†’ ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } )
25 ovexd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โ†’ ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) โˆˆ V )
26 16 23 24 25 fvmptd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โ†’ ( ( ๐‘ƒ ยท ๐‘„ ) โ€˜ ๐‘ฅ ) = ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) )
27 26 neeq1d โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โ†’ ( ( ( ๐‘ƒ ยท ๐‘„ ) โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ๐‘… ) โ†” ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) โ‰  ( 0g โ€˜ ๐‘… ) ) )
28 simp-4l โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ๐œ‘ )
29 oveq2 โŠข ( ๐‘ = ๐‘’ โ†’ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) )
30 29 eqeq1d โŠข ( ๐‘ = ๐‘’ โ†’ ( ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘€ โ†” ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) = ๐‘€ ) )
31 30 necon3bbid โŠข ( ๐‘ = ๐‘’ โ†’ ( ยฌ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘€ โ†” ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) )
32 simplr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } )
33 elrabi โŠข ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†’ ๐‘’ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } )
34 32 33 syl โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ๐‘’ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } )
35 simpr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ )
36 31 34 35 elrabd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ยฌ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘€ } )
37 notrab โŠข ( { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆ– { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘€ } ) = { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ยฌ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘€ }
38 36 37 eleqtrrdi โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•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 โŠข ( Base โ€˜ ๐‘… ) = ( Base โ€˜ ๐‘… )
40 2 39 10 12 13 mplelf โŠข ( ๐œ‘ โ†’ ๐‘ƒ : { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โŸถ ( Base โ€˜ ๐‘… ) )
41 eqid โŠข ( 0g โ€˜ ๐‘… ) = ( 0g โ€˜ ๐‘… )
42 1 41 12 4 5 6 8 mhpdeg โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ supp ( 0g โ€˜ ๐‘… ) ) โŠ† { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘€ } )
43 ovex โŠข ( โ„•0 โ†‘m ๐ผ ) โˆˆ V
44 43 rabex โŠข { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆˆ V
45 44 a1i โŠข ( ๐œ‘ โ†’ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆˆ V )
46 fvexd โŠข ( ๐œ‘ โ†’ ( 0g โ€˜ ๐‘… ) โˆˆ V )
47 40 42 45 46 suppssr โŠข ( ( ๐œ‘ โˆง ๐‘’ โˆˆ ( { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆ– { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘€ } ) ) โ†’ ( ๐‘ƒ โ€˜ ๐‘’ ) = ( 0g โ€˜ ๐‘… ) )
48 28 38 47 syl2anc โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ( ๐‘ƒ โ€˜ ๐‘’ ) = ( 0g โ€˜ ๐‘… ) )
49 48 oveq1d โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) = ( ( 0g โ€˜ ๐‘… ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) )
50 5 ad4antr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ๐‘… โˆˆ Ring )
51 14 ad4antr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ๐‘„ โˆˆ ( Base โ€˜ ๐‘Œ ) )
52 2 39 10 12 51 mplelf โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ๐‘„ : { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โŸถ ( Base โ€˜ ๐‘… ) )
53 simp-4r โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } )
54 eqid โŠข { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } = { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ }
55 12 54 psrbagconcl โŠข ( ( ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } )
56 53 32 55 syl2anc โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } )
57 elrabi โŠข ( ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†’ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } )
58 56 57 syl โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } )
59 52 58 ffvelcdmd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โˆˆ ( Base โ€˜ ๐‘… ) )
60 39 11 41 ringlz โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โˆˆ ( Base โ€˜ ๐‘… ) ) โ†’ ( ( 0g โ€˜ ๐‘… ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) = ( 0g โ€˜ ๐‘… ) )
61 50 59 60 syl2anc โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ( ( 0g โ€˜ ๐‘… ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) = ( 0g โ€˜ ๐‘… ) )
62 49 61 eqtrd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ ) โ†’ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) = ( 0g โ€˜ ๐‘… ) )
63 simp-4l โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ๐œ‘ )
64 oveq2 โŠข ( ๐‘ = ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โ†’ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) )
65 64 eqeq1d โŠข ( ๐‘ = ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โ†’ ( ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘ โ†” ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) = ๐‘ ) )
66 65 necon3bbid โŠข ( ๐‘ = ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โ†’ ( ยฌ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘ โ†” ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) )
67 simp-4r โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } )
68 simplr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } )
69 67 68 55 syl2anc โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } )
70 69 57 syl โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } )
71 simpr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ )
72 66 70 71 elrabd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•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 โŠข ( { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆ– { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘ } ) = { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ยฌ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘ }
74 72 73 eleqtrrdi โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•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 ๐‘ ) = ๐‘ } ) )
75 2 39 10 12 14 mplelf โŠข ( ๐œ‘ โ†’ ๐‘„ : { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โŸถ ( Base โ€˜ ๐‘… ) )
76 1 41 12 4 5 7 9 mhpdeg โŠข ( ๐œ‘ โ†’ ( ๐‘„ supp ( 0g โ€˜ ๐‘… ) ) โŠ† { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘ } )
77 75 76 45 46 suppssr โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โˆˆ ( { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆ– { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ ) = ๐‘ } ) ) โ†’ ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) = ( 0g โ€˜ ๐‘… ) )
78 63 74 77 syl2anc โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) = ( 0g โ€˜ ๐‘… ) )
79 78 oveq2d โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) = ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( 0g โ€˜ ๐‘… ) ) )
80 5 ad4antr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ๐‘… โˆˆ Ring )
81 13 ad4antr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ๐‘ƒ โˆˆ ( Base โ€˜ ๐‘Œ ) )
82 2 39 10 12 81 mplelf โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ๐‘ƒ : { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โŸถ ( Base โ€˜ ๐‘… ) )
83 33 adantl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ๐‘’ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } )
84 83 adantr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ๐‘’ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } )
85 82 84 ffvelcdmd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ( ๐‘ƒ โ€˜ ๐‘’ ) โˆˆ ( Base โ€˜ ๐‘… ) )
86 39 11 41 ringrz โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ƒ โ€˜ ๐‘’ ) โˆˆ ( Base โ€˜ ๐‘… ) ) โ†’ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( 0g โ€˜ ๐‘… ) ) = ( 0g โ€˜ ๐‘… ) )
87 80 85 86 syl2anc โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( 0g โ€˜ ๐‘… ) ) = ( 0g โ€˜ ๐‘… ) )
88 79 87 eqtrd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†’ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) = ( 0g โ€˜ ๐‘… ) )
89 nn0subm โŠข โ„•0 โˆˆ ( SubMnd โ€˜ โ„‚fld )
90 eqid โŠข ( โ„‚fld โ†พs โ„•0 ) = ( โ„‚fld โ†พs โ„•0 )
91 90 submbas โŠข ( โ„•0 โˆˆ ( SubMnd โ€˜ โ„‚fld ) โ†’ โ„•0 = ( Base โ€˜ ( โ„‚fld โ†พs โ„•0 ) ) )
92 89 91 ax-mp โŠข โ„•0 = ( Base โ€˜ ( โ„‚fld โ†พs โ„•0 ) )
93 cnfld0 โŠข 0 = ( 0g โ€˜ โ„‚fld )
94 90 93 subm0 โŠข ( โ„•0 โˆˆ ( SubMnd โ€˜ โ„‚fld ) โ†’ 0 = ( 0g โ€˜ ( โ„‚fld โ†พs โ„•0 ) ) )
95 89 94 ax-mp โŠข 0 = ( 0g โ€˜ ( โ„‚fld โ†พs โ„•0 ) )
96 nn0ex โŠข โ„•0 โˆˆ V
97 cnfldadd โŠข + = ( +g โ€˜ โ„‚fld )
98 90 97 ressplusg โŠข ( โ„•0 โˆˆ V โ†’ + = ( +g โ€˜ ( โ„‚fld โ†พs โ„•0 ) ) )
99 96 98 ax-mp โŠข + = ( +g โ€˜ ( โ„‚fld โ†พs โ„•0 ) )
100 cnring โŠข โ„‚fld โˆˆ Ring
101 ringcmn โŠข ( โ„‚fld โˆˆ Ring โ†’ โ„‚fld โˆˆ CMnd )
102 100 101 ax-mp โŠข โ„‚fld โˆˆ CMnd
103 90 submcmn โŠข ( ( โ„‚fld โˆˆ CMnd โˆง โ„•0 โˆˆ ( SubMnd โ€˜ โ„‚fld ) ) โ†’ ( โ„‚fld โ†พs โ„•0 ) โˆˆ CMnd )
104 102 89 103 mp2an โŠข ( โ„‚fld โ†พs โ„•0 ) โˆˆ CMnd
105 104 a1i โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( โ„‚fld โ†พs โ„•0 ) โˆˆ CMnd )
106 4 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ๐ผ โˆˆ ๐‘‰ )
107 12 psrbagf โŠข ( ๐‘’ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โ†’ ๐‘’ : ๐ผ โŸถ โ„•0 )
108 83 107 syl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ๐‘’ : ๐ผ โŸถ โ„•0 )
109 simpllr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } )
110 12 psrbagf โŠข ( ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โ†’ ๐‘ฅ : ๐ผ โŸถ โ„•0 )
111 109 110 syl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ๐‘ฅ : ๐ผ โŸถ โ„•0 )
112 111 ffnd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ๐‘ฅ Fn ๐ผ )
113 108 ffnd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ๐‘’ Fn ๐ผ )
114 inidm โŠข ( ๐ผ โˆฉ ๐ผ ) = ๐ผ
115 eqidd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘– โˆˆ ๐ผ ) โ†’ ( ๐‘ฅ โ€˜ ๐‘– ) = ( ๐‘ฅ โ€˜ ๐‘– ) )
116 eqidd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘– โˆˆ ๐ผ ) โ†’ ( ๐‘’ โ€˜ ๐‘– ) = ( ๐‘’ โ€˜ ๐‘– ) )
117 112 113 106 106 114 115 116 offval โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) = ( ๐‘– โˆˆ ๐ผ โ†ฆ ( ( ๐‘ฅ โ€˜ ๐‘– ) โˆ’ ( ๐‘’ โ€˜ ๐‘– ) ) ) )
118 simpl โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘– โˆˆ ๐ผ ) โ†’ ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) )
119 simplr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘– โˆˆ ๐ผ ) โ†’ ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } )
120 breq1 โŠข ( ๐‘ = ๐‘’ โ†’ ( ๐‘ โˆ˜r โ‰ค ๐‘ฅ โ†” ๐‘’ โˆ˜r โ‰ค ๐‘ฅ ) )
121 120 elrab โŠข ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†” ( ๐‘’ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆง ๐‘’ โˆ˜r โ‰ค ๐‘ฅ ) )
122 121 simprbi โŠข ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†’ ๐‘’ โˆ˜r โ‰ค ๐‘ฅ )
123 119 122 syl โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘– โˆˆ ๐ผ ) โ†’ ๐‘’ โˆ˜r โ‰ค ๐‘ฅ )
124 simpr โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘– โˆˆ ๐ผ ) โ†’ ๐‘– โˆˆ ๐ผ )
125 113 112 106 106 114 116 115 ofrval โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘’ โˆ˜r โ‰ค ๐‘ฅ โˆง ๐‘– โˆˆ ๐ผ ) โ†’ ( ๐‘’ โ€˜ ๐‘– ) โ‰ค ( ๐‘ฅ โ€˜ ๐‘– ) )
126 118 123 124 125 syl3anc โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘– โˆˆ ๐ผ ) โ†’ ( ๐‘’ โ€˜ ๐‘– ) โ‰ค ( ๐‘ฅ โ€˜ ๐‘– ) )
127 108 ffvelcdmda โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘– โˆˆ ๐ผ ) โ†’ ( ๐‘’ โ€˜ ๐‘– ) โˆˆ โ„•0 )
128 111 ffvelcdmda โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘– โˆˆ ๐ผ ) โ†’ ( ๐‘ฅ โ€˜ ๐‘– ) โˆˆ โ„•0 )
129 nn0sub โŠข ( ( ( ๐‘’ โ€˜ ๐‘– ) โˆˆ โ„•0 โˆง ( ๐‘ฅ โ€˜ ๐‘– ) โˆˆ โ„•0 ) โ†’ ( ( ๐‘’ โ€˜ ๐‘– ) โ‰ค ( ๐‘ฅ โ€˜ ๐‘– ) โ†” ( ( ๐‘ฅ โ€˜ ๐‘– ) โˆ’ ( ๐‘’ โ€˜ ๐‘– ) ) โˆˆ โ„•0 ) )
130 127 128 129 syl2anc โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘– โˆˆ ๐ผ ) โ†’ ( ( ๐‘’ โ€˜ ๐‘– ) โ‰ค ( ๐‘ฅ โ€˜ ๐‘– ) โ†” ( ( ๐‘ฅ โ€˜ ๐‘– ) โˆ’ ( ๐‘’ โ€˜ ๐‘– ) ) โˆˆ โ„•0 ) )
131 126 130 mpbid โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘– โˆˆ ๐ผ ) โ†’ ( ( ๐‘ฅ โ€˜ ๐‘– ) โˆ’ ( ๐‘’ โ€˜ ๐‘– ) ) โˆˆ โ„•0 )
132 117 131 fmpt3d โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) : ๐ผ โŸถ โ„•0 )
133 108 ffund โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ Fun ๐‘’ )
134 c0ex โŠข 0 โˆˆ V
135 106 134 jctir โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐ผ โˆˆ ๐‘‰ โˆง 0 โˆˆ V ) )
136 fsuppeq โŠข ( ( ๐ผ โˆˆ ๐‘‰ โˆง 0 โˆˆ V ) โ†’ ( ๐‘’ : ๐ผ โŸถ โ„•0 โ†’ ( ๐‘’ supp 0 ) = ( โ—ก ๐‘’ โ€œ ( โ„•0 โˆ– { 0 } ) ) ) )
137 135 108 136 sylc โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘’ supp 0 ) = ( โ—ก ๐‘’ โ€œ ( โ„•0 โˆ– { 0 } ) ) )
138 dfn2 โŠข โ„• = ( โ„•0 โˆ– { 0 } )
139 138 imaeq2i โŠข ( โ—ก ๐‘’ โ€œ โ„• ) = ( โ—ก ๐‘’ โ€œ ( โ„•0 โˆ– { 0 } ) )
140 137 139 eqtr4di โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘’ supp 0 ) = ( โ—ก ๐‘’ โ€œ โ„• ) )
141 12 psrbag โŠข ( ๐ผ โˆˆ ๐‘‰ โ†’ ( ๐‘’ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โ†” ( ๐‘’ : ๐ผ โŸถ โ„•0 โˆง ( โ—ก ๐‘’ โ€œ โ„• ) โˆˆ Fin ) ) )
142 106 141 syl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘’ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โ†” ( ๐‘’ : ๐ผ โŸถ โ„•0 โˆง ( โ—ก ๐‘’ โ€œ โ„• ) โˆˆ Fin ) ) )
143 83 142 mpbid โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘’ : ๐ผ โŸถ โ„•0 โˆง ( โ—ก ๐‘’ โ€œ โ„• ) โˆˆ Fin ) )
144 143 simprd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( โ—ก ๐‘’ โ€œ โ„• ) โˆˆ Fin )
145 140 144 eqeltrd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘’ supp 0 ) โˆˆ Fin )
146 83 elexd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ๐‘’ โˆˆ V )
147 isfsupp โŠข ( ( ๐‘’ โˆˆ V โˆง 0 โˆˆ V ) โ†’ ( ๐‘’ finSupp 0 โ†” ( Fun ๐‘’ โˆง ( ๐‘’ supp 0 ) โˆˆ Fin ) ) )
148 146 134 147 sylancl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘’ finSupp 0 โ†” ( Fun ๐‘’ โˆง ( ๐‘’ supp 0 ) โˆˆ Fin ) ) )
149 133 145 148 mpbir2and โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ๐‘’ finSupp 0 )
150 112 113 106 106 offun โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ Fun ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) )
151 12 psrbagfsupp โŠข ( ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โ†’ ๐‘ฅ finSupp 0 )
152 109 151 syl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ๐‘ฅ finSupp 0 )
153 152 149 fsuppunfi โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ( ๐‘ฅ supp 0 ) โˆช ( ๐‘’ supp 0 ) ) โˆˆ Fin )
154 0nn0 โŠข 0 โˆˆ โ„•0
155 154 a1i โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ 0 โˆˆ โ„•0 )
156 0m0e0 โŠข ( 0 โˆ’ 0 ) = 0
157 156 a1i โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( 0 โˆ’ 0 ) = 0 )
158 106 155 111 108 157 suppofssd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) supp 0 ) โŠ† ( ( ๐‘ฅ supp 0 ) โˆช ( ๐‘’ supp 0 ) ) )
159 153 158 ssfid โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) supp 0 ) โˆˆ Fin )
160 ovexd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โˆˆ V )
161 isfsupp โŠข ( ( ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โˆˆ V โˆง 0 โˆˆ V ) โ†’ ( ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) finSupp 0 โ†” ( Fun ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โˆง ( ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) supp 0 ) โˆˆ Fin ) ) )
162 160 134 161 sylancl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) finSupp 0 โ†” ( Fun ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) โˆง ( ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) supp 0 ) โˆˆ Fin ) ) )
163 150 159 162 mpbir2and โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) finSupp 0 )
164 92 95 99 105 106 108 132 149 163 gsumadd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•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 โˆ’ ๐‘’ ) ) ) )
165 108 ffvelcdmda โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘ โˆˆ ๐ผ ) โ†’ ( ๐‘’ โ€˜ ๐‘ ) โˆˆ โ„•0 )
166 165 nn0cnd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘ โˆˆ ๐ผ ) โ†’ ( ๐‘’ โ€˜ ๐‘ ) โˆˆ โ„‚ )
167 111 ffvelcdmda โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘ โˆˆ ๐ผ ) โ†’ ( ๐‘ฅ โ€˜ ๐‘ ) โˆˆ โ„•0 )
168 167 nn0cnd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘ โˆˆ ๐ผ ) โ†’ ( ๐‘ฅ โ€˜ ๐‘ ) โˆˆ โ„‚ )
169 166 168 pncan3d โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘ โˆˆ ๐ผ ) โ†’ ( ( ๐‘’ โ€˜ ๐‘ ) + ( ( ๐‘ฅ โ€˜ ๐‘ ) โˆ’ ( ๐‘’ โ€˜ ๐‘ ) ) ) = ( ๐‘ฅ โ€˜ ๐‘ ) )
170 169 mpteq2dva โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘ โˆˆ ๐ผ โ†ฆ ( ( ๐‘’ โ€˜ ๐‘ ) + ( ( ๐‘ฅ โ€˜ ๐‘ ) โˆ’ ( ๐‘’ โ€˜ ๐‘ ) ) ) ) = ( ๐‘ โˆˆ ๐ผ โ†ฆ ( ๐‘ฅ โ€˜ ๐‘ ) ) )
171 fvexd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘ โˆˆ ๐ผ ) โ†’ ( ๐‘’ โ€˜ ๐‘ ) โˆˆ V )
172 ovexd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โˆง ๐‘ โˆˆ ๐ผ ) โ†’ ( ( ๐‘ฅ โ€˜ ๐‘ ) โˆ’ ( ๐‘’ โ€˜ ๐‘ ) ) โˆˆ V )
173 108 feqmptd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ๐‘’ = ( ๐‘ โˆˆ ๐ผ โ†ฆ ( ๐‘’ โ€˜ ๐‘ ) ) )
174 111 feqmptd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ๐‘ฅ = ( ๐‘ โˆˆ ๐ผ โ†ฆ ( ๐‘ฅ โ€˜ ๐‘ ) ) )
175 106 167 165 174 173 offval2 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) = ( ๐‘ โˆˆ ๐ผ โ†ฆ ( ( ๐‘ฅ โ€˜ ๐‘ ) โˆ’ ( ๐‘’ โ€˜ ๐‘ ) ) ) )
176 106 171 172 173 175 offval2 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘’ โˆ˜f + ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) = ( ๐‘ โˆˆ ๐ผ โ†ฆ ( ( ๐‘’ โ€˜ ๐‘ ) + ( ( ๐‘ฅ โ€˜ ๐‘ ) โˆ’ ( ๐‘’ โ€˜ ๐‘ ) ) ) ) )
177 170 176 174 3eqtr4d โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ๐‘’ โˆ˜f + ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) = ๐‘ฅ )
178 177 oveq2d โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘’ โˆ˜f + ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) = ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) )
179 164 178 eqtr3d โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•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 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) )
181 179 180 eqnetrd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) + ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) โ‰  ( ๐‘€ + ๐‘ ) )
182 oveq12 โŠข ( ( ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) = ๐‘€ โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) = ๐‘ ) โ†’ ( ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) + ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) = ( ๐‘€ + ๐‘ ) )
183 182 a1i โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•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 โˆ’ ๐‘’ ) ) ) = ( ๐‘€ + ๐‘ ) ) )
184 183 necon3ad โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•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 โˆ’ ๐‘’ ) ) = ๐‘ ) ) )
185 181 184 mpd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ยฌ ( ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) = ๐‘€ โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) = ๐‘ ) )
186 neorian โŠข ( ( ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ โˆจ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) โ†” ยฌ ( ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) = ๐‘€ โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) = ๐‘ ) )
187 185 186 sylibr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘’ ) โ‰  ๐‘€ โˆจ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) โ‰  ๐‘ ) )
188 62 88 187 mpjaodan โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โˆง ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } ) โ†’ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) = ( 0g โ€˜ ๐‘… ) )
189 188 mpteq2dva โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โ†’ ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) ) = ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( 0g โ€˜ ๐‘… ) ) )
190 189 oveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โ†’ ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) = ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( 0g โ€˜ ๐‘… ) ) ) )
191 ringmnd โŠข ( ๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ Mnd )
192 5 191 syl โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Mnd )
193 192 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โ†’ ๐‘… โˆˆ Mnd )
194 44 rabex โŠข { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โˆˆ V
195 41 gsumz โŠข ( ( ๐‘… โˆˆ Mnd โˆง { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โˆˆ V ) โ†’ ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( 0g โ€˜ ๐‘… ) ) ) = ( 0g โ€˜ ๐‘… ) )
196 193 194 195 sylancl โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โ†’ ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( 0g โ€˜ ๐‘… ) ) ) = ( 0g โ€˜ ๐‘… ) )
197 190 196 eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โˆง ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) ) โ†’ ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) = ( 0g โ€˜ ๐‘… ) )
198 197 ex โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โ†’ ( ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) โ‰  ( ๐‘€ + ๐‘ ) โ†’ ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) = ( 0g โ€˜ ๐‘… ) ) )
199 198 necon1d โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โ†’ ( ( ๐‘… ฮฃg ( ๐‘’ โˆˆ { ๐‘ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } โˆฃ ๐‘ โˆ˜r โ‰ค ๐‘ฅ } โ†ฆ ( ( ๐‘ƒ โ€˜ ๐‘’ ) ( .r โ€˜ ๐‘… ) ( ๐‘„ โ€˜ ( ๐‘ฅ โˆ˜f โˆ’ ๐‘’ ) ) ) ) ) โ‰  ( 0g โ€˜ ๐‘… ) โ†’ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) = ( ๐‘€ + ๐‘ ) ) )
200 27 199 sylbid โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ) โ†’ ( ( ( ๐‘ƒ ยท ๐‘„ ) โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ๐‘… ) โ†’ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) = ( ๐‘€ + ๐‘ ) ) )
201 200 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ( ( ( ๐‘ƒ ยท ๐‘„ ) โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ๐‘… ) โ†’ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) = ( ๐‘€ + ๐‘ ) ) )
202 6 7 nn0addcld โŠข ( ๐œ‘ โ†’ ( ๐‘€ + ๐‘ ) โˆˆ โ„•0 )
203 2 mplring โŠข ( ( ๐ผ โˆˆ ๐‘‰ โˆง ๐‘… โˆˆ Ring ) โ†’ ๐‘Œ โˆˆ Ring )
204 4 5 203 syl2anc โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ Ring )
205 10 3 ringcl โŠข ( ( ๐‘Œ โˆˆ Ring โˆง ๐‘ƒ โˆˆ ( Base โ€˜ ๐‘Œ ) โˆง ๐‘„ โˆˆ ( Base โ€˜ ๐‘Œ ) ) โ†’ ( ๐‘ƒ ยท ๐‘„ ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
206 204 13 14 205 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ ยท ๐‘„ ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
207 1 2 10 41 12 4 5 202 206 ismhp3 โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ ยท ๐‘„ ) โˆˆ ( ๐ป โ€˜ ( ๐‘€ + ๐‘ ) ) โ†” โˆ€ ๐‘ฅ โˆˆ { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin } ( ( ( ๐‘ƒ ยท ๐‘„ ) โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ๐‘… ) โ†’ ( ( โ„‚fld โ†พs โ„•0 ) ฮฃg ๐‘ฅ ) = ( ๐‘€ + ๐‘ ) ) ) )
208 201 207 mpbird โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ ยท ๐‘„ ) โˆˆ ( ๐ป โ€˜ ( ๐‘€ + ๐‘ ) ) )