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

Theorem precsexlem3 28081
Description: Lemma for surreal reciprocals. Calculate the value of the recursive function at a successor. (Contributed by Scott Fenton, 12-Mar-2025.)
Hypotheses
Ref Expression
precsexlem.1 ๐น = rec((๐‘ โˆˆ V โ†ฆ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ), โŸจ{ 0s }, โˆ…โŸฉ)
precsexlem.2 ๐ฟ = (1st โˆ˜ ๐น)
precsexlem.3 ๐‘… = (2nd โˆ˜ ๐น)
Assertion
Ref Expression
precsexlem3 (๐ผ โˆˆ ฯ‰ โ†’ (๐นโ€˜suc ๐ผ) = โŸจ((๐ฟโ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ)
Distinct variable groups:   ๐ด,๐‘Ž,๐‘™,๐‘,๐‘Ÿ,๐‘ฅ,๐‘ฅ๐ฟ,๐‘ฅ๐‘…   ๐น,๐‘™,๐‘   ๐ผ,๐‘Ž,๐‘™,๐‘,๐‘Ÿ,๐‘ฅ,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ,๐‘ฆ๐‘…   ๐ฟ,๐‘Ž,๐‘™,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ   ๐‘…,๐‘Ž,๐‘™,๐‘Ÿ,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐‘…
Allowed substitution hints:   ๐ด(๐‘ฆ๐ฟ,๐‘ฆ๐‘…)   ๐‘…(๐‘ฅ,๐‘,๐‘ฆ๐ฟ)   ๐น(๐‘ฅ,๐‘Ÿ,๐‘Ž,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ,๐‘ฆ๐‘…)   ๐ฟ(๐‘ฅ,๐‘Ÿ,๐‘,๐‘ฆ๐‘…)

Proof of Theorem precsexlem3
StepHypRef Expression
1 nnon 7868 . . 3 (๐ผ โˆˆ ฯ‰ โ†’ ๐ผ โˆˆ On)
2 opex 5460 . . . . 5 โŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ โˆˆ V
32csbex 5305 . . . 4 โฆ‹(2nd โ€˜(๐นโ€˜๐ผ)) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ โˆˆ V
43csbex 5305 . . 3 โฆ‹(1st โ€˜(๐นโ€˜๐ผ)) / ๐‘™โฆŒโฆ‹(2nd โ€˜(๐นโ€˜๐ผ)) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ โˆˆ V
5 precsexlem.1 . . . 4 ๐น = rec((๐‘ โˆˆ V โ†ฆ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ), โŸจ{ 0s }, โˆ…โŸฉ)
6 fveq2 6891 . . . . 5 (๐‘ = (๐นโ€˜๐ผ) โ†’ (1st โ€˜๐‘) = (1st โ€˜(๐นโ€˜๐ผ)))
7 fveq2 6891 . . . . . 6 (๐‘ = (๐นโ€˜๐ผ) โ†’ (2nd โ€˜๐‘) = (2nd โ€˜(๐นโ€˜๐ผ)))
87csbeq1d 3893 . . . . 5 (๐‘ = (๐นโ€˜๐ผ) โ†’ โฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ = โฆ‹(2nd โ€˜(๐นโ€˜๐ผ)) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ)
96, 8csbeq12dv 3898 . . . 4 (๐‘ = (๐นโ€˜๐ผ) โ†’ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ = โฆ‹(1st โ€˜(๐นโ€˜๐ผ)) / ๐‘™โฆŒโฆ‹(2nd โ€˜(๐นโ€˜๐ผ)) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ)
105, 9rdgsucmpt 8443 . . 3 ((๐ผ โˆˆ On โˆง โฆ‹(1st โ€˜(๐นโ€˜๐ผ)) / ๐‘™โฆŒโฆ‹(2nd โ€˜(๐นโ€˜๐ผ)) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ โˆˆ V) โ†’ (๐นโ€˜suc ๐ผ) = โฆ‹(1st โ€˜(๐นโ€˜๐ผ)) / ๐‘™โฆŒโฆ‹(2nd โ€˜(๐นโ€˜๐ผ)) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ)
111, 4, 10sylancl 585 . 2 (๐ผ โˆˆ ฯ‰ โ†’ (๐นโ€˜suc ๐ผ) = โฆ‹(1st โ€˜(๐นโ€˜๐ผ)) / ๐‘™โฆŒโฆ‹(2nd โ€˜(๐นโ€˜๐ผ)) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ)
12 precsexlem.2 . . . . . 6 ๐ฟ = (1st โˆ˜ ๐น)
1312fveq1i 6892 . . . . 5 (๐ฟโ€˜๐ผ) = ((1st โˆ˜ ๐น)โ€˜๐ผ)
14 rdgfnon 8430 . . . . . . 7 rec((๐‘ โˆˆ V โ†ฆ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ), โŸจ{ 0s }, โˆ…โŸฉ) Fn On
155fneq1i 6645 . . . . . . 7 (๐น Fn On โ†” rec((๐‘ โˆˆ V โ†ฆ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ), โŸจ{ 0s }, โˆ…โŸฉ) Fn On)
1614, 15mpbir 230 . . . . . 6 ๐น Fn On
17 fvco2 6989 . . . . . 6 ((๐น Fn On โˆง ๐ผ โˆˆ On) โ†’ ((1st โˆ˜ ๐น)โ€˜๐ผ) = (1st โ€˜(๐นโ€˜๐ผ)))
1816, 1, 17sylancr 586 . . . . 5 (๐ผ โˆˆ ฯ‰ โ†’ ((1st โˆ˜ ๐น)โ€˜๐ผ) = (1st โ€˜(๐นโ€˜๐ผ)))
1913, 18eqtrid 2779 . . . 4 (๐ผ โˆˆ ฯ‰ โ†’ (๐ฟโ€˜๐ผ) = (1st โ€˜(๐นโ€˜๐ผ)))
20 precsexlem.3 . . . . . . 7 ๐‘… = (2nd โˆ˜ ๐น)
2120fveq1i 6892 . . . . . 6 (๐‘…โ€˜๐ผ) = ((2nd โˆ˜ ๐น)โ€˜๐ผ)
22 fvco2 6989 . . . . . . 7 ((๐น Fn On โˆง ๐ผ โˆˆ On) โ†’ ((2nd โˆ˜ ๐น)โ€˜๐ผ) = (2nd โ€˜(๐นโ€˜๐ผ)))
2316, 1, 22sylancr 586 . . . . . 6 (๐ผ โˆˆ ฯ‰ โ†’ ((2nd โˆ˜ ๐น)โ€˜๐ผ) = (2nd โ€˜(๐นโ€˜๐ผ)))
2421, 23eqtrid 2779 . . . . 5 (๐ผ โˆˆ ฯ‰ โ†’ (๐‘…โ€˜๐ผ) = (2nd โ€˜(๐นโ€˜๐ผ)))
2524csbeq1d 3893 . . . 4 (๐ผ โˆˆ ฯ‰ โ†’ โฆ‹(๐‘…โ€˜๐ผ) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ = โฆ‹(2nd โ€˜(๐นโ€˜๐ผ)) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ)
2619, 25csbeq12dv 3898 . . 3 (๐ผ โˆˆ ฯ‰ โ†’ โฆ‹(๐ฟโ€˜๐ผ) / ๐‘™โฆŒโฆ‹(๐‘…โ€˜๐ผ) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ = โฆ‹(1st โ€˜(๐นโ€˜๐ผ)) / ๐‘™โฆŒโฆ‹(2nd โ€˜(๐นโ€˜๐ผ)) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ)
27 fvex 6904 . . . . . 6 (๐‘…โ€˜๐ผ) โˆˆ V
28 rexeq 3316 . . . . . . . . . . 11 (๐‘Ÿ = (๐‘…โ€˜๐ผ) โ†’ (โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)))
2928rexbidv 3173 . . . . . . . . . 10 (๐‘Ÿ = (๐‘…โ€˜๐ผ) โ†’ (โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)))
3029abbidv 2796 . . . . . . . . 9 (๐‘Ÿ = (๐‘…โ€˜๐ผ) โ†’ {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)} = {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})
3130uneq2d 4159 . . . . . . . 8 (๐‘Ÿ = (๐‘…โ€˜๐ผ) โ†’ ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)}) = ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)}))
3231uneq2d 4159 . . . . . . 7 (๐‘Ÿ = (๐‘…โ€˜๐ผ) โ†’ (๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})) = (๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})))
33 id 22 . . . . . . . 8 (๐‘Ÿ = (๐‘…โ€˜๐ผ) โ†’ ๐‘Ÿ = (๐‘…โ€˜๐ผ))
34 rexeq 3316 . . . . . . . . . . 11 (๐‘Ÿ = (๐‘…โ€˜๐ผ) โ†’ (โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)))
3534rexbidv 3173 . . . . . . . . . 10 (๐‘Ÿ = (๐‘…โ€˜๐ผ) โ†’ (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)))
3635abbidv 2796 . . . . . . . . 9 (๐‘Ÿ = (๐‘…โ€˜๐ผ) โ†’ {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)} = {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)})
3736uneq2d 4159 . . . . . . . 8 (๐‘Ÿ = (๐‘…โ€˜๐ผ) โ†’ ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}) = ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))
3833, 37uneq12d 4160 . . . . . . 7 (๐‘Ÿ = (๐‘…โ€˜๐ผ) โ†’ (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)})) = ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)})))
3932, 38opeq12d 4877 . . . . . 6 (๐‘Ÿ = (๐‘…โ€˜๐ผ) โ†’ โŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ = โŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ)
4027, 39csbie 3925 . . . . 5 โฆ‹(๐‘…โ€˜๐ผ) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ = โŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ
4140csbeq2i 3897 . . . 4 โฆ‹(๐ฟโ€˜๐ผ) / ๐‘™โฆŒโฆ‹(๐‘…โ€˜๐ผ) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ = โฆ‹(๐ฟโ€˜๐ผ) / ๐‘™โฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ
42 fvex 6904 . . . . 5 (๐ฟโ€˜๐ผ) โˆˆ V
43 id 22 . . . . . . 7 (๐‘™ = (๐ฟโ€˜๐ผ) โ†’ ๐‘™ = (๐ฟโ€˜๐ผ))
44 rexeq 3316 . . . . . . . . . 10 (๐‘™ = (๐ฟโ€˜๐ผ) โ†’ (โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)))
4544rexbidv 3173 . . . . . . . . 9 (๐‘™ = (๐ฟโ€˜๐ผ) โ†’ (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)))
4645abbidv 2796 . . . . . . . 8 (๐‘™ = (๐ฟโ€˜๐ผ) โ†’ {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} = {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)})
4746uneq1d 4158 . . . . . . 7 (๐‘™ = (๐ฟโ€˜๐ผ) โ†’ ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)}) = ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)}))
4843, 47uneq12d 4160 . . . . . 6 (๐‘™ = (๐ฟโ€˜๐ผ) โ†’ (๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})) = ((๐ฟโ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})))
49 rexeq 3316 . . . . . . . . . 10 (๐‘™ = (๐ฟโ€˜๐ผ) โ†’ (โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)))
5049rexbidv 3173 . . . . . . . . 9 (๐‘™ = (๐ฟโ€˜๐ผ) โ†’ (โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)))
5150abbidv 2796 . . . . . . . 8 (๐‘™ = (๐ฟโ€˜๐ผ) โ†’ {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} = {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)})
5251uneq1d 4158 . . . . . . 7 (๐‘™ = (๐ฟโ€˜๐ผ) โ†’ ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}) = ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))
5352uneq2d 4159 . . . . . 6 (๐‘™ = (๐ฟโ€˜๐ผ) โ†’ ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)})) = ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)})))
5448, 53opeq12d 4877 . . . . 5 (๐‘™ = (๐ฟโ€˜๐ผ) โ†’ โŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ = โŸจ((๐ฟโ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ)
5542, 54csbie 3925 . . . 4 โฆ‹(๐ฟโ€˜๐ผ) / ๐‘™โฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ = โŸจ((๐ฟโ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ
5641, 55eqtri 2755 . . 3 โฆ‹(๐ฟโ€˜๐ผ) / ๐‘™โฆŒโฆ‹(๐‘…โ€˜๐ผ) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ = โŸจ((๐ฟโ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ
5726, 56eqtr3di 2782 . 2 (๐ผ โˆˆ ฯ‰ โ†’ โฆ‹(1st โ€˜(๐นโ€˜๐ผ)) / ๐‘™โฆŒโฆ‹(2nd โ€˜(๐นโ€˜๐ผ)) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ = โŸจ((๐ฟโ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ)
5811, 57eqtrd 2767 1 (๐ผ โˆˆ ฯ‰ โ†’ (๐นโ€˜suc ๐ผ) = โŸจ((๐ฟโ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   = wceq 1534   โˆˆ wcel 2099  {cab 2704  โˆƒwrex 3065  {crab 3427  Vcvv 3469  โฆ‹csb 3889   โˆช cun 3942  โˆ…c0 4318  {csn 4624  โŸจcop 4630   class class class wbr 5142   โ†ฆ cmpt 5225   โˆ˜ ccom 5676  Oncon0 6363  suc csuc 6365   Fn wfn 6537  โ€˜cfv 6542  (class class class)co 7414  ฯ‰com 7862  1st c1st 7983  2nd c2nd 7984  reccrdg 8421   <s cslt 27548   0s c0s 27729   1s c1s 27730   L cleft 27746   R cright 27747   +s cadds 27850   -s csubs 27907   ยทs cmuls 27980   /su cdivs 28061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7732
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-om 7863  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422
This theorem is referenced by:  precsexlem4  28082  precsexlem5  28083
  Copyright terms: Public domain W3C validator