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

Theorem axcontlem1 28260
Description: Lemma for axcont 28272. Change bound variables for later use. (Contributed by Scott Fenton, 20-Jun-2013.)
Hypothesis
Ref Expression
axcontlem1.1 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
Assertion
Ref Expression
axcontlem1 ๐น = {โŸจ๐‘ฆ, ๐‘ โŸฉ โˆฃ (๐‘ฆ โˆˆ ๐ท โˆง (๐‘  โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘— โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘—) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘—)) + (๐‘  ยท (๐‘ˆโ€˜๐‘—)))))}
Distinct variable groups:   ๐ท,๐‘ ,๐‘ก,๐‘ฅ,๐‘ฆ   ๐‘–,๐‘—,๐‘ ,๐‘ก,๐‘ฅ,๐‘ฆ,๐‘   ๐‘ˆ,๐‘–,๐‘—,๐‘ ,๐‘ก,๐‘ฅ,๐‘ฆ   ๐‘–,๐‘,๐‘—,๐‘ ,๐‘ก,๐‘ฅ,๐‘ฆ
Allowed substitution hints:   ๐ท(๐‘–,๐‘—)   ๐น(๐‘ฅ,๐‘ฆ,๐‘ก,๐‘–,๐‘—,๐‘ )

Proof of Theorem axcontlem1
StepHypRef Expression
1 axcontlem1.1 . 2 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
2 eleq1w 2816 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘ฅ โˆˆ ๐ท โ†” ๐‘ฆ โˆˆ ๐ท))
32adantr 481 . . . 4 ((๐‘ฅ = ๐‘ฆ โˆง ๐‘ก = ๐‘ ) โ†’ (๐‘ฅ โˆˆ ๐ท โ†” ๐‘ฆ โˆˆ ๐ท))
4 eleq1w 2816 . . . . . 6 (๐‘ก = ๐‘  โ†’ (๐‘ก โˆˆ (0[,)+โˆž) โ†” ๐‘  โˆˆ (0[,)+โˆž)))
54adantl 482 . . . . 5 ((๐‘ฅ = ๐‘ฆ โˆง ๐‘ก = ๐‘ ) โ†’ (๐‘ก โˆˆ (0[,)+โˆž) โ†” ๐‘  โˆˆ (0[,)+โˆž)))
6 fveq1 6890 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘ฅโ€˜๐‘–) = (๐‘ฆโ€˜๐‘–))
7 oveq2 7419 . . . . . . . . . 10 (๐‘ก = ๐‘  โ†’ (1 โˆ’ ๐‘ก) = (1 โˆ’ ๐‘ ))
87oveq1d 7426 . . . . . . . . 9 (๐‘ก = ๐‘  โ†’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) = ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)))
9 oveq1 7418 . . . . . . . . 9 (๐‘ก = ๐‘  โ†’ (๐‘ก ยท (๐‘ˆโ€˜๐‘–)) = (๐‘  ยท (๐‘ˆโ€˜๐‘–)))
108, 9oveq12d 7429 . . . . . . . 8 (๐‘ก = ๐‘  โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))))
116, 10eqeqan12d 2746 . . . . . . 7 ((๐‘ฅ = ๐‘ฆ โˆง ๐‘ก = ๐‘ ) โ†’ ((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” (๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))))
1211ralbidv 3177 . . . . . 6 ((๐‘ฅ = ๐‘ฆ โˆง ๐‘ก = ๐‘ ) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))))
13 fveq2 6891 . . . . . . . 8 (๐‘– = ๐‘— โ†’ (๐‘ฆโ€˜๐‘–) = (๐‘ฆโ€˜๐‘—))
14 fveq2 6891 . . . . . . . . . 10 (๐‘– = ๐‘— โ†’ (๐‘โ€˜๐‘–) = (๐‘โ€˜๐‘—))
1514oveq2d 7427 . . . . . . . . 9 (๐‘– = ๐‘— โ†’ ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) = ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘—)))
16 fveq2 6891 . . . . . . . . . 10 (๐‘– = ๐‘— โ†’ (๐‘ˆโ€˜๐‘–) = (๐‘ˆโ€˜๐‘—))
1716oveq2d 7427 . . . . . . . . 9 (๐‘– = ๐‘— โ†’ (๐‘  ยท (๐‘ˆโ€˜๐‘–)) = (๐‘  ยท (๐‘ˆโ€˜๐‘—)))
1815, 17oveq12d 7429 . . . . . . . 8 (๐‘– = ๐‘— โ†’ (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘—)) + (๐‘  ยท (๐‘ˆโ€˜๐‘—))))
1913, 18eqeq12d 2748 . . . . . . 7 (๐‘– = ๐‘— โ†’ ((๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))) โ†” (๐‘ฆโ€˜๐‘—) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘—)) + (๐‘  ยท (๐‘ˆโ€˜๐‘—)))))
2019cbvralvw 3234 . . . . . 6 (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆ€๐‘— โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘—) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘—)) + (๐‘  ยท (๐‘ˆโ€˜๐‘—))))
2112, 20bitrdi 286 . . . . 5 ((๐‘ฅ = ๐‘ฆ โˆง ๐‘ก = ๐‘ ) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆ€๐‘— โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘—) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘—)) + (๐‘  ยท (๐‘ˆโ€˜๐‘—)))))
225, 21anbi12d 631 . . . 4 ((๐‘ฅ = ๐‘ฆ โˆง ๐‘ก = ๐‘ ) โ†’ ((๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†” (๐‘  โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘— โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘—) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘—)) + (๐‘  ยท (๐‘ˆโ€˜๐‘—))))))
233, 22anbi12d 631 . . 3 ((๐‘ฅ = ๐‘ฆ โˆง ๐‘ก = ๐‘ ) โ†’ ((๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))) โ†” (๐‘ฆ โˆˆ ๐ท โˆง (๐‘  โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘— โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘—) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘—)) + (๐‘  ยท (๐‘ˆโ€˜๐‘—)))))))
2423cbvopabv 5221 . 2 {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))} = {โŸจ๐‘ฆ, ๐‘ โŸฉ โˆฃ (๐‘ฆ โˆˆ ๐ท โˆง (๐‘  โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘— โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘—) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘—)) + (๐‘  ยท (๐‘ˆโ€˜๐‘—)))))}
251, 24eqtri 2760 1 ๐น = {โŸจ๐‘ฆ, ๐‘ โŸฉ โˆฃ (๐‘ฆ โˆˆ ๐ท โˆง (๐‘  โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘— โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘—) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘—)) + (๐‘  ยท (๐‘ˆโ€˜๐‘—)))))}
Colors of variables: wff setvar class
Syntax hints:   โ†” wb 205   โˆง wa 396   = wceq 1541   โˆˆ wcel 2106  โˆ€wral 3061  {copab 5210  โ€˜cfv 6543  (class class class)co 7411  0cc0 11112  1c1 11113   + caddc 11115   ยท cmul 11117  +โˆžcpnf 11247   โˆ’ cmin 11446  [,)cico 13328  ...cfz 13486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-iota 6495  df-fv 6551  df-ov 7414
This theorem is referenced by:  axcontlem6  28265  axcontlem11  28270
  Copyright terms: Public domain W3C validator