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

Theorem addsdilem1 27846
Description: Lemma for surreal distribution. Expand the left hand side of the main expression. (Contributed by Scott Fenton, 8-Mar-2025.)
Hypotheses
Ref Expression
addsdilem.1 (๐œ‘ โ†’ ๐ด โˆˆ No )
addsdilem.2 (๐œ‘ โ†’ ๐ต โˆˆ No )
addsdilem.3 (๐œ‘ โ†’ ๐ถ โˆˆ No )
Assertion
Ref Expression
addsdilem1 (๐œ‘ โ†’ (๐ด ยทs (๐ต +s ๐ถ)) = ((({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))})) |s (({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))}))))
Distinct variable groups:   ๐ด,๐‘Ž,๐‘ฅ๐ฟ   ๐ด,๐‘ฅ๐‘…,๐‘ฆ๐ฟ   ๐ด,๐‘ฆ๐‘…   ๐ด,๐‘ง๐ฟ   ๐ด,๐‘ง๐‘…   ๐ต,๐‘Ž,๐‘ฅ๐ฟ   ๐ต,๐‘ฅ๐‘…,๐‘ฆ๐ฟ   ๐ต,๐‘ฆ๐‘…   ๐ต,๐‘ง๐ฟ   ๐ต,๐‘ง๐‘…   ๐ถ,๐‘Ž,๐‘ฅ๐ฟ   ๐ถ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ   ๐ถ,๐‘ฆ๐‘…   ๐ถ,๐‘ง๐ฟ   ๐ถ,๐‘ง๐‘…   ๐‘Ž,๐‘ฅ๐‘…,๐‘ฆ๐ฟ   ๐‘Ž,๐‘ฆ๐‘…   ๐‘Ž,๐‘ง๐ฟ   ๐‘Ž,๐‘ง๐‘…   ๐‘ฅ๐ฟ,๐‘ฆ๐ฟ   ๐‘ฅ๐ฟ,๐‘ฆ๐‘…   ๐‘ฅ๐ฟ,๐‘ง๐ฟ   ๐‘ฅ๐ฟ,๐‘ง๐‘…   ๐‘ฅ๐‘…,๐‘ฆ๐‘…   ๐‘ฅ๐‘…,๐‘ง๐ฟ   ๐‘ฅ๐‘…,๐‘ง๐‘…
Allowed substitution hints:   ๐œ‘(๐‘Ž,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ,๐‘ฆ๐‘…,๐‘ง๐ฟ,๐‘ง๐‘…)

Proof of Theorem addsdilem1
Dummy variables ๐‘ ๐‘ก are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lltropt 27605 . . . 4 ( L โ€˜๐ด) <<s ( R โ€˜๐ด)
21a1i 11 . . 3 (๐œ‘ โ†’ ( L โ€˜๐ด) <<s ( R โ€˜๐ด))
3 addsdilem.2 . . . 4 (๐œ‘ โ†’ ๐ต โˆˆ No )
4 addsdilem.3 . . . 4 (๐œ‘ โ†’ ๐ถ โˆˆ No )
53, 4addscut2 27702 . . 3 (๐œ‘ โ†’ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)}) <<s ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)}))
6 addsdilem.1 . . . . 5 (๐œ‘ โ†’ ๐ด โˆˆ No )
7 lrcut 27635 . . . . 5 (๐ด โˆˆ No โ†’ (( L โ€˜๐ด) |s ( R โ€˜๐ด)) = ๐ด)
86, 7syl 17 . . . 4 (๐œ‘ โ†’ (( L โ€˜๐ด) |s ( R โ€˜๐ด)) = ๐ด)
98eqcomd 2737 . . 3 (๐œ‘ โ†’ ๐ด = (( L โ€˜๐ด) |s ( R โ€˜๐ด)))
10 addsval2 27686 . . . 4 ((๐ต โˆˆ No โˆง ๐ถ โˆˆ No ) โ†’ (๐ต +s ๐ถ) = (({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)}) |s ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})))
113, 4, 10syl2anc 583 . . 3 (๐œ‘ โ†’ (๐ต +s ๐ถ) = (({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)}) |s ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})))
122, 5, 9, 11mulsunif 27845 . 2 (๐œ‘ โ†’ (๐ด ยทs (๐ต +s ๐ถ)) = (({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))}) |s ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))})))
13 unab 4298 . . . . 5 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))}) = {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ))))}
14 r19.43 3121 . . . . . . 7 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)(โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))) โ†” (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))))
15 rexun 4190 . . . . . . . . 9 (โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โˆจ โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
16 eqeq1 2735 . . . . . . . . . . . . 13 (๐‘ก = ๐‘ โ†’ (๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ) โ†” ๐‘ = (๐‘ฆ๐ฟ +s ๐ถ)))
1716rexbidv 3177 . . . . . . . . . . . 12 (๐‘ก = ๐‘ โ†’ (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (๐‘ฆ๐ฟ +s ๐ถ)))
1817rexab 3690 . . . . . . . . . . 11 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” โˆƒ๐‘(โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
19 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)โˆƒ๐‘(๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
20 ovex 7445 . . . . . . . . . . . . . 14 (๐‘ฆ๐ฟ +s ๐ถ) โˆˆ V
21 oveq2 7420 . . . . . . . . . . . . . . . . 17 (๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โ†’ (๐ด ยทs ๐‘) = (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ)))
2221oveq2d 7428 . . . . . . . . . . . . . . . 16 (๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โ†’ ((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) = ((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))))
23 oveq2 7420 . . . . . . . . . . . . . . . 16 (๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โ†’ (๐‘ฅ๐ฟ ยทs ๐‘) = (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ)))
2422, 23oveq12d 7430 . . . . . . . . . . . . . . 15 (๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โ†’ (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))))
2524eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โ†’ (๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ)))))
2620, 25ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘(๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))))
2726rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)โˆƒ๐‘(๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))))
28 r19.41v 3187 . . . . . . . . . . . . 13 (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
2928exbii 1849 . . . . . . . . . . . 12 (โˆƒ๐‘โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘(โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
3019, 27, 293bitr3ri 302 . . . . . . . . . . 11 (โˆƒ๐‘(โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))))
3118, 30bitri 275 . . . . . . . . . 10 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))))
32 eqeq1 2735 . . . . . . . . . . . . 13 (๐‘ก = ๐‘ โ†’ (๐‘ก = (๐ต +s ๐‘ง๐ฟ) โ†” ๐‘ = (๐ต +s ๐‘ง๐ฟ)))
3332rexbidv 3177 . . . . . . . . . . . 12 (๐‘ก = ๐‘ โ†’ (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ) โ†” โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐ฟ)))
3433rexab 3690 . . . . . . . . . . 11 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” โˆƒ๐‘(โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
35 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)โˆƒ๐‘(๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
36 ovex 7445 . . . . . . . . . . . . . 14 (๐ต +s ๐‘ง๐ฟ) โˆˆ V
37 oveq2 7420 . . . . . . . . . . . . . . . . 17 (๐‘ = (๐ต +s ๐‘ง๐ฟ) โ†’ (๐ด ยทs ๐‘) = (๐ด ยทs (๐ต +s ๐‘ง๐ฟ)))
3837oveq2d 7428 . . . . . . . . . . . . . . . 16 (๐‘ = (๐ต +s ๐‘ง๐ฟ) โ†’ ((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) = ((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))))
39 oveq2 7420 . . . . . . . . . . . . . . . 16 (๐‘ = (๐ต +s ๐‘ง๐ฟ) โ†’ (๐‘ฅ๐ฟ ยทs ๐‘) = (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))
4038, 39oveq12d 7430 . . . . . . . . . . . . . . 15 (๐‘ = (๐ต +s ๐‘ง๐ฟ) โ†’ (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ))))
4140eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ = (๐ต +s ๐‘ง๐ฟ) โ†’ (๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))))
4236, 41ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘(๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ))))
4342rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)โˆƒ๐‘(๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ))))
44 r19.41v 3187 . . . . . . . . . . . . 13 (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
4544exbii 1849 . . . . . . . . . . . 12 (โˆƒ๐‘โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘(โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
4635, 43, 453bitr3ri 302 . . . . . . . . . . 11 (โˆƒ๐‘(โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ))))
4734, 46bitri 275 . . . . . . . . . 10 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ))))
4831, 47orbi12i 912 . . . . . . . . 9 ((โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โˆจ โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))))
4915, 48bitr2i 276 . . . . . . . 8 ((โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))) โ†” โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)))
5049rexbii 3093 . . . . . . 7 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)(โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)))
5114, 50bitr3i 277 . . . . . 6 ((โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)))
5251abbii 2801 . . . . 5 {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ))))} = {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))}
5313, 52eqtri 2759 . . . 4 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))}) = {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))}
54 unab 4298 . . . . 5 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))}) = {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…))))}
55 r19.43 3121 . . . . . . 7 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)(โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))) โ†” (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))))
56 rexun 4190 . . . . . . . . 9 (โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โˆจ โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
57 eqeq1 2735 . . . . . . . . . . . . 13 (๐‘ก = ๐‘ โ†’ (๐‘ก = (๐‘ฆ๐‘… +s ๐ถ) โ†” ๐‘ = (๐‘ฆ๐‘… +s ๐ถ)))
5857rexbidv 3177 . . . . . . . . . . . 12 (๐‘ก = ๐‘ โ†’ (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (๐‘ฆ๐‘… +s ๐ถ)))
5958rexab 3690 . . . . . . . . . . 11 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” โˆƒ๐‘(โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
60 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)โˆƒ๐‘(๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
61 ovex 7445 . . . . . . . . . . . . . 14 (๐‘ฆ๐‘… +s ๐ถ) โˆˆ V
62 oveq2 7420 . . . . . . . . . . . . . . . . 17 (๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โ†’ (๐ด ยทs ๐‘) = (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ)))
6362oveq2d 7428 . . . . . . . . . . . . . . . 16 (๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โ†’ ((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) = ((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))))
64 oveq2 7420 . . . . . . . . . . . . . . . 16 (๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โ†’ (๐‘ฅ๐‘… ยทs ๐‘) = (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ)))
6563, 64oveq12d 7430 . . . . . . . . . . . . . . 15 (๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โ†’ (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))))
6665eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โ†’ (๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ)))))
6761, 66ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘(๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))))
6867rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)โˆƒ๐‘(๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))))
69 r19.41v 3187 . . . . . . . . . . . . 13 (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
7069exbii 1849 . . . . . . . . . . . 12 (โˆƒ๐‘โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘(โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
7160, 68, 703bitr3ri 302 . . . . . . . . . . 11 (โˆƒ๐‘(โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))))
7259, 71bitri 275 . . . . . . . . . 10 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))))
73 eqeq1 2735 . . . . . . . . . . . . 13 (๐‘ก = ๐‘ โ†’ (๐‘ก = (๐ต +s ๐‘ง๐‘…) โ†” ๐‘ = (๐ต +s ๐‘ง๐‘…)))
7473rexbidv 3177 . . . . . . . . . . . 12 (๐‘ก = ๐‘ โ†’ (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…) โ†” โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐‘…)))
7574rexab 3690 . . . . . . . . . . 11 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” โˆƒ๐‘(โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
76 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)โˆƒ๐‘(๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
77 ovex 7445 . . . . . . . . . . . . . 14 (๐ต +s ๐‘ง๐‘…) โˆˆ V
78 oveq2 7420 . . . . . . . . . . . . . . . . 17 (๐‘ = (๐ต +s ๐‘ง๐‘…) โ†’ (๐ด ยทs ๐‘) = (๐ด ยทs (๐ต +s ๐‘ง๐‘…)))
7978oveq2d 7428 . . . . . . . . . . . . . . . 16 (๐‘ = (๐ต +s ๐‘ง๐‘…) โ†’ ((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) = ((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))))
80 oveq2 7420 . . . . . . . . . . . . . . . 16 (๐‘ = (๐ต +s ๐‘ง๐‘…) โ†’ (๐‘ฅ๐‘… ยทs ๐‘) = (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))
8179, 80oveq12d 7430 . . . . . . . . . . . . . . 15 (๐‘ = (๐ต +s ๐‘ง๐‘…) โ†’ (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…))))
8281eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ = (๐ต +s ๐‘ง๐‘…) โ†’ (๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))))
8377, 82ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘(๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…))))
8483rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)โˆƒ๐‘(๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…))))
85 r19.41v 3187 . . . . . . . . . . . . 13 (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
8685exbii 1849 . . . . . . . . . . . 12 (โˆƒ๐‘โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘(โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
8776, 84, 863bitr3ri 302 . . . . . . . . . . 11 (โˆƒ๐‘(โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…))))
8875, 87bitri 275 . . . . . . . . . 10 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…))))
8972, 88orbi12i 912 . . . . . . . . 9 ((โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โˆจ โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))))
9056, 89bitr2i 276 . . . . . . . 8 ((โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))) โ†” โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)))
9190rexbii 3093 . . . . . . 7 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)(โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)))
9255, 91bitr3i 277 . . . . . 6 ((โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)))
9392abbii 2801 . . . . 5 {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…))))} = {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))}
9454, 93eqtri 2759 . . . 4 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))}) = {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))}
9553, 94uneq12i 4161 . . 3 (({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))})) = ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))})
96 unab 4298 . . . . 5 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))}) = {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…))))}
97 r19.43 3121 . . . . . . 7 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)(โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))) โ†” (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))))
98 rexun 4190 . . . . . . . . 9 (โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โˆจ โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
9958rexab 3690 . . . . . . . . . . 11 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” โˆƒ๐‘(โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
100 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)โˆƒ๐‘(๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
10162oveq2d 7428 . . . . . . . . . . . . . . . 16 (๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โ†’ ((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) = ((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))))
102 oveq2 7420 . . . . . . . . . . . . . . . 16 (๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โ†’ (๐‘ฅ๐ฟ ยทs ๐‘) = (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ)))
103101, 102oveq12d 7430 . . . . . . . . . . . . . . 15 (๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โ†’ (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))))
104103eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โ†’ (๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ)))))
10561, 104ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘(๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))))
106105rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)โˆƒ๐‘(๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))))
107 r19.41v 3187 . . . . . . . . . . . . 13 (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
108107exbii 1849 . . . . . . . . . . . 12 (โˆƒ๐‘โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘(โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
109100, 106, 1083bitr3ri 302 . . . . . . . . . . 11 (โˆƒ๐‘(โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (๐‘ฆ๐‘… +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))))
11099, 109bitri 275 . . . . . . . . . 10 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))))
11174rexab 3690 . . . . . . . . . . 11 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” โˆƒ๐‘(โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
112 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)โˆƒ๐‘(๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
11378oveq2d 7428 . . . . . . . . . . . . . . . 16 (๐‘ = (๐ต +s ๐‘ง๐‘…) โ†’ ((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) = ((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))))
114 oveq2 7420 . . . . . . . . . . . . . . . 16 (๐‘ = (๐ต +s ๐‘ง๐‘…) โ†’ (๐‘ฅ๐ฟ ยทs ๐‘) = (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))
115113, 114oveq12d 7430 . . . . . . . . . . . . . . 15 (๐‘ = (๐ต +s ๐‘ง๐‘…) โ†’ (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…))))
116115eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ = (๐ต +s ๐‘ง๐‘…) โ†’ (๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))))
11777, 116ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘(๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…))))
118117rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)โˆƒ๐‘(๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…))))
119 r19.41v 3187 . . . . . . . . . . . . 13 (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
120119exbii 1849 . . . . . . . . . . . 12 (โˆƒ๐‘โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘(โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))))
121112, 118, 1203bitr3ri 302 . . . . . . . . . . 11 (โˆƒ๐‘(โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐‘…) โˆง ๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…))))
122111, 121bitri 275 . . . . . . . . . 10 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โ†” โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…))))
123110, 122orbi12i 912 . . . . . . . . 9 ((โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)) โˆจ โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)}๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))) โ†” (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))))
12498, 123bitr2i 276 . . . . . . . 8 ((โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))) โ†” โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)))
125124rexbii 3093 . . . . . . 7 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)(โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)))
12697, 125bitr3i 277 . . . . . 6 ((โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘)))
127126abbii 2801 . . . . 5 {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…))))} = {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))}
12896, 127eqtri 2759 . . . 4 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))}) = {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))}
129 unab 4298 . . . . 5 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))}) = {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ))))}
130 r19.43 3121 . . . . . . 7 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)(โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))) โ†” (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))))
131 rexun 4190 . . . . . . . . 9 (โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โˆจ โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
13217rexab 3690 . . . . . . . . . . 11 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” โˆƒ๐‘(โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
133 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)โˆƒ๐‘(๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
13421oveq2d 7428 . . . . . . . . . . . . . . . 16 (๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โ†’ ((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) = ((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))))
135 oveq2 7420 . . . . . . . . . . . . . . . 16 (๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โ†’ (๐‘ฅ๐‘… ยทs ๐‘) = (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ)))
136134, 135oveq12d 7430 . . . . . . . . . . . . . . 15 (๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โ†’ (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))))
137136eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โ†’ (๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ)))))
13820, 137ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘(๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))))
139138rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)โˆƒ๐‘(๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))))
140 r19.41v 3187 . . . . . . . . . . . . 13 (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
141140exbii 1849 . . . . . . . . . . . 12 (โˆƒ๐‘โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘(โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
142133, 139, 1413bitr3ri 302 . . . . . . . . . . 11 (โˆƒ๐‘(โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (๐‘ฆ๐ฟ +s ๐ถ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))))
143132, 142bitri 275 . . . . . . . . . 10 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))))
14433rexab 3690 . . . . . . . . . . 11 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” โˆƒ๐‘(โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
145 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)โˆƒ๐‘(๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
14637oveq2d 7428 . . . . . . . . . . . . . . . 16 (๐‘ = (๐ต +s ๐‘ง๐ฟ) โ†’ ((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) = ((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))))
147 oveq2 7420 . . . . . . . . . . . . . . . 16 (๐‘ = (๐ต +s ๐‘ง๐ฟ) โ†’ (๐‘ฅ๐‘… ยทs ๐‘) = (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))
148146, 147oveq12d 7430 . . . . . . . . . . . . . . 15 (๐‘ = (๐ต +s ๐‘ง๐ฟ) โ†’ (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ))))
149148eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ = (๐ต +s ๐‘ง๐ฟ) โ†’ (๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))))
15036, 149ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘(๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ))))
151150rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)โˆƒ๐‘(๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ))))
152 r19.41v 3187 . . . . . . . . . . . . 13 (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
153152exbii 1849 . . . . . . . . . . . 12 (โˆƒ๐‘โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘(โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))))
154145, 151, 1533bitr3ri 302 . . . . . . . . . . 11 (โˆƒ๐‘(โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (๐ต +s ๐‘ง๐ฟ) โˆง ๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ))))
155144, 154bitri 275 . . . . . . . . . 10 (โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โ†” โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ))))
156143, 155orbi12i 912 . . . . . . . . 9 ((โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)) โˆจ โˆƒ๐‘ โˆˆ {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)}๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))) โ†” (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))))
157131, 156bitr2i 276 . . . . . . . 8 ((โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))) โ†” โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)))
158157rexbii 3093 . . . . . . 7 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)(โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)))
159130, 158bitr3i 277 . . . . . 6 ((โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘)))
160159abbii 2801 . . . . 5 {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ))))} = {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))}
161129, 160eqtri 2759 . . . 4 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))}) = {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))}
162128, 161uneq12i 4161 . . 3 (({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))})) = ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))})
16395, 162oveq12i 7424 . 2 ((({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))})) |s (({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))}))) = (({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))}) |s ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (๐‘ฆ๐‘… +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐‘…)})๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐ฟ ยทs ๐‘))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ โˆˆ ({๐‘ก โˆฃ โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (๐‘ฆ๐ฟ +s ๐ถ)} โˆช {๐‘ก โˆฃ โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (๐ต +s ๐‘ง๐ฟ)})๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs ๐‘)) -s (๐‘ฅ๐‘… ยทs ๐‘))}))
16412, 163eqtr4di 2789 1 (๐œ‘ โ†’ (๐ด ยทs (๐ต +s ๐ถ)) = ((({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐ฟ +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐ฟ)))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐‘… +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐‘…)))})) |s (({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐‘… +s ๐ถ))) -s (๐‘ฅ๐ฟ ยทs (๐‘ฆ๐‘… +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐‘…))) -s (๐‘ฅ๐ฟ ยทs (๐ต +s ๐‘ง๐‘…)))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐‘ฆ๐ฟ +s ๐ถ))) -s (๐‘ฅ๐‘… ยทs (๐‘ฆ๐ฟ +s ๐ถ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = (((๐‘ฅ๐‘… ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐‘ง๐ฟ))) -s (๐‘ฅ๐‘… ยทs (๐ต +s ๐‘ง๐ฟ)))}))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   โˆจ wo 844   = wceq 1540  โˆƒwex 1780   โˆˆ wcel 2105  {cab 2708  โˆƒwrex 3069   โˆช cun 3946   class class class wbr 5148  โ€˜cfv 6543  (class class class)co 7412   No csur 27380   <<s csslt 27519   |s cscut 27521   L cleft 27578   R cright 27579   +s cadds 27682   -s csubs 27735   ยทs cmuls 27802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-ot 4637  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7979  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-1o 8470  df-2o 8471  df-nadd 8669  df-no 27383  df-slt 27384  df-bday 27385  df-sle 27485  df-sslt 27520  df-scut 27522  df-0s 27563  df-made 27580  df-old 27581  df-left 27583  df-right 27584  df-norec 27661  df-norec2 27672  df-adds 27683  df-negs 27736  df-subs 27737  df-muls 27803
This theorem is referenced by:  addsdi  27850
  Copyright terms: Public domain W3C validator