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

Theorem addsdilem2 27847
Description: Lemma for surreal distribution. Expand the right 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
addsdilem2 (๐œ‘ โ†’ ((๐ด ยทs ๐ต) +s (๐ด ยทs ๐ถ)) = ((({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)))})) |s (({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)))}))))
Distinct variable groups:   ๐ด,๐‘Ž,๐‘ฅ๐ฟ   ๐ด,๐‘ฅ๐‘…,๐‘ฆ๐ฟ   ๐ด,๐‘ฆ๐‘…   ๐ด,๐‘ง๐ฟ   ๐ด,๐‘ง๐‘…   ๐ต,๐‘Ž,๐‘ฅ๐ฟ   ๐ต,๐‘ฅ๐‘…,๐‘ฆ๐ฟ   ๐ต,๐‘ฆ๐‘…   ๐ต,๐‘ง๐ฟ   ๐ต,๐‘ง๐‘…   ๐ถ,๐‘Ž,๐‘ฅ๐ฟ   ๐ถ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ   ๐ถ,๐‘ฆ๐‘…   ๐ถ,๐‘ง๐ฟ   ๐ถ,๐‘ง๐‘…   ๐‘Ž,๐‘ฅ๐‘…,๐‘ฆ๐ฟ   ๐‘Ž,๐‘ฆ๐‘…   ๐‘Ž,๐‘ง๐ฟ   ๐‘Ž,๐‘ง๐‘…   ๐‘ฅ๐ฟ,๐‘ฆ๐ฟ   ๐‘ฅ๐ฟ,๐‘ฆ๐‘…   ๐‘ฅ๐ฟ,๐‘ง๐ฟ   ๐‘ฅ๐ฟ,๐‘ง๐‘…   ๐‘ฅ๐‘…,๐‘ฆ๐‘…   ๐‘ฅ๐‘…,๐‘ง๐ฟ   ๐‘ฅ๐‘…,๐‘ง๐‘…
Allowed substitution hints:   ๐œ‘(๐‘Ž,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ,๐‘ฆ๐‘…,๐‘ง๐ฟ,๐‘ง๐‘…)

Proof of Theorem addsdilem2
Dummy variables ๐‘ ๐‘ก are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 addsdilem.1 . . . 4 (๐œ‘ โ†’ ๐ด โˆˆ No )
2 addsdilem.2 . . . 4 (๐œ‘ โ†’ ๐ต โˆˆ No )
31, 2mulscut2 27829 . . 3 (๐œ‘ โ†’ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))}) <<s ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))}))
4 addsdilem.3 . . . 4 (๐œ‘ โ†’ ๐ถ โˆˆ No )
51, 4mulscut2 27829 . . 3 (๐œ‘ โ†’ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))}) <<s ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))}))
6 mulsval2 27807 . . . 4 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (๐ด ยทs ๐ต) = (({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))}) |s ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))})))
71, 2, 6syl2anc 583 . . 3 (๐œ‘ โ†’ (๐ด ยทs ๐ต) = (({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))}) |s ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))})))
8 mulsval2 27807 . . . 4 ((๐ด โˆˆ No โˆง ๐ถ โˆˆ No ) โ†’ (๐ด ยทs ๐ถ) = (({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))}) |s ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))})))
91, 4, 8syl2anc 583 . . 3 (๐œ‘ โ†’ (๐ด ยทs ๐ถ) = (({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))}) |s ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))})))
103, 5, 7, 9addsunif 27725 . 2 (๐œ‘ โ†’ ((๐ด ยทs ๐ต) +s (๐ด ยทs ๐ถ)) = (({๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)}) |s ({๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)})))
11 unab 4298 . . . . 5 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))}) = {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))}
12 rexun 4190 . . . . . . 7 (โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โˆจ โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
13 eqeq1 2735 . . . . . . . . . . 11 (๐‘ = ๐‘ก โ†’ (๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โ†” ๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))))
14132rexbidv 3218 . . . . . . . . . 10 (๐‘ = ๐‘ก โ†’ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))))
1514rexab 3690 . . . . . . . . 9 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
16 rexcom4 3284 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘กโˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
17 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘กโˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
18 ovex 7445 . . . . . . . . . . . . . 14 (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆˆ V
19 oveq1 7419 . . . . . . . . . . . . . . 15 (๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โ†’ (๐‘ก +s (๐ด ยทs ๐ถ)) = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
2019eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โ†’ (๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” ๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))))
2118, 20ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” ๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
2221rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
2317, 22bitr3i 277 . . . . . . . . . . 11 (โˆƒ๐‘กโˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
2423rexbii 3093 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
25 r19.41vv 3223 . . . . . . . . . . 11 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
2625exbii 1849 . . . . . . . . . 10 (โˆƒ๐‘กโˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
2716, 24, 263bitr3ri 302 . . . . . . . . 9 (โˆƒ๐‘ก(โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
2815, 27bitri 275 . . . . . . . 8 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
29 eqeq1 2735 . . . . . . . . . . 11 (๐‘ = ๐‘ก โ†’ (๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โ†” ๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))))
30292rexbidv 3218 . . . . . . . . . 10 (๐‘ = ๐‘ก โ†’ (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))))
3130rexab 3690 . . . . . . . . 9 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
32 rexcom4 3284 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘กโˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
33 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘กโˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
34 ovex 7445 . . . . . . . . . . . . . 14 (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆˆ V
35 oveq1 7419 . . . . . . . . . . . . . . 15 (๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โ†’ (๐‘ก +s (๐ด ยทs ๐ถ)) = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
3635eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โ†’ (๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” ๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))))
3734, 36ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” ๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
3837rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
3933, 38bitr3i 277 . . . . . . . . . . 11 (โˆƒ๐‘กโˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
4039rexbii 3093 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
41 r19.41vv 3223 . . . . . . . . . . 11 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
4241exbii 1849 . . . . . . . . . 10 (โˆƒ๐‘กโˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
4332, 40, 423bitr3ri 302 . . . . . . . . 9 (โˆƒ๐‘ก(โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
4431, 43bitri 275 . . . . . . . 8 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
4528, 44orbi12i 912 . . . . . . 7 ((โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โˆจ โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))))
4612, 45bitr2i 276 . . . . . 6 ((โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)))
4746abbii 2801 . . . . 5 {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))} = {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))}
4811, 47eqtri 2759 . . . 4 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))}) = {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))}
49 unab 4298 . . . . 5 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)))}) = {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))))}
50 rexun 4190 . . . . . . 7 (โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โˆจ โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
51 eqeq1 2735 . . . . . . . . . . 11 (๐‘ = ๐‘ก โ†’ (๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โ†” ๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))))
52512rexbidv 3218 . . . . . . . . . 10 (๐‘ = ๐‘ก โ†’ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))))
5352rexab 3690 . . . . . . . . 9 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
54 rexcom4 3284 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘กโˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
55 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘กโˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
56 ovex 7445 . . . . . . . . . . . . . 14 (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆˆ V
57 oveq2 7420 . . . . . . . . . . . . . . 15 (๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โ†’ ((๐ด ยทs ๐ต) +s ๐‘ก) = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))))
5857eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โ†’ (๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” ๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)))))
5956, 58ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” ๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))))
6059rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))))
6155, 60bitr3i 277 . . . . . . . . . . 11 (โˆƒ๐‘กโˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))))
6261rexbii 3093 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))))
63 r19.41vv 3223 . . . . . . . . . . 11 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
6463exbii 1849 . . . . . . . . . 10 (โˆƒ๐‘กโˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
6554, 62, 643bitr3ri 302 . . . . . . . . 9 (โˆƒ๐‘ก(โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))))
6653, 65bitri 275 . . . . . . . 8 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))))
67 eqeq1 2735 . . . . . . . . . . 11 (๐‘ = ๐‘ก โ†’ (๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โ†” ๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))))
68672rexbidv 3218 . . . . . . . . . 10 (๐‘ = ๐‘ก โ†’ (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))))
6968rexab 3690 . . . . . . . . 9 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
70 rexcom4 3284 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘กโˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
71 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘กโˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
72 ovex 7445 . . . . . . . . . . . . . 14 (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆˆ V
73 oveq2 7420 . . . . . . . . . . . . . . 15 (๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โ†’ ((๐ด ยทs ๐ต) +s ๐‘ก) = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))))
7473eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โ†’ (๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” ๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)))))
7572, 74ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” ๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))))
7675rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))))
7771, 76bitr3i 277 . . . . . . . . . . 11 (โˆƒ๐‘กโˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))))
7877rexbii 3093 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))))
79 r19.41vv 3223 . . . . . . . . . . 11 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
8079exbii 1849 . . . . . . . . . 10 (โˆƒ๐‘กโˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
8170, 78, 803bitr3ri 302 . . . . . . . . 9 (โˆƒ๐‘ก(โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))))
8269, 81bitri 275 . . . . . . . 8 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))))
8366, 82orbi12i 912 . . . . . . 7 ((โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โˆจ โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)))))
8450, 83bitr2i 276 . . . . . 6 ((โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)))) โ†” โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก))
8584abbii 2801 . . . . 5 {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))))} = {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)}
8649, 85eqtri 2759 . . . 4 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)))}) = {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)}
8748, 86uneq12i 4161 . . 3 (({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)))})) = ({๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)})
88 unab 4298 . . . . 5 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))}) = {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))}
89 rexun 4190 . . . . . . 7 (โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โˆจ โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
90 eqeq1 2735 . . . . . . . . . . 11 (๐‘ = ๐‘ก โ†’ (๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โ†” ๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))))
91902rexbidv 3218 . . . . . . . . . 10 (๐‘ = ๐‘ก โ†’ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))))
9291rexab 3690 . . . . . . . . 9 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
93 rexcom4 3284 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘กโˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
94 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘กโˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
95 ovex 7445 . . . . . . . . . . . . . 14 (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆˆ V
96 oveq1 7419 . . . . . . . . . . . . . . 15 (๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โ†’ (๐‘ก +s (๐ด ยทs ๐ถ)) = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
9796eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โ†’ (๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” ๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))))
9895, 97ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” ๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
9998rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
10094, 99bitr3i 277 . . . . . . . . . . 11 (โˆƒ๐‘กโˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
101100rexbii 3093 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
102 r19.41vv 3223 . . . . . . . . . . 11 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
103102exbii 1849 . . . . . . . . . 10 (โˆƒ๐‘กโˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
10493, 101, 1033bitr3ri 302 . . . . . . . . 9 (โˆƒ๐‘ก(โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
10592, 104bitri 275 . . . . . . . 8 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)))
106 eqeq1 2735 . . . . . . . . . . 11 (๐‘ = ๐‘ก โ†’ (๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โ†” ๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))))
1071062rexbidv 3218 . . . . . . . . . 10 (๐‘ = ๐‘ก โ†’ (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))))
108107rexab 3690 . . . . . . . . 9 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
109 rexcom4 3284 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘กโˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
110 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘กโˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
111 ovex 7445 . . . . . . . . . . . . . 14 (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆˆ V
112 oveq1 7419 . . . . . . . . . . . . . . 15 (๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โ†’ (๐‘ก +s (๐ด ยทs ๐ถ)) = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
113112eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โ†’ (๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” ๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))))
114111, 113ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” ๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
115114rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
116110, 115bitr3i 277 . . . . . . . . . . 11 (โˆƒ๐‘กโˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
117116rexbii 3093 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
118 r19.41vv 3223 . . . . . . . . . . 11 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
119118exbii 1849 . . . . . . . . . 10 (โˆƒ๐‘กโˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))))
120109, 117, 1193bitr3ri 302 . . . . . . . . 9 (โˆƒ๐‘ก(โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) โˆง ๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
121108, 120bitri 275 . . . . . . . 8 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))
122105, 121orbi12i 912 . . . . . . 7 ((โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)) โˆจ โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))}๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))) โ†” (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))))
12389, 122bitr2i 276 . . . . . 6 ((โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))) โ†” โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ)))
124123abbii 2801 . . . . 5 {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ)) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ)))} = {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))}
12588, 124eqtri 2759 . . . 4 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))}) = {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))}
126 unab 4298 . . . . 5 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)))}) = {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))))}
127 rexun 4190 . . . . . . 7 (โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โˆจ โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
128 eqeq1 2735 . . . . . . . . . . 11 (๐‘ = ๐‘ก โ†’ (๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โ†” ๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))))
1291282rexbidv 3218 . . . . . . . . . 10 (๐‘ = ๐‘ก โ†’ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))))
130129rexab 3690 . . . . . . . . 9 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
131 rexcom4 3284 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘กโˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
132 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘กโˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
133 ovex 7445 . . . . . . . . . . . . . 14 (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆˆ V
134 oveq2 7420 . . . . . . . . . . . . . . 15 (๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โ†’ ((๐ด ยทs ๐ต) +s ๐‘ก) = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))))
135134eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โ†’ (๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” ๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)))))
136133, 135ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” ๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))))
137136rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))))
138132, 137bitr3i 277 . . . . . . . . . . 11 (โˆƒ๐‘กโˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))))
139138rexbii 3093 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))))
140 r19.41vv 3223 . . . . . . . . . . 11 (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
141140exbii 1849 . . . . . . . . . 10 (โˆƒ๐‘กโˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
142131, 139, 1413bitr3ri 302 . . . . . . . . 9 (โˆƒ๐‘ก(โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))))
143130, 142bitri 275 . . . . . . . 8 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))))
144 eqeq1 2735 . . . . . . . . . . 11 (๐‘ = ๐‘ก โ†’ (๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โ†” ๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))))
1451442rexbidv 3218 . . . . . . . . . 10 (๐‘ = ๐‘ก โ†’ (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))))
146145rexab 3690 . . . . . . . . 9 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
147 rexcom4 3284 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘กโˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
148 rexcom4 3284 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘กโˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
149 ovex 7445 . . . . . . . . . . . . . 14 (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆˆ V
150 oveq2 7420 . . . . . . . . . . . . . . 15 (๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โ†’ ((๐ด ยทs ๐ต) +s ๐‘ก) = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))))
151150eqeq2d 2742 . . . . . . . . . . . . . 14 (๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โ†’ (๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” ๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)))))
152149, 151ceqsexv 3525 . . . . . . . . . . . . 13 (โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” ๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))))
153152rexbii 3093 . . . . . . . . . . . 12 (โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)โˆƒ๐‘ก(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))))
154148, 153bitr3i 277 . . . . . . . . . . 11 (โˆƒ๐‘กโˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))))
155154rexbii 3093 . . . . . . . . . 10 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘กโˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))))
156 r19.41vv 3223 . . . . . . . . . . 11 (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” (โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
157156exbii 1849 . . . . . . . . . 10 (โˆƒ๐‘กโˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)(๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ก(โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)))
158147, 155, 1573bitr3ri 302 . . . . . . . . 9 (โˆƒ๐‘ก(โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ก = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)) โˆง ๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))))
159146, 158bitri 275 . . . . . . . 8 (โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โ†” โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))))
160143, 159orbi12i 912 . . . . . . 7 ((โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก) โˆจ โˆƒ๐‘ก โˆˆ {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))}๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)) โ†” (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)))))
161127, 160bitr2i 276 . . . . . 6 ((โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)))) โ†” โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก))
162161abbii 2801 . . . . 5 {๐‘Ž โˆฃ (โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))) โˆจ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))))} = {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)}
163126, 162eqtri 2759 . . . 4 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)))}) = {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)}
164125, 163uneq12i 4161 . . 3 (({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)))})) = ({๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)})
16587, 164oveq12i 7424 . 2 ((({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)))})) |s (({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ)))}))) = (({๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)}) |s ({๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ))})๐‘Ž = (๐‘ก +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ก โˆˆ ({๐‘ โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘ = (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…))} โˆช {๐‘ โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘ = (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐ฟ))})๐‘Ž = ((๐ด ยทs ๐ต) +s ๐‘ก)}))
16610, 165eqtr4di 2789 1 (๐œ‘ โ†’ ((๐ด ยทs ๐ต) +s (๐ด ยทs ๐ถ)) = ((({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐ฟ)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐ฟ)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐‘… ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐‘… ยทs ๐‘ง๐‘…)))})) |s (({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ( R โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ฆ๐‘…)) +s (๐ด ยทs ๐ถ))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ( L โ€˜๐ต)๐‘Ž = ((((๐‘ฅ๐‘… ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ๐ฟ)) -s (๐‘ฅ๐‘… ยทs ๐‘ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))}) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ ( L โ€˜๐ด)โˆƒ๐‘ง๐‘… โˆˆ ( R โ€˜๐ถ)๐‘Ž = ((๐ด ยทs ๐ต) +s (((๐‘ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐‘ง๐‘…)) -s (๐‘ฅ๐ฟ ยทs ๐‘ง๐‘…)))} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ง๐ฟ โˆˆ ( L โ€˜๐ถ)๐‘Ž = ((๐ด ยท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  โ€˜cfv 6543  (class class class)co 7412   No csur 27380   |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