Step |
Hyp |
Ref |
Expression |
1 |
|
mulsval |
โข ( ( ๐ด โ 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 |
โข { ๐ โฃ โ ๐ โ ( L โ ๐ด ) โ ๐ โ ( L โ ๐ต ) ๐ = ( ( ( ๐ ยทs ๐ต ) +s ( ๐ด ยทs ๐ ) ) -s ( ๐ ยทs ๐ ) ) } = { ๐ โฃ โ ๐ โ ( L โ ๐ด ) โ ๐ โ ( L โ ๐ต ) ๐ = ( ( ( ๐ ยทs ๐ต ) +s ( ๐ด ยทs ๐ ) ) -s ( ๐ ยทs ๐ ) ) } |
3 |
|
mulsval2lem |
โข { ๐ โฃ โ ๐ โ ( R โ ๐ด ) โ ๐ โ ( R โ ๐ต ) ๐ = ( ( ( ๐ ยทs ๐ต ) +s ( ๐ด ยทs ๐ ) ) -s ( ๐ ยทs ๐ ) ) } = { โ โฃ โ ๐ โ ( R โ ๐ด ) โ ๐ โ ( R โ ๐ต ) โ = ( ( ( ๐ ยทs ๐ต ) +s ( ๐ด ยทs ๐ ) ) -s ( ๐ ยทs ๐ ) ) } |
4 |
2 3
|
uneq12i |
โข ( { ๐ โฃ โ ๐ โ ( 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 |
โข { ๐ โฃ โ ๐ก โ ( L โ ๐ด ) โ ๐ข โ ( R โ ๐ต ) ๐ = ( ( ( ๐ก ยทs ๐ต ) +s ( ๐ด ยทs ๐ข ) ) -s ( ๐ก ยทs ๐ข ) ) } = { ๐ โฃ โ ๐ โ ( L โ ๐ด ) โ ๐ โ ( R โ ๐ต ) ๐ = ( ( ( ๐ ยทs ๐ต ) +s ( ๐ด ยทs ๐ ) ) -s ( ๐ ยทs ๐ ) ) } |
6 |
|
mulsval2lem |
โข { ๐ โฃ โ ๐ฃ โ ( R โ ๐ด ) โ ๐ค โ ( L โ ๐ต ) ๐ = ( ( ( ๐ฃ ยทs ๐ต ) +s ( ๐ด ยทs ๐ค ) ) -s ( ๐ฃ ยทs ๐ค ) ) } = { ๐ โฃ โ ๐ฅ โ ( R โ ๐ด ) โ ๐ฆ โ ( L โ ๐ต ) ๐ = ( ( ( ๐ฅ ยทs ๐ต ) +s ( ๐ด ยทs ๐ฆ ) ) -s ( ๐ฅ ยทs ๐ฆ ) ) } |
7 |
5 6
|
uneq12i |
โข ( { ๐ โฃ โ ๐ก โ ( 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 |
โข ( ( { ๐ โฃ โ ๐ โ ( 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 |
โข ( ( ๐ด โ 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 ๐ค ) ) } ) ) ) |