Step | Hyp | Ref
| Expression |
1 | | mulsval 27913 |
. 2
โข ((๐ด โ
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 ๐ฆ))}))) |
2 | | mulsval2lem 27914 |
. . . 4
โข {๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} = {๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} |
3 | | mulsval2lem 27914 |
. . . 4
โข {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))} = {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} |
4 | 2, 3 | uneq12i 4153 |
. . 3
โข ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) = ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) |
5 | | mulsval2lem 27914 |
. . . 4
โข {๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} = {๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( R โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} |
6 | | mulsval2lem 27914 |
. . . 4
โข {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))} = {๐ โฃ โ๐ฅ โ ( R โ๐ด)โ๐ฆ โ ( L โ๐ต)๐ = (((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ))} |
7 | 5, 6 | uneq12i 4153 |
. . 3
โข ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}) = ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( R โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ฅ โ ( R โ๐ด)โ๐ฆ โ ( L โ๐ต)๐ = (((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ))}) |
8 | 4, 7 | oveq12i 7413 |
. 2
โข (({๐ โฃ โ๐ โ ( 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 ๐ค))})) = (({๐ โฃ โ๐ โ ( 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 ๐ฆ))})) |
9 | 1, 8 | eqtr4di 2782 |
1
โข ((๐ด โ
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 ๐ค))}))) |