Step | Hyp | Ref
| Expression |
1 | | mulsunif.1 |
. . 3
โข (๐ โ ๐ฟ <<s ๐
) |
2 | | mulsunif.2 |
. . 3
โข (๐ โ ๐ <<s ๐) |
3 | | mulsunif.3 |
. . 3
โข (๐ โ ๐ด = (๐ฟ |s ๐
)) |
4 | | mulsunif.4 |
. . 3
โข (๐ โ ๐ต = (๐ |s ๐)) |
5 | 1, 2, 3, 4 | mulsuniflem 27953 |
. 2
โข (๐ โ (๐ด ยทs ๐ต) = (({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ๐
โ๐ โ ๐ โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) |s ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ฅ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ฅ)) -s (๐ ยทs ๐ฅ))}))) |
6 | | mulsval2lem 27914 |
. . . 4
โข {๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} = {๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} |
7 | | mulsval2lem 27914 |
. . . 4
โข {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))} = {โ โฃ โ๐ โ ๐
โ๐ โ ๐ โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} |
8 | 6, 7 | uneq12i 4153 |
. . 3
โข ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) = ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ๐
โ๐ โ ๐ โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) |
9 | | mulsval2lem 27914 |
. . . 4
โข {๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} = {๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} |
10 | | mulsval2lem 27914 |
. . . 4
โข {๐ โฃ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))} = {๐ โฃ โ๐ โ ๐
โ๐ฅ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ฅ)) -s (๐ ยทs ๐ฅ))} |
11 | 9, 10 | uneq12i 4153 |
. . 3
โข ({๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}) = ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ฅ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ฅ)) -s (๐ ยทs ๐ฅ))}) |
12 | 8, 11 | oveq12i 7413 |
. 2
โข (({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) |s ({๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))})) = (({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ๐
โ๐ โ ๐ โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) |s ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ฅ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ฅ)) -s (๐ ยทs ๐ฅ))})) |
13 | 5, 12 | eqtr4di 2782 |
1
โข (๐ โ (๐ด ยทs ๐ต) = (({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) |s ({๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}))) |