Metamath Proof Explorer


Theorem stoweidlem30

Description: This lemma is used to prove the existence of a function p as in Lemma 1 BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 <= p <= 1, p__(t_0) = 0, and p > 0 on T - U. Z is used for t_0, P is used for p, ( Gi ) is used for p__(t_i). (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem30.1 โŠข ๐‘„ = { โ„Ž โˆˆ ๐ด โˆฃ ( ( โ„Ž โ€˜ ๐‘ ) = 0 โˆง โˆ€ ๐‘ก โˆˆ ๐‘‡ ( 0 โ‰ค ( โ„Ž โ€˜ ๐‘ก ) โˆง ( โ„Ž โ€˜ ๐‘ก ) โ‰ค 1 ) ) }
stoweidlem30.2 โŠข ๐‘ƒ = ( ๐‘ก โˆˆ ๐‘‡ โ†ฆ ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘ก ) ) )
stoweidlem30.3 โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
stoweidlem30.4 โŠข ( ๐œ‘ โ†’ ๐บ : ( 1 ... ๐‘€ ) โŸถ ๐‘„ )
stoweidlem30.5 โŠข ( ( ๐œ‘ โˆง ๐‘“ โˆˆ ๐ด ) โ†’ ๐‘“ : ๐‘‡ โŸถ โ„ )
Assertion stoweidlem30 ( ( ๐œ‘ โˆง ๐‘† โˆˆ ๐‘‡ ) โ†’ ( ๐‘ƒ โ€˜ ๐‘† ) = ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘† ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem30.1 โŠข ๐‘„ = { โ„Ž โˆˆ ๐ด โˆฃ ( ( โ„Ž โ€˜ ๐‘ ) = 0 โˆง โˆ€ ๐‘ก โˆˆ ๐‘‡ ( 0 โ‰ค ( โ„Ž โ€˜ ๐‘ก ) โˆง ( โ„Ž โ€˜ ๐‘ก ) โ‰ค 1 ) ) }
2 stoweidlem30.2 โŠข ๐‘ƒ = ( ๐‘ก โˆˆ ๐‘‡ โ†ฆ ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘ก ) ) )
3 stoweidlem30.3 โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
4 stoweidlem30.4 โŠข ( ๐œ‘ โ†’ ๐บ : ( 1 ... ๐‘€ ) โŸถ ๐‘„ )
5 stoweidlem30.5 โŠข ( ( ๐œ‘ โˆง ๐‘“ โˆˆ ๐ด ) โ†’ ๐‘“ : ๐‘‡ โŸถ โ„ )
6 eleq1 โŠข ( ๐‘  = ๐‘† โ†’ ( ๐‘  โˆˆ ๐‘‡ โ†” ๐‘† โˆˆ ๐‘‡ ) )
7 6 anbi2d โŠข ( ๐‘  = ๐‘† โ†’ ( ( ๐œ‘ โˆง ๐‘  โˆˆ ๐‘‡ ) โ†” ( ๐œ‘ โˆง ๐‘† โˆˆ ๐‘‡ ) ) )
8 fveq2 โŠข ( ๐‘  = ๐‘† โ†’ ( ๐‘ƒ โ€˜ ๐‘  ) = ( ๐‘ƒ โ€˜ ๐‘† ) )
9 fveq2 โŠข ( ๐‘  = ๐‘† โ†’ ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) = ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘† ) )
10 9 sumeq2sdv โŠข ( ๐‘  = ๐‘† โ†’ ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) = ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘† ) )
11 10 oveq2d โŠข ( ๐‘  = ๐‘† โ†’ ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) ) = ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘† ) ) )
12 8 11 eqeq12d โŠข ( ๐‘  = ๐‘† โ†’ ( ( ๐‘ƒ โ€˜ ๐‘  ) = ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) ) โ†” ( ๐‘ƒ โ€˜ ๐‘† ) = ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘† ) ) ) )
13 7 12 imbi12d โŠข ( ๐‘  = ๐‘† โ†’ ( ( ( ๐œ‘ โˆง ๐‘  โˆˆ ๐‘‡ ) โ†’ ( ๐‘ƒ โ€˜ ๐‘  ) = ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) ) ) โ†” ( ( ๐œ‘ โˆง ๐‘† โˆˆ ๐‘‡ ) โ†’ ( ๐‘ƒ โ€˜ ๐‘† ) = ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘† ) ) ) ) )
14 fveq2 โŠข ( ๐‘ก = ๐‘  โ†’ ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘ก ) = ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) )
15 14 sumeq2sdv โŠข ( ๐‘ก = ๐‘  โ†’ ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘ก ) = ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) )
16 15 oveq2d โŠข ( ๐‘ก = ๐‘  โ†’ ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘ก ) ) = ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) ) )
17 simpr โŠข ( ( ๐œ‘ โˆง ๐‘  โˆˆ ๐‘‡ ) โ†’ ๐‘  โˆˆ ๐‘‡ )
18 3 nnrecred โŠข ( ๐œ‘ โ†’ ( 1 / ๐‘€ ) โˆˆ โ„ )
19 18 adantr โŠข ( ( ๐œ‘ โˆง ๐‘  โˆˆ ๐‘‡ ) โ†’ ( 1 / ๐‘€ ) โˆˆ โ„ )
20 fzfid โŠข ( ( ๐œ‘ โˆง ๐‘  โˆˆ ๐‘‡ ) โ†’ ( 1 ... ๐‘€ ) โˆˆ Fin )
21 1 4 5 stoweidlem15 โŠข ( ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 1 ... ๐‘€ ) ) โˆง ๐‘  โˆˆ ๐‘‡ ) โ†’ ( ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) โˆˆ โ„ โˆง 0 โ‰ค ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) โˆง ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) โ‰ค 1 ) )
22 21 simp1d โŠข ( ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 1 ... ๐‘€ ) ) โˆง ๐‘  โˆˆ ๐‘‡ ) โ†’ ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) โˆˆ โ„ )
23 22 an32s โŠข ( ( ( ๐œ‘ โˆง ๐‘  โˆˆ ๐‘‡ ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘€ ) ) โ†’ ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) โˆˆ โ„ )
24 20 23 fsumrecl โŠข ( ( ๐œ‘ โˆง ๐‘  โˆˆ ๐‘‡ ) โ†’ ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) โˆˆ โ„ )
25 19 24 remulcld โŠข ( ( ๐œ‘ โˆง ๐‘  โˆˆ ๐‘‡ ) โ†’ ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) ) โˆˆ โ„ )
26 2 16 17 25 fvmptd3 โŠข ( ( ๐œ‘ โˆง ๐‘  โˆˆ ๐‘‡ ) โ†’ ( ๐‘ƒ โ€˜ ๐‘  ) = ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘  ) ) )
27 13 26 vtoclg โŠข ( ๐‘† โˆˆ ๐‘‡ โ†’ ( ( ๐œ‘ โˆง ๐‘† โˆˆ ๐‘‡ ) โ†’ ( ๐‘ƒ โ€˜ ๐‘† ) = ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘† ) ) ) )
28 27 anabsi7 โŠข ( ( ๐œ‘ โˆง ๐‘† โˆˆ ๐‘‡ ) โ†’ ( ๐‘ƒ โ€˜ ๐‘† ) = ( ( 1 / ๐‘€ ) ยท ฮฃ ๐‘– โˆˆ ( 1 ... ๐‘€ ) ( ( ๐บ โ€˜ ๐‘– ) โ€˜ ๐‘† ) ) )